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
Fields Modifier and Type Field Description ActivityModule
activity
HeuristicAssertionModule
assertionModule
SatCPBridge[]
boolVarToDomains
private MapClause
clauseToLearn
Core
core
java.lang.Integer[]
cpToSatLevels
private int
currentSatLevel
DomainClausesDatabase
domainDatabase
DomainTranslator
domainTranslator
(package private) boolean
empty
private boolean
hasSolution
int
levelToBackjumpTo
private java.util.ArrayDeque<int[]>
modelClausesToAdd
private boolean
mustBacktrack
MemoryPool
pool
java.util.Set<IntVar>
registeredVars
SatChangesListener
satChangesListener
java.lang.Integer[]
satToCpLevels
Store
store
private IntQueue
toAssertLiterals
private Trail
trail
int
verbosity
-
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 Constructor Description SatWrapper()
creates everything in the right order
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description void
addModelClause(int[] clause)
void
addModelClause(java.util.Collection<java.lang.Integer> clause)
add model (globally valid) clause to solver, in a delayed fashionprivate void
addSatLevel()
adds one level for SAT side, and remembers the association between CP and SAT levelsvoid
addSolverComponent(SolverComponent module)
to add some module to the solvervoid
addWrapperComponent(WrapperComponent module)
add a componentjava.util.Set<Var>
arguments()
It returns the variables in a scope of the constraint.int
boolVarToCpValue(int literal)
transform a literal 'x=v' into a value 'v' for some CP variableIntVar
boolVarToCpVar(int literal)
get the IntVar back from a literalSatCPBridge
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 occursint
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'void
forget()
asks the solver to forget useless clauses, to free memoryint
getConsistencyPruningEvent(Var var)
It retrieves the pruning event which causes reevaluation of the constraint.int
getDefaultConsistencyPruningEvent()
int
getMostActiveLiteral()
asks the solver for which literal is the most active.java.lang.String
id()
It gives the id string of a constraint.void
impose(Constraint constraint)
add the constraint to the wrapper (ie, constraint.imposeToSat(this))void
impose(Store store)
It imposes the constraint in a given store.void
increaseWeight()
It increases the weight of the variables in the constraint scope.void
initialize(Core core)
initializes the component with the given solver.boolean
isEqualityBoolVar(int literal)
checks if the boolean variable represents an assertion 'x=v' or 'x<=v'boolean
isVarLiteral(int literal)
checks if this literal corresponds to some CP variableboolean
log(java.lang.Object o, java.lang.String format, java.lang.Object... args)
log method, similar to printf.void
onConflict(MapClause clause, int level)
wrapper listens for conflicts.void
onExplain(MapClause explanation)
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
processOneLiteral()
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
register(IntVar result)
void
register(IntVar variable, boolean translate)
registers the variable so that we can use it in SAT solvervoid
removeConstraint()
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
satisfied()
It checks if the constraint is satisfied.private void
setBoolVariable(int variable, boolean value)
called when a boolean variable is set to some boolean valuejava.lang.String
showClauseMeaning(java.lang.Iterable<java.lang.Integer> literals)
java.lang.String
showLiteralMeaning(int literal)
(for debug) show what a literal meansvoid
toCNF(java.io.BufferedWriter output)
java.lang.String
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 Detail
-
empty
boolean empty
-
core
public Core core
-
activity
public ActivityModule activity
-
assertionModule
public HeuristicAssertionModule assertionModule
-
boolVarToDomains
public SatCPBridge[] boolVarToDomains
-
satChangesListener
public SatChangesListener satChangesListener
-
store
public Store store
-
pool
public MemoryPool pool
-
domainDatabase
public DomainClausesDatabase domainDatabase
-
domainTranslator
public DomainTranslator domainTranslator
-
registeredVars
public final java.util.Set<IntVar> registeredVars
-
levelToBackjumpTo
public int levelToBackjumpTo
-
satToCpLevels
public java.lang.Integer[] satToCpLevels
-
cpToSatLevels
public java.lang.Integer[] cpToSatLevels
-
verbosity
public int verbosity
-
trail
private Trail trail
-
currentSatLevel
private int currentSatLevel
-
modelClausesToAdd
private final java.util.ArrayDeque<int[]> modelClausesToAdd
-
toAssertLiterals
private IntQueue toAssertLiterals
-
clauseToLearn
private MapClause clauseToLearn
-
mustBacktrack
private boolean mustBacktrack
-
hasSolution
private boolean hasSolution
-
-
Method Detail
-
register
public void register(IntVar result)
-
register
public void register(IntVar variable, boolean translate)
registers the variable so that we can use it in SAT solver- Parameters:
variable
- the CP IntVar variabletranslate
- indicate whether to use == or <=
-
consistency
public void consistency(Store store)
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
public void onConflict(MapClause clause, int level)
wrapper listens for conflicts.- Specified by:
onConflict
in interfaceConflictListener
- Parameters:
clause
- the conflict (unsatisfiable) clauselevel
- the level at which the conflict occurred
-
onExplain
public void onExplain(MapClause explanation)
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
public void queueVariable(int level, Var var)
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
public int getConsistencyPruningEvent(Var var)
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
public java.lang.String showLiteralMeaning(int literal)
(for debug) show what a literal means- Parameters:
literal
- literal for showing its meaning- Returns:
- literal meaning
-
showClauseMeaning
public java.lang.String showClauseMeaning(java.lang.Iterable<java.lang.Integer> literals)
-
id
public java.lang.String 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
public java.lang.String 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
public java.util.Set<Var> 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
public final void addSolverComponent(SolverComponent module)
to add some module to the solver- Parameters:
module
- the module to add
-
addWrapperComponent
public final void addWrapperComponent(WrapperComponent module)
add a component- Parameters:
module
- the component
-
forget
public final void forget()
asks the solver to forget useless clauses, to free memory
-
addModelClause
public final void addModelClause(java.util.Collection<java.lang.Integer> clause)
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
public final void impose(Constraint constraint)
add the constraint to the wrapper (ie, constraint.imposeToSat(this))- Parameters:
constraint
- the constraint to add
-
impose
public final void impose(Store store)
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
public final 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'- 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
public final SatCPBridge boolVarToDomain(int literal)
returns the CpVarDomain associated with this literal- Parameters:
literal
- the boolean literal- Returns:
- a range
-
boolVarToCpVar
public final IntVar boolVarToCpVar(int literal)
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
public boolean log(java.lang.Object o, java.lang.String format, java.lang.Object... args)
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
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
-
toCNF
public void toCNF(java.io.BufferedWriter output) throws java.io.IOException
- Throws:
java.io.IOException
-
-