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.9

Author:

Simon Cruanes and Radoslaw Szymanek

Field Summary

Fields

Modifier and Type	Field and Description
ActivityModule	activity
HeuristicAssertionModule	assertionModule
SatCPBridge[]	boolVarToDomains
Core	core
Integer[]	cpToSatLevels
DomainClausesDatabase	domainDatabase
DomainTranslator	domainTranslator
int	levelToBackjumpTo
MemoryPool	pool
Set<IntVar>	registeredVars
SatChangesListener	satChangesListener
Integer[]	satToCpLevels
Store	store
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 and Description
SatWrapper() creates everything in the right order

Method Summary

Modifier and Type	Method and Description
void	addModelClause(Collection<Integer> clause) add model (globally valid) clause to solver, in a delayed fashion
void	addModelClause(int[] clause)
void	addSolverComponent(SolverComponent module) to add some module to the solver
void	addWrapperComponent(WrapperComponent module) add a component
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 variable
IntVar	boolVarToCpVar(int literal) get the IntVar back from a literal
SatCPBridge	boolVarToDomain(int literal) returns the CpVarDomain associated with this literal
void	consistency(Store store) The point where all operations are effectively done in the SAT solver, until no operation remains or a conflict occurs
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'
void	forget() asks the solver to forget useless clauses, to free memory
int	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.
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 variable
boolean	log(Object o, String format, 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 backtrack
void	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 reason
void	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 solver
void	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.
String	showClauseMeaning(Iterable<Integer> literals)
String	showLiteralMeaning(int literal) (for debug) show what a literal means
void	toCNF(BufferedWriter output)
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, long2int, 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

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 Set<IntVar> registeredVars

levelToBackjumpTo

public int levelToBackjumpTo

satToCpLevels

public Integer[] satToCpLevels

cpToSatLevels

public Integer[] cpToSatLevels

verbosity

public int verbosity

Constructor Detail

SatWrapper

public SatWrapper()

creates everything in the right order

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 variable

translate - 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 class Constraint

Parameters:

store - constraint store within which the constraint consistency is being checked.

onConflict

public void onConflict(MapClause clause,
                       int level)

wrapper listens for conflicts.

Specified by:

onConflict in interface ConflictListener

Parameters:

clause - the conflict (unsatisfiable) clause

level - 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 interface ExplanationListener

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 interface SolutionListener

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 interface Stateful

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 class Constraint

Parameters:

level - the level of the store at which the change has occurred.

var - variable which has changed.

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 class Constraint

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 class Constraint

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 String showLiteralMeaning(int literal)

(for debug) show what a literal means

Parameters:

literal - literal for showing its meaning

Returns:

literal meaning

showClauseMeaning

public String showClauseMeaning(Iterable<Integer> literals)

id

public String id()

Description copied from class: Constraint

It gives the id string of a constraint.

Overrides:

id in class Constraint

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 class Constraint

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 interface SatisfiedPresent

Returns:

true if constraint is possible to verify that it is satisfied.

toString

public String toString()

Description copied from class: Constraint

It produces a string representation of a constraint state.

Overrides:

toString in class Constraint

increaseWeight

public void increaseWeight()

Description copied from class: Constraint

It increases the weight of the variables in the constraint scope.

Overrides:

increaseWeight in class Constraint

arguments

public Set<Var> arguments()

Description copied from class: Constraint

It returns the variables in a scope of the constraint.

Overrides:

arguments in class Constraint

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(Collection<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 class Constraint

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 variable

value - a value in the range of this variable

isEquality - 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(Object o,
                   String format,
                   Object... args)

log method, similar to printf. Example: wrapper.log(this, "%s is %d", "foo", 42);

Parameters:

o - the object that logs something (use this)

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 interface StartStopListener

onStop

public void onStop()

Description copied from interface: StartStopListener

called when the solver stop search, for any reason

Specified by:

onStop in interface StartStopListener

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

toCNF

public void toCNF(BufferedWriter output)
           throws IOException

Throws:

IOException