Package org.jacop.jasat.core.clauses
Class LongClausesDatabase
java.lang.Object
org.jacop.jasat.core.clauses.AbstractClausesDatabase
org.jacop.jasat.core.clauses.LongClausesDatabase
- All Implemented Interfaces:
ClauseDatabaseInterface
,SolverComponent
A pool of long clauses, implemented with two watched an blocking literals
to minimize cache misses.
- Version:
- 4.9
-
Field Summary
FieldsModifier and TypeFieldDescriptionprivate int[][]
private int
private static final int
(package private) Random
Put it one place so there is only one Random generator for the whole SAT solver.private int[][]
private static final int
Fields inherited from class org.jacop.jasat.core.clauses.AbstractClausesDatabase
CLAUSE_RATE_AVERAGE, CLAUSE_RATE_I_WANT_THIS_CLAUSE, CLAUSE_RATE_LOW, CLAUSE_RATE_UNSUPPORTED, CLAUSE_RATE_WELL_SUPPORTED, core, databaseIndex, dbStore, MINIMUM_VAR_WATCH_SIZE, pool, trail, watchLists
-
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionint
addClause
(int[] clause, boolean isModel) It adds a clause to the database.void
assertLiteral
(int literal) It informs the ClausesDatabase that this literal is set, so that it can perform unit propagation.void
backjump
(int level) Do everything needed to return to the given level.boolean
canRemove
(int clauseId) It tells if the implementation of ClausesDatabase can remove clauses or notvoid
ensureSize
(int size) be sure that the database can contain numberOfClauses clausesprivate final boolean
isActive
(int literal) is the literal at position @param literalPos satisfied or active ?private final boolean
isActiveOrSatisfied
(int literal) is the literal at position @param literalPos satisfied or active ?private final boolean
isSatisfied
(int literal) is the literal at position @param literalPos satisfied in current trail ?int
rateThisClause
(int[] clause) Indicates how much this database is optimized for this clause.void
removeClause
(int clauseId) It removes the clause which unique ID is @param clauseId.resolutionWith
(int clauseIndex, MapClause clause) It returns the clause obtained by resolution between clauseIndex and clause.int
size()
number of clauses in the databasevoid
toCNF
(BufferedWriter output) It creates a CNF description of the clauses stored in this database.Methods inherited from class org.jacop.jasat.core.clauses.AbstractClausesDatabase
addWatch, doesWatch, ensureWatch, getDatabaseIndex, indexToUniqueId, initialize, removeWatch, setDatabaseIndex, swap, toString, toString, uniqueIdToIndex
-
Field Details
-
DEFAULT_INITIAL_NUMBER_OF_CLAUSES
private static final int DEFAULT_INITIAL_NUMBER_OF_CLAUSES- See Also:
-
SIZE_OF_CLAUSE_CACHE
private static final int SIZE_OF_CLAUSE_CACHE- See Also:
-
currentIndex
private int currentIndex -
clauses
private int[][] clauses -
literalsCache
private int[][] literalsCache -
generator
Random generatorPut it one place so there is only one Random generator for the whole SAT solver. TODO: Radek.
-
-
Constructor Details
-
LongClausesDatabase
public LongClausesDatabase()
-
-
Method Details
-
addClause
public int addClause(int[] clause, boolean isModel) Description copied from interface:ClauseDatabaseInterface
It adds a clause to the database. This can change the state of the solver, for example if the clause is unsatisfiable in the current trail affectation, the solver will get in the conflict state.- Parameters:
clause
- the clause to addisModel
- defined if the clause is model clause- Returns:
- the unique ID referring to the clause
-
assertLiteral
public void assertLiteral(int literal) Description copied from interface:ClauseDatabaseInterface
It informs the ClausesDatabase that this literal is set, so that it can perform unit propagation.- Parameters:
literal
- the literal that is set
-
removeClause
public void removeClause(int clauseId) Description copied from interface:ClauseDatabaseInterface
It removes the clause which unique ID is @param clauseId.- Parameters:
clauseId
- clause id
-
canRemove
public boolean canRemove(int clauseId) Description copied from interface:ClauseDatabaseInterface
It tells if the implementation of ClausesDatabase can remove clauses or not- Parameters:
clauseId
- the unique Id of the clause- Returns:
- true iff removal of clauses is possible
-
resolutionWith
Description copied from interface:ClauseDatabaseInterface
It returns the clause obtained by resolution between clauseIndex and clause. It will also modify in place the given SetClause (avoid allocating).- Parameters:
clauseIndex
- the unique id of the clauseclause
- an explanation clause that is modified by resolution- Returns:
- the clause obtained by resolution
-
backjump
public void backjump(int level) Description copied from interface:ClauseDatabaseInterface
Do everything needed to return to the given level.- Parameters:
level
- the level to return to. Must be < solver.getCurrentLevel().
-
rateThisClause
public int rateThisClause(int[] clause) Description copied from class:AbstractClausesDatabase
Indicates how much this database is optimized for this clause. The Database that gives the higher rank will get the clause.- Specified by:
rateThisClause
in classAbstractClausesDatabase
- Parameters:
clause
- a clause to rate- Returns:
- a non negative integer indicating how much the database is interested in this clause
-
size
public int size()Description copied from class:AbstractClausesDatabase
number of clauses in the database- Specified by:
size
in interfaceClauseDatabaseInterface
- Specified by:
size
in classAbstractClausesDatabase
- Returns:
- the number of clauses in the database
-
ensureSize
public void ensureSize(int size) be sure that the database can contain numberOfClauses clauses- Parameters:
size
- the size of the database to be ensured
-
isSatisfied
private final boolean isSatisfied(int literal) is the literal at position @param literalPos satisfied in current trail ? -
isActiveOrSatisfied
private final boolean isActiveOrSatisfied(int literal) is the literal at position @param literalPos satisfied or active ? -
isActive
private final boolean isActive(int literal) is the literal at position @param literalPos satisfied or active ? -
toCNF
Description copied from class:AbstractClausesDatabase
It creates a CNF description of the clauses stored in this database.- Specified by:
toCNF
in interfaceClauseDatabaseInterface
- Specified by:
toCNF
in classAbstractClausesDatabase
- Parameters:
output
- it specifies the target to which the description will be written.- Throws:
IOException
- execption from java.io package
-