Core (JaCoP 4.9.0 API)

java.lang.Object
- org.jacop.jasat.core.Core

All Implemented Interfaces:

SolverComponent
```
public final class Core
extends 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.9

Author:

Simon Cruanes and Radoslaw Szymanek

Field Summary

Fields
Modifier and Type	Field and Description
`AssertionListener[]`	`assertionModules`
`long`	`assignmentNum`
`BackjumpListener[]`	`backjumpModules`
`ClauseListener[]`	`clauseModules`
`Config`	`config`
`ConflictLearning`	`conflictLearning`
`ConflictListener[]`	`conflictModules`
`int`	`currentLevel`
`int`	`currentState`
`DatabasesStore`	`dbStore`
`MapClause`	`explanationClause`
`ExplanationListener[]`	`explanationModules`
`ForgetListener[]`	`forgetModules`
`boolean`	`isStopped`
`PrintStream`	`logStream`
`int`	`numAssertionModules`
`int`	`numBackjumpModules`
`int`	`numClauseModules`
`int`	`numConflictModules`
`int`	`numExplanationModules`
`int`	`numForgetModules`
`int`	`numPropagateModules`
`int`	`numRestartModules`
`int`	`numSolutionModules`
`int`	`numStartStopModules`
`MemoryPool`	`pool`
`PropagateListener[]`	`propagateModules`
`BackjumpListener[]`	`restartModules`
`SearchModule`	`search`
`SolutionListener[]`	`solutionModules`
`StartStopListener[]`	`startStopModules`
`Timer`	`timer`
`IntQueue`	`toPropagate`
`Trail`	`trail`
`int`	`verbosity`

Constructor Summary

Constructors
Constructor and Description
`Core()` initializes the solver with a default configuration.
`Core(Config config)` creates the solver, which in turn creates all inner components and connect them together.

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`void`	`addComponent(SolverComponent module)` give the module access to the whole class, even if the solver is only known as a ISatSolver
`int`	`addModelClause(int[] clause)` same as previous, add the clause as a model clause
`int`	`addModelClause(IntVec clause)` adds a clause to the solver
`void`	`assertLiteral(int literal, int newLevel)` decides a single step of search by setting the value of a variable
`void`	`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 memory
`int`	`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 give
`long`	`getTime(String s)` get the time associated with given mark, or 0 if none
`long`	`getTimeDiff(String s)` gets the time difference (in ms) between now and the mark
`boolean`	`hasSolution()`
`void`	`initialize(Core core)` initializes the component with the given solver.
`void`	`logc(int level, String s, Object... args)` logs less important messages, in comments
`void`	`logc(String s, Object... args)` logs important messages in comments
`void`	`markTime(String s)` remembers that @param s is associated with the current time (in ms)
`void`	`printSolution()` prints the current solution on standard output
`boolean`	`removeClause(int clauseId)` removes the clause with unique Id, if possible
`void`	`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 problem
`void`	`start()` notify all modules that we start
`void`	`stop()` notify all modules that we stop
`String`	`toString()`
`void`	`triggerBackjumpEvent(int level)` triggers an event to backjump
`void`	`triggerConflictEvent(MapClause clause)` triggers a conflict.
`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 learning
`void`	`triggerPropagateEvent(int literal, int unitClauseId)` triggers a unit propagation event.
`void`	`triggerRestartEvent()` triggers an event of restart
`void`	`triggerSatEvent()` to trigger if the problem is found to be satisfiable
`void`	`triggerUnsatEvent()` to trigger if the problem is found to be not satisfiable
`void`	`unitPropagate()` performs propagation on all unit clauses until either : - no unit clause remains - a conflict occurs

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

- Field Detail
  - toPropagate
```
public IntQueue toPropagate
```
  - explanationClause
```
public MapClause explanationClause
```
  - assignmentNum
```
public long assignmentNum
```
  - isStopped
```
public boolean isStopped
```
  - timer
```
public 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 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
  - 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 true
    
    newLevel - 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
  - 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 satisfied
    
    unitClauseId - 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(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(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(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(String s,
                       Object... args)
```
    logs important messages in comments
    
    Parameters:
    
    s - the message
    
    args - the arguments for the message
  - logc
```
public final void logc(int level,
                       String s,
                       Object... args)
```
    logs less important messages, in comments
    
    Parameters:
    
    level - verbosity level
    
    s - the message
    
    args - 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 String toString()
```
    Overrides:
    
    toString in class 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 interface SolverComponent
    
    Parameters:
    
    core - core component to initialize

Class Core

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

toPropagate

explanationClause

assignmentNum

isStopped

timer

pool

dbStore

trail

search

config

verbosity

logStream

currentLevel

currentState

conflictLearning

assertionModules

backjumpModules

conflictModules

propagateModules

solutionModules

forgetModules

clauseModules

explanationModules

startStopModules

restartModules

numAssertionModules

numBackjumpModules

numConflictModules

numPropagateModules

numSolutionModules

numForgetModules

numClauseModules

numExplanationModules

numStartStopModules

numRestartModules

Constructor Detail

Core

Core

Method Detail

addModelClause

addModelClause

canRemove

removeClause

assertLiteral

backjumpToLevel

restart

start

stop

forget

getLevelToBackjump

getLevelToBackjump

getFreshVariable

getManyFreshVariables

setMaxVariable

getMaxVariable

addComponent

unitPropagate

triggerIdleEvent

triggerLearnEvent

triggerConflictEvent

triggerPropagateEvent

triggerBackjumpEvent

triggerRestartEvent

triggerSatEvent

triggerUnsatEvent

markTime

getTime

getTimeDiff

logc

logc

hasSolution

printSolution

getReturnCode

toString