Package org.jacop.jasat.core.clauses
Class DefaultClausesDatabase
- java.lang.Object
-
- org.jacop.jasat.core.clauses.AbstractClausesDatabase
-
- org.jacop.jasat.core.clauses.DefaultClausesDatabase
-
- All Implemented Interfaces:
ClauseDatabaseInterface
,SolverComponent
public final class DefaultClausesDatabase extends AbstractClausesDatabase
A standard database of clauses, implemented in an efficient way such that insertion or removal of clauses works fast.Two-watched literals are used for fast unit propagation. The two first literals of each clauses are the watches.
- Version:
- 4.7
-
-
Field Summary
Fields Modifier and Type Field Description private int[][]
clauses
private int
currentIndex
private static int
DEFAULT_INITIAL_NUMBER_OF_CLAUSES
private int
numRemoved
-
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 Constructor Description DefaultClausesDatabase()
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description int
addClause(int[] clause, boolean isModel)
It adds a clause to the database.void
assertLiteral(int literal)
Notify the watches that this literal is set, updating the watched clauses and propagating literals if pertinent.void
backjump(int level)
returns to the given levelboolean
canRemove(int clauseId)
It tells if the implementation of ClausesDatabase can remove clauses or notprivate java.lang.String
checkWatches4Clause(int clauseIndex)
(used for debug) checks if the 2 first literals of the clauses are exactly the set of literals that watch this clauseprivate java.lang.String
checkWatches4var(int var)
(used for debug) checks if the 2 first literals of the clauses are exactly the set of literals that watch this clausevoid
ensureSize(int size)
be sure that the database can contain @param size clausesprivate void
putAt0And1(int[] clause, int i, int j)
assuming i != j, this modifies clause so that the elements that were at position i and j will now be at position 0 and 1 (i.e.int
rateThisClause(int[] clause)
Indicates how much this database is optimized for this clause.void
removeClause(int clauseIndex)
It removes the clause which unique ID is @param clauseId.MapClause
resolutionWith(int clauseId, MapClause explanation)
It returns the clause obtained by resolution between clauseIndex and clause.int
size()
number of clauses in the databasevoid
toCNF(java.io.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 Detail
-
DEFAULT_INITIAL_NUMBER_OF_CLAUSES
private static final int DEFAULT_INITIAL_NUMBER_OF_CLAUSES
- See Also:
- Constant Field Values
-
clauses
private int[][] clauses
-
currentIndex
private int currentIndex
-
numRemoved
private int numRemoved
-
-
Method Detail
-
assertLiteral
public void assertLiteral(int literal)
Notify the watches that this literal is set, updating the watched clauses and propagating literals if pertinent. If a conflict occurs, the solver conflict Event will be triggered. This is the main part of unit propagation for the solver.It always creates a list of new watched list (newWatchedList).
- Parameters:
literal
- the literal that is being set
-
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
-
removeClause
public void removeClause(int clauseIndex)
Description copied from interface:ClauseDatabaseInterface
It removes the clause which unique ID is @param clauseId.- Parameters:
clauseIndex
- 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
public MapClause resolutionWith(int clauseId, MapClause explanation)
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:
clauseId
- the unique id of the clauseexplanation
- an explanation clause that is modified by resolution- Returns:
- the clause obtained by resolution
-
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
-
backjump
public void backjump(int level)
returns to the given level- Parameters:
level
- the level to return to. Must be < solver.getCurrentLevel().
-
checkWatches4Clause
private java.lang.String checkWatches4Clause(int clauseIndex)
(used for debug) checks if the 2 first literals of the clauses are exactly the set of literals that watch this clause- Parameters:
clauseIndex
- the index of the clause
-
checkWatches4var
private java.lang.String checkWatches4var(int var)
(used for debug) checks if the 2 first literals of the clauses are exactly the set of literals that watch this clause- Parameters:
clauseIndex
- the index of the clause
-
putAt0And1
private final void putAt0And1(int[] clause, int i, int j)
assuming i != j, this modifies clause so that the elements that were at position i and j will now be at position 0 and 1 (i.e. clause[i] becomes clause[0] and clause[j] becomes clause[1])- Parameters:
clause
- the clause to modifyi
- the first indexj
- the second index
-
ensureSize
public void ensureSize(int size)
be sure that the database can contain @param size clauses- Parameters:
size
- the number of clauses
-
toCNF
public void toCNF(java.io.BufferedWriter output) throws java.io.IOException
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:
java.io.IOException
- execption from java.io package
-
-