org.jacop.jasat.core

Class ConflictLearning

java.lang.Object

org.jacop.jasat.core.ConflictLearning

All Implemented Interfaces:

SolverComponent

public final class ConflictLearning
extends Object
implements SolverComponent

A solver component for conflict learning. (first UIP algorithm)

Version:

4.9

Author:

Simon Cruanes and Radoslaw Szymanek

Constructor Summary

Constructors

Constructor and Description
ConflictLearning()

Method Summary

Modifier and Type	Method and Description
void	applyExplainUIP(MapClause explanationClause) It builds the explanation clause made of all literals that were involved in a conflict (ie which are in the clause and were asserted, or were asserted and triggered, in another clause, the propagation of a literal present in the current clause)
int	getLevelToBackjump(MapClause explanationClause) It computes to which level we should backjump to solve the conflict explained by @param explanationClause
void	initialize(Core core) initializes the component with the given solver.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ConflictLearning

public ConflictLearning()

Method Detail

getLevelToBackjump

public int getLevelToBackjump(MapClause explanationClause)

It computes to which level we should backjump to solve the conflict explained by @param explanationClause

Parameters:

explanationClause - used for backjumping computation

Returns:

a level

applyExplainUIP

public void applyExplainUIP(MapClause explanationClause)

It builds the explanation clause made of all literals that were involved in a conflict (ie which are in the clause and were asserted, or were asserted and triggered, in another clause, the propagation of a literal present in the current clause)

Parameters:

explanationClause - the SetClause we use, which must be initialized to the conflict clause

initialize

public void initialize(Core core)

Description copied from interface: SolverComponent

initializes the component with the given solver. May be called only once. This method must register the component to the solver for the run.

Specified by:

initialize in interface SolverComponent

Parameters:

core - core component to initialize