Package org.jacop.jasat.core
Class Core
- java.lang.Object
-
- org.jacop.jasat.core.Core
-
- All Implemented Interfaces:
SolverComponent
public final class Core extends java.lang.Object implements 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
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description private 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
getFreshVariable()
gets a fresh variable that one can use for example for lazy clause generation.int
getLevelToBackjump()
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
getMaxVariable()
int
getReturnCode()
before exiting, we must know which return code we must givelong
getTime(java.lang.String s)
get the time associated with given mark, or 0 if nonelong
getTimeDiff(java.lang.String s)
gets the time difference (in ms) between now and the markboolean
hasSolution()
void
initialize(Core core)
initializes the component with the given solver.void
logc(int level, java.lang.String s, java.lang.Object... args)
logs less important messages, in commentsvoid
logc(java.lang.String s, java.lang.Object... args)
logs important messages in commentsvoid
markTime(java.lang.String s)
remembers that @param s is associated with the current time (in ms)void
printSolution()
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 stopjava.lang.String
toString()
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
triggerForgetEvent()
triggers an event of forget()void
triggerIdleEvent()
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
triggerRestartEvent()
triggers an event of restartvoid
triggerSatEvent()
to trigger if the problem is found to be satisfiablevoid
triggerUnsatEvent()
to trigger if the problem is found to be not satisfiablevoid
unitPropagate()
performs propagation on all unit clauses until either : - no unit clause remains - a conflict occurs
-
-
-
Field Detail
-
toPropagate
public IntQueue toPropagate
-
explanationClause
public MapClause explanationClause
-
assignmentNum
public long assignmentNum
-
mustForget
private boolean mustForget
-
maxVariable
private int maxVariable
-
timeMap
private java.util.Map<java.lang.String,java.lang.Long> timeMap
-
isStopped
public boolean isStopped
-
timer
public java.util.Timer timer
-
pool
public MemoryPool pool
-
dbStore
public DatabasesStore dbStore
-
trail
public Trail trail
-
search
public SearchModule search
-
config
public Config config
-
verbosity
public int verbosity
-
logStream
public java.io.PrintStream logStream
-
currentLevel
public int currentLevel
-
currentState
public int currentState
-
conflictLearning
public ConflictLearning conflictLearning
-
assertionModules
public AssertionListener[] assertionModules
-
backjumpModules
public BackjumpListener[] backjumpModules
-
conflictModules
public ConflictListener[] conflictModules
-
propagateModules
public PropagateListener[] propagateModules
-
solutionModules
public SolutionListener[] solutionModules
-
forgetModules
public ForgetListener[] forgetModules
-
clauseModules
public ClauseListener[] clauseModules
-
explanationModules
public ExplanationListener[] explanationModules
-
startStopModules
public StartStopListener[] startStopModules
-
restartModules
public BackjumpListener[] 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 Detail
-
Core
public Core(Config config)
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 Detail
-
addModelClause
public int addModelClause(IntVec clause)
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
public int getLevelToBackjump(MapClause explanationClause)
-
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
public void addComponent(SolverComponent module)
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
public void triggerLearnEvent(MapClause clauseToLearn)
triggers an event of learning- Parameters:
clauseToLearn
- the clause which is learnt
-
triggerConflictEvent
public void triggerConflictEvent(MapClause clause)
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
public final void markTime(java.lang.String s)
remembers that @param s is associated with the current time (in ms)- Parameters:
s
- the mark of current time
-
getTime
public final long getTime(java.lang.String s)
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
public final long getTimeDiff(java.lang.String s)
gets the time difference (in ms) between now and the mark- Parameters:
s
- the mark- Returns:
- the time elapsed since mark, in ms
-
logc
public final void logc(java.lang.String s, java.lang.Object... args)
logs important messages in comments- Parameters:
s
- the messageargs
- the arguments for the message
-
logc
public final void logc(int level, java.lang.String s, java.lang.Object... args)
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
public java.lang.String toString()
- Overrides:
toString
in classjava.lang.Object
-
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
-
-