Package org.jacop.jasat.core.clauses
Class TernaryClausesDatabase
- java.lang.Object
-
- org.jacop.jasat.core.clauses.AbstractClausesDatabase
-
- org.jacop.jasat.core.clauses.TernaryClausesDatabase
-
- All Implemented Interfaces:
ClauseDatabaseInterface
,SolverComponent
public final class TernaryClausesDatabase extends AbstractClausesDatabase
A database for ternary clauses. It only accepts those.It does not work with watched literals. All literals are watching and if any of them changes then clause is being checked for unit propagation.
Pros : no need to change watches. Cons : need to check the clause every time any literal changes.
TODO, check if this the efficient way of dealing with ternary clauses.
- Version:
- 4.8
-
-
Field Summary
Fields Modifier and Type Field Description private int[]
clauses
private int[]
curLit
private int
currentIndex
private int[]
curValues
private static int
INITIAL_SIZE
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 TernaryClausesDatabase()
-
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)
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 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.MapClause
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(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
-
INITIAL_SIZE
private static final int INITIAL_SIZE
- See Also:
- Constant Field Values
-
clauses
private int[] clauses
-
curValues
private int[] curValues
-
curLit
private int[] curLit
-
currentIndex
private int currentIndex
-
numRemoved
private int numRemoved
-
-
Method Detail
-
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
public MapClause resolutionWith(int clauseId, MapClause clause)
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
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
-
-