Package org.jacop.jasat.core
Class ConflictLearning
java.lang.Object
org.jacop.jasat.core.ConflictLearning
- All Implemented Interfaces:
SolverComponent
A solver component for conflict learning. (first UIP algorithm)
- Version:
- 4.9
-
Field Summary
Fields -
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionprivate final 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 final 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 Details
-
core
-
dbStore
-
trail
-
-
Constructor Details
-
ConflictLearning
public ConflictLearning()
-
-
Method Details
-
getLevelToBackjump
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
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
performs one step of resolution for conflict explanation on given explanation clause.- Parameters:
explanationClause
- the explanation clauseliteral
- the literal that must be resolved
-
initialize
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
-