Package org.jacop.jasat.core.clauses
Class BinaryClausesDatabase
java.lang.Object
org.jacop.jasat.core.clauses.AbstractClausesDatabase
org.jacop.jasat.core.clauses.BinaryClausesDatabase
- All Implemented Interfaces:
ClauseDatabaseInterface
,SolverComponent
A database for binary clauses. It only accepts those.
- Version:
- 4.8
-
Field Summary
FieldsModifier and TypeFieldDescriptionprivate int[]
private int
private static final int
private 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) TODO Efficiency,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 notprivate final int
notifyClause
(int clauseIndex) when something changed, find the status of the clauseint
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 clauseId, 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
-
INITIAL_SIZE
private static final int INITIAL_SIZE- See Also:
-
clauses
private int[] clauses -
currentIndex
private int currentIndex -
numRemoved
private int numRemoved
-
-
Constructor Details
-
BinaryClausesDatabase
public BinaryClausesDatabase()
-
-
Method Details
-
addClause
public int addClause(int[] clause, boolean isModel) TODO Efficiency,Watches require a very large array, but there maybe not so many binary clauses. Maybe a hashmap, connecting variable and list of watched clauses is more appropriate.
- 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:
clauseId
- 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
-
notifyClause
private final int notifyClause(int clauseIndex) when something changed, find the status of the clause- Parameters:
clauseIndex
- index of the clause- Returns:
- the state of the 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
-
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
-