Package org.jacop.satwrapper
Class SatWrapper
java.lang.Object
org.jacop.constraints.DecomposedConstraint<Constraint>
org.jacop.constraints.Constraint
org.jacop.satwrapper.SatWrapper
- All Implemented Interfaces:
SatisfiedPresent
,Stateful
,SolverComponent
,ConflictListener
,ExplanationListener
,SolutionListener
,StartStopListener
public final class SatWrapper
extends Constraint
implements ConflictListener, ExplanationListener, StartStopListener, SolutionListener, Stateful, SatisfiedPresent
wrapper to communicate between SAT solver and CP solver.
It listens for SAT conflicts, so that it can force the CP solver to
backtrack until the conflict is resolved in SAT.
It listens to propagations, to know which literals are asserted in SAT, to
report those assertions on CP variables domains.
- Version:
- 4.8
-
Field Summary
FieldsModifier and TypeFieldDescriptionprivate MapClause
Integer[]
private int
(package private) boolean
private boolean
int
private final ArrayDeque<int[]>
private boolean
Integer[]
private IntQueue
private Trail
int
Fields inherited from class org.jacop.constraints.Constraint
atomicExecution, consistencyPruningEvents, constraintScope, earlyTerminationOK, increaseWeight, numberId, scope, trace
Fields inherited from class org.jacop.constraints.DecomposedConstraint
queueIndex
-
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionfinal void
addModelClause
(int[] clause) final void
addModelClause
(Collection<Integer> clause) add model (globally valid) clause to solver, in a delayed fashionprivate void
adds one level for SAT side, and remembers the association between CP and SAT levelsfinal void
addSolverComponent
(SolverComponent module) to add some module to the solverfinal void
addWrapperComponent
(WrapperComponent module) add a componentIt returns the variables in a scope of the constraint.final int
boolVarToCpValue
(int literal) transform a literal 'x=v' into a value 'v' for some CP variablefinal IntVar
boolVarToCpVar
(int literal) get the IntVar back from a literalfinal SatCPBridge
boolVarToDomain
(int literal) returns the CpVarDomain associated with this literalvoid
consistency
(Store store) The point where all operations are effectively done in the SAT solver, until no operation remains or a conflict occursfinal int
cpVarToBoolVar
(IntVar variable, int value, boolean isEquality) given a CP variable and a value, retrieve the associated boolean literal for either 'variable = value' or either 'variable <= value'final void
forget()
asks the solver to forget useless clauses, to free memoryint
It retrieves the pruning event which causes reevaluation of the constraint.int
int
asks the solver for which literal is the most active.id()
It gives the id string of a constraint.final void
impose
(Constraint constraint) add the constraint to the wrapper (ie, constraint.imposeToSat(this))final void
It imposes the constraint in a given store.void
It increases the weight of the variables in the constraint scope.void
initialize
(Core core) initializes the component with the given solver.final boolean
isEqualityBoolVar
(int literal) checks if the boolean variable represents an assertion 'x=v' or 'x<=v'final boolean
isVarLiteral
(int literal) checks if this literal corresponds to some CP variableboolean
log method, similar to printf.void
onConflict
(MapClause clause, int level) wrapper listens for conflicts.void
wrapper listens for explanations, to know how deep to backtrackvoid
onSolution
(boolean satisfiable) a handler called when a solution is found.void
onStart()
called when the solver starts search.void
onStop()
called when the solver stop search, for any reasonprivate void
assert the next literal from toAssertLiteralsvoid
queueVariable
(int level, Var var) This is a function called to indicate which variable in a scope of constraint has changed.void
void
registers the variable so that we can use it in SAT solvervoid
It removes the constraint by removing this constraint from all variables.void
removeLevel
(int cpLevel) when the CP solver decides to remove a level, the wrapper must force the SAT solver to backtrack accordingly, to keep mappings between the two search trees consistent.boolean
It checks if the constraint is satisfied.private void
setBoolVariable
(int variable, boolean value) called when a boolean variable is set to some boolean valueshowClauseMeaning
(Iterable<Integer> literals) showLiteralMeaning
(int literal) (for debug) show what a literal meansvoid
toCNF
(BufferedWriter output) toString()
It produces a string representation of a constraint state.Methods inherited from class org.jacop.constraints.Constraint
afc, cleanAfterFailure, decompose, getGuideConstraint, getGuideValue, getGuideVariable, grounded, grounded, impose, imposeDecomposition, intArrayToString, numberArgs, requiresMonotonicity, setConsistencyPruningEvent, setConstraintScope, setScope, setScope, setScope, setScope, setScope, setWatchedVariableGrounded, supplyGuideFeedback, updateAFC, watchedVariableGrounded
Methods inherited from class org.jacop.constraints.DecomposedConstraint
auxiliaryVariables, checkInput, checkInput, checkInputForDuplication, checkInputForDuplicationSkipSingletons, checkInputForNullness, checkInputForNullness, checkInputForNullness, derivative, getDubletonsSkipSingletons, imposeDecomposition
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
Methods inherited from interface org.jacop.api.Stateful
isStateful
-
Field Details
-
empty
boolean empty -
core
-
activity
-
assertionModule
-
boolVarToDomains
-
satChangesListener
-
store
-
pool
-
domainDatabase
-
domainTranslator
-
registeredVars
-
levelToBackjumpTo
public int levelToBackjumpTo -
satToCpLevels
-
cpToSatLevels
-
verbosity
public int verbosity -
trail
-
currentSatLevel
private int currentSatLevel -
modelClausesToAdd
-
toAssertLiterals
-
clauseToLearn
-
mustBacktrack
private boolean mustBacktrack -
hasSolution
private boolean hasSolution
-
-
Constructor Details
-
SatWrapper
public SatWrapper()creates everything in the right order
-
-
Method Details
-
register
-
register
registers the variable so that we can use it in SAT solver- Parameters:
variable
- the CP IntVar variabletranslate
- indicate whether to use == or <=
-
consistency
The point where all operations are effectively done in the SAT solver, until no operation remains or a conflict occurs- Specified by:
consistency
in classConstraint
- Parameters:
store
- constraint store within which the constraint consistency is being checked.
-
processOneLiteral
private void processOneLiteral()assert the next literal from toAssertLiterals -
addSatLevel
private void addSatLevel()adds one level for SAT side, and remembers the association between CP and SAT levels -
onConflict
wrapper listens for conflicts.- Specified by:
onConflict
in interfaceConflictListener
- Parameters:
clause
- the conflict (unsatisfiable) clauselevel
- the level at which the conflict occurred
-
onExplain
wrapper listens for explanations, to know how deep to backtrack- Specified by:
onExplain
in interfaceExplanationListener
- Parameters:
explanation
- the explanation clause
-
onSolution
public void onSolution(boolean satisfiable) Description copied from interface:SolutionListener
a handler called when a solution is found.- Specified by:
onSolution
in interfaceSolutionListener
- Parameters:
satisfiable
- true when the solution is Satisfiable, false if it is Unsatisfiable.
-
removeLevel
public void removeLevel(int cpLevel) when the CP solver decides to remove a level, the wrapper must force the SAT solver to backtrack accordingly, to keep mappings between the two search trees consistent. This is also the place where the wrapper can decide that a conflict in the SAT solver has been solved.- Specified by:
removeLevel
in interfaceStateful
- Parameters:
cpLevel
- the level which is being removed.
-
queueVariable
Description copied from class:Constraint
This is a function called to indicate which variable in a scope of constraint has changed. It also indicates a store level at which the change has occurred.- Overrides:
queueVariable
in classConstraint
- Parameters:
level
- the level of the store at which the change has occurred.var
- variable which has changed.
-
setBoolVariable
private void setBoolVariable(int variable, boolean value) called when a boolean variable is set to some boolean value- Parameters:
variable
- the boolean variablevalue
- the value (true or false) of this variable
-
getConsistencyPruningEvent
Description copied from class:Constraint
It retrieves the pruning event which causes reevaluation of the constraint.- Overrides:
getConsistencyPruningEvent
in classConstraint
- Parameters:
var
- variable for which pruning event is retrieved- Returns:
- it returns the int code of the pruning event (GROUND, BOUND, ANY, NONE)
-
getDefaultConsistencyPruningEvent
public int getDefaultConsistencyPruningEvent()- Specified by:
getDefaultConsistencyPruningEvent
in classConstraint
-
getMostActiveLiteral
public int getMostActiveLiteral()asks the solver for which literal is the most active. It will return a literal, which can be transformed into a variable and a value from the variable domain. Useful when the CP solver does not know which variable to set to continue research- Returns:
- a literal corresponding to some possible (variable,value)
-
showLiteralMeaning
(for debug) show what a literal means- Parameters:
literal
- literal for showing its meaning- Returns:
- literal meaning
-
showClauseMeaning
-
id
Description copied from class:Constraint
It gives the id string of a constraint.- Overrides:
id
in classConstraint
- Returns:
- string id of the constraint.
-
removeConstraint
public void removeConstraint()Description copied from class:Constraint
It removes the constraint by removing this constraint from all variables.- Overrides:
removeConstraint
in classConstraint
-
satisfied
public boolean satisfied()Description copied from interface:SatisfiedPresent
It checks if the constraint is satisfied. It can return false even if constraint is satisfied but not all variables in its scope are grounded. It needs to return true if all variables in its scope are grounded and constraint is satisfied.Implementations of this interface for constraints that are not PrimitiveConstraint may require constraint imposition and consistency check as a requirement to work correctly.
- Specified by:
satisfied
in interfaceSatisfiedPresent
- Returns:
- true if constraint is possible to verify that it is satisfied.
-
toString
Description copied from class:Constraint
It produces a string representation of a constraint state.- Overrides:
toString
in classConstraint
-
increaseWeight
public void increaseWeight()Description copied from class:Constraint
It increases the weight of the variables in the constraint scope.- Overrides:
increaseWeight
in classConstraint
-
arguments
Description copied from class:Constraint
It returns the variables in a scope of the constraint.- Overrides:
arguments
in classConstraint
- Returns:
- variables in a scope of the constraint.
-
addSolverComponent
to add some module to the solver- Parameters:
module
- the module to add
-
addWrapperComponent
add a component- Parameters:
module
- the component
-
forget
public final void forget()asks the solver to forget useless clauses, to free memory -
addModelClause
add model (globally valid) clause to solver, in a delayed fashion- Parameters:
clause
- the clause to add
-
addModelClause
public final void addModelClause(int[] clause) -
impose
add the constraint to the wrapper (ie, constraint.imposeToSat(this))- Parameters:
constraint
- the constraint to add
-
impose
Description copied from class:Constraint
It imposes the constraint in a given store.- Overrides:
impose
in classConstraint
- Parameters:
store
- the constraint store to which the constraint is imposed to.
-
cpVarToBoolVar
given a CP variable and a value, retrieve the associated boolean literal for either 'variable = value' or either 'variable <= value'- Parameters:
variable
- the CP variablevalue
- a value in the range of this variableisEquality
- a boolean, true if we want the literal that stands for 'x=d', false for 'x<=d'- Returns:
- the corresponding literal, or 0 if it is out of bounds
-
boolVarToDomain
returns the CpVarDomain associated with this literal- Parameters:
literal
- the boolean literal- Returns:
- a range
-
boolVarToCpVar
get the IntVar back from a literal- Parameters:
literal
- the literal- Returns:
- IntVar represented by the literal
-
boolVarToCpValue
public final int boolVarToCpValue(int literal) transform a literal 'x=v' into a value 'v' for some CP variable- Parameters:
literal
- literal to be transformed to value it represents- Returns:
- the value represented by this literal
-
isEqualityBoolVar
public final boolean isEqualityBoolVar(int literal) checks if the boolean variable represents an assertion 'x=v' or 'x<=v'- Parameters:
literal
- the boolean literal- Returns:
- true if the literal represents a proposition 'x=v', false if it represents 'x<=v'
-
isVarLiteral
public final boolean isVarLiteral(int literal) checks if this literal corresponds to some CP variable- Parameters:
literal
- the literal- Returns:
- true if this literal stands for some 'x=v' or 'x<=v' proposition
-
log
log method, similar to printf. Example: wrapper.log(this, "%s is %d", "foo", 42);- Parameters:
o
- the object that logs something (usethis
)format
- the format string (the message, if no formatting)args
- the arguments to fill in the format- Returns:
- always true
-
onStart
public void onStart()Description copied from interface:StartStopListener
called when the solver starts search. It will be called only once.- Specified by:
onStart
in interfaceStartStopListener
-
onStop
public void onStop()Description copied from interface:StartStopListener
called when the solver stop search, for any reason- Specified by:
onStop
in interfaceStartStopListener
-
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
-
toCNF
- Throws:
IOException
-