Package org.jacop.jasat.core
Class Core
java.lang.Object
org.jacop.jasat.core.Core
- All Implemented Interfaces:
SolverComponent
The main solver structure, to be used either by a search component or by
another program that uses it for conflict learning and detection.
This implements interfaces for being manipulated from the outside, and from its components
- Version:
- 4.8
-
Field Summary
FieldsModifier and TypeFieldDescriptionlong
int
int
boolean
private int
private boolean
int
int
int
int
int
int
int
int
int
int
int
-
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionprivate int
addClause
(int[] clause, boolean isModelClause) add @param clause to the pool of clausesvoid
addComponent
(SolverComponent module) give the module access to the whole class, even if the solver is only known as a ISatSolverint
addModelClause
(int[] clause) same as previous, add the clause as a model clauseint
addModelClause
(IntVec clause) adds a clause to the solvervoid
assertLiteral
(int literal, int newLevel) decides a single step of search by setting the value of a variablevoid
backjumpToLevel
(int level) tells the SAT-solver to backtrack to the given level.boolean
canRemove
(int clauseId) predicate : can we remove the clause without breaking the correctness of the solver ?void
forget()
removes the less useful learnt clauses to free memoryint
gets a fresh variable that one can use for example for lazy clause generation.int
Computes at which level we should backjump to solve the conflict.int
getLevelToBackjump
(MapClause explanationClause) int
getManyFreshVariables
(int number) get several new variables at once, more efficiently than running getFreshVariable() @param number times.int
final int
before exiting, we must know which return code we must givefinal long
get the time associated with given mark, or 0 if nonefinal long
gets the time difference (in ms) between now and the markfinal boolean
void
initialize
(Core core) initializes the component with the given solver.final void
logs less important messages, in commentsfinal void
logs important messages in commentsfinal void
remembers that @param s is associated with the current time (in ms)final void
prints the current solution on standard outputboolean
removeClause
(int clauseId) removes the clause with unique Id, if possiblevoid
restart()
make a restart, that is, restart search from level 0.void
setMaxVariable
(int maxVariable) Tells the solver what is the greatest variable in the problemvoid
start()
notify all modules that we startvoid
stop()
notify all modules that we stoptoString()
private void
triggerAssertEvent
(int literal, int newLevel) triggers an event for assertion of a literalvoid
triggerBackjumpEvent
(int level) triggers an event to backjumpvoid
triggerConflictEvent
(MapClause clause) triggers a conflict.private void
triggers an event of forget()void
tells the SAT-solver to return to a normal state after a conflict has been solved (backjump or restart)void
triggerLearnEvent
(MapClause clauseToLearn) triggers an event of learningvoid
triggerPropagateEvent
(int literal, int unitClauseId) triggers a unit propagation event.void
triggers an event of restartvoid
to trigger if the problem is found to be satisfiablevoid
to trigger if the problem is found to be not satisfiablefinal void
performs propagation on all unit clauses until either : - no unit clause remains - a conflict occurs
-
Field Details
-
toPropagate
-
explanationClause
-
assignmentNum
public long assignmentNum -
mustForget
private boolean mustForget -
maxVariable
private int maxVariable -
timeMap
-
isStopped
public boolean isStopped -
timer
-
pool
-
dbStore
-
trail
-
search
-
config
-
verbosity
public int verbosity -
logStream
-
currentLevel
public int currentLevel -
currentState
public int currentState -
conflictLearning
-
assertionModules
-
backjumpModules
-
conflictModules
-
propagateModules
-
solutionModules
-
forgetModules
-
clauseModules
-
explanationModules
-
startStopModules
-
restartModules
-
numAssertionModules
public int numAssertionModules -
numBackjumpModules
public int numBackjumpModules -
numConflictModules
public int numConflictModules -
numPropagateModules
public int numPropagateModules -
numSolutionModules
public int numSolutionModules -
numForgetModules
public int numForgetModules -
numClauseModules
public int numClauseModules -
numExplanationModules
public int numExplanationModules -
numStartStopModules
public int numStartStopModules -
numRestartModules
public int numRestartModules
-
-
Constructor Details
-
Core
creates the solver, which in turn creates all inner components and connect them together.- Parameters:
config
- configuration for the solver
-
Core
public Core()initializes the solver with a default configuration.
-
-
Method Details
-
addModelClause
adds a clause to the solver- Parameters:
clause
- the clause to add- Returns:
- the unique ID of the clause
-
addModelClause
public int addModelClause(int[] clause) same as previous, add the clause as a model clause- Parameters:
clause
- the clause to add- Returns:
- the unique ID of this clause, or -1 if it is trivial
-
addClause
private int addClause(int[] clause, boolean isModelClause) add @param clause to the pool of clauses -
canRemove
public boolean canRemove(int clauseId) predicate : can we remove the clause without breaking the correctness of the solver ?- Parameters:
clauseId
- the unique Id of the clause- Returns:
- true if removing the clause is allowed
-
removeClause
public boolean removeClause(int clauseId) removes the clause with unique Id, if possible- Parameters:
clauseId
- the unique Id of the clause to remove- Returns:
- true if success, false if failure
-
assertLiteral
public void assertLiteral(int literal, int newLevel) decides a single step of search by setting the value of a variable- Parameters:
literal
- the literal to set truenewLevel
- the current search level
-
backjumpToLevel
public void backjumpToLevel(int level) tells the SAT-solver to backtrack to the given level. The level must be lower or equal to the solver's current level.- Parameters:
level
- the level to return to
-
restart
public void restart()make a restart, that is, restart search from level 0. -
start
public void start()notify all modules that we start -
stop
public void stop()notify all modules that we stop -
forget
public void forget()removes the less useful learnt clauses to free memory -
getLevelToBackjump
public int getLevelToBackjump()Computes at which level we should backjump to solve the conflict. The solver must be in CONFLICT state.- Returns:
- a level lower than the current level, in which the solver state would no longer be CONFLICT.
-
getLevelToBackjump
-
getFreshVariable
public int getFreshVariable()gets a fresh variable that one can use for example for lazy clause generation. If used, every clause added must use only the variables get by this way, or a variable collision could occur.- Returns:
- a fresh variable
-
getManyFreshVariables
public int getManyFreshVariables(int number) get several new variables at once, more efficiently than running getFreshVariable() @param number times. The variables range from the returned int to the returned int + @param number - 1- Parameters:
number
- the number of fresh variables we want- Returns:
- The first variable in the range of new variables
-
setMaxVariable
public void setMaxVariable(int maxVariable) Tells the solver what is the greatest variable in the problem- Parameters:
maxVariable
- the new maximum variable. Must not be lower than solver.getMaxVariable().
-
getMaxVariable
public int getMaxVariable()- Returns:
- the current max variable
-
addComponent
give the module access to the whole class, even if the solver is only known as a ISatSolver- Parameters:
module
- the module to add to the solver
-
unitPropagate
public final void unitPropagate()performs propagation on all unit clauses until either : - no unit clause remains - a conflict occurs -
triggerForgetEvent
private void triggerForgetEvent()triggers an event of forget() -
triggerAssertEvent
private void triggerAssertEvent(int literal, int newLevel) triggers an event for assertion of a literal- Parameters:
literal
- the literal assertednewLevel
- the new level, after assertion. It must be strictly greater than currentLevel.
-
triggerIdleEvent
public void triggerIdleEvent()tells the SAT-solver to return to a normal state after a conflict has been solved (backjump or restart) -
triggerLearnEvent
triggers an event of learning- Parameters:
clauseToLearn
- the clause which is learnt
-
triggerConflictEvent
triggers a conflict. The next step of the research should be conflict learning and then backjumping.- Parameters:
clause
- an unsatisfiable clause.
-
triggerPropagateEvent
public void triggerPropagateEvent(int literal, int unitClauseId) triggers a unit propagation event. This keeps the same level.- Parameters:
literal
- the unique unset literal, which must be true for the clause to be satisfiedunitClauseId
- the unique id of the unit clause that propagates
-
triggerBackjumpEvent
public void triggerBackjumpEvent(int level) triggers an event to backjump- Parameters:
level
- the level to backjump to
-
triggerRestartEvent
public void triggerRestartEvent()triggers an event of restart -
triggerSatEvent
public void triggerSatEvent()to trigger if the problem is found to be satisfiable -
triggerUnsatEvent
public void triggerUnsatEvent()to trigger if the problem is found to be not satisfiable -
markTime
remembers that @param s is associated with the current time (in ms)- Parameters:
s
- the mark of current time
-
getTime
get the time associated with given mark, or 0 if none- Parameters:
s
- the mark- Returns:
- the time associated with given mark, or 0 if none
-
getTimeDiff
gets the time difference (in ms) between now and the mark- Parameters:
s
- the mark- Returns:
- the time elapsed since mark, in ms
-
logc
logs important messages in comments- Parameters:
s
- the messageargs
- the arguments for the message
-
logc
logs less important messages, in comments- Parameters:
level
- verbosity levels
- the messageargs
- the arguments for the message
-
hasSolution
public final boolean hasSolution()- Returns:
- true if the solver reached a solution
-
printSolution
public final void printSolution()prints the current solution on standard output -
getReturnCode
public final int getReturnCode()before exiting, we must know which return code we must give- Returns:
- the return code to exit with
-
toString
-
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
-