Package org.jacop.jasat.core
Class ConflictLearning
- java.lang.Object
-
- org.jacop.jasat.core.ConflictLearning
-
- All Implemented Interfaces:
SolverComponent
public final class ConflictLearning extends java.lang.Object implements SolverComponent
A solver component for conflict learning. (first UIP algorithm)- Version:
- 4.7
-
-
Constructor Summary
Constructors Constructor Description ConflictLearning()
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description private void
applyExplain(MapClause explanationClause, int literal)
performs one step of resolution for conflict explanation on given explanation clause.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)private int
findPositionTopLiteral(MapClause explanationClause, int level, int startingPosition)
It gets the position of last set literal of the clause.int
getLevelToBackjump(MapClause explanationClause)
It computes to which level we should backjump to solve the conflict explained by @param explanationClausevoid
initialize(Core core)
initializes the component with the given solver.
-
-
-
Field Detail
-
core
private Core core
-
dbStore
private DatabasesStore dbStore
-
trail
private Trail trail
-
-
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
-
findPositionTopLiteral
private final int findPositionTopLiteral(MapClause explanationClause, int level, int startingPosition)
It gets the position of last set literal of the clause.- Parameters:
explanationClause
- the clauselevel
- the level of selectable literals- Returns:
- the last set literal of the clause, at current level, or 0 if none has been found
-
applyExplain
private final void applyExplain(MapClause explanationClause, int literal)
performs one step of resolution for conflict explanation on given explanation clause.- Parameters:
explanationClause
- the explanation clauseliteral
- the literal that must be resolved
-
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 interfaceSolverComponent
- Parameters:
core
- core component to initialize
-
-