Package org.jacop.satwrapper.translation
Class DomainClausesDatabase
java.lang.Object
org.jacop.jasat.core.clauses.AbstractClausesDatabase
org.jacop.satwrapper.translation.DomainClausesDatabase
- All Implemented Interfaces:
ClauseDatabaseInterface
,SolverComponent
,WrapperComponent
public final class DomainClausesDatabase
extends AbstractClausesDatabase
implements WrapperComponent
clause database designed to handle efficiently CP domain constraints, with
the interface of boolean clauses databases.
This database must be added in the SAT solver (ideally at first position) and linked to the wrapper; it can then propagate literals that have a CP semantic with respect to their meaning about domains.
- Version:
- 4.10
-
Field Summary
FieldsFields 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 assertedLiteral) this is responsible for propagating literals within the SAT solver to keep domain constraints coherent.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 void
clear()
clear everything (no more propagations or ignored literals)void
initialize
(SatWrapper wrapper) connect the component to the wrappervoid
propagate
(int literal, int assertedLiteral) propagates the literal directly in the SAT solverint
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) to get a real clause to resolve with, we seek for the clause at the origin of the propagation.int
size()
number of clauses in the databasevoid
toCNF
(BufferedWriter output) It creates a CNF description of the clauses stored in this database.prints the content of the database in a nice way, each line being prefixed withMethods inherited from class org.jacop.jasat.core.clauses.AbstractClausesDatabase
addWatch, doesWatch, ensureWatch, getDatabaseIndex, indexToUniqueId, initialize, removeWatch, setDatabaseIndex, swap, toString, uniqueIdToIndex
-
Field Details
-
wrapper
-
propagationCauses
private int[] propagationCauses
-
-
Constructor Details
-
DomainClausesDatabase
public DomainClausesDatabase()
-
-
Method Details
-
assertLiteral
public void assertLiteral(int assertedLiteral) this is responsible for propagating literals within the SAT solver to keep domain constraints coherent. It is informed by the SAT solver that some literal has been set, and propagate other variable literals.- Specified by:
assertLiteral
in interfaceClauseDatabaseInterface
- Parameters:
assertedLiteral
- the literal that is set
-
propagate
public void propagate(int literal, int assertedLiteral) propagates the literal directly in the SAT solver- Parameters:
literal
- the literal to propagateassertedLiteral
- the literal that has been the origin of the propagation
-
clear
private void clear()clear everything (no more propagations or ignored literals) -
resolutionWith
to get a real clause to resolve with, we seek for the clause at the origin of the propagation.- Specified by:
resolutionWith
in interfaceClauseDatabaseInterface
- 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.- Specified by:
backjump
in interfaceClauseDatabaseInterface
- 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
-
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.- Specified by:
addClause
in interfaceClauseDatabaseInterface
- 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 clauseId) Description copied from interface:ClauseDatabaseInterface
It removes the clause which unique ID is @param clauseId.- Specified by:
removeClause
in interfaceClauseDatabaseInterface
- 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- Specified by:
canRemove
in interfaceClauseDatabaseInterface
- Parameters:
clauseId
- the unique Id of the clause- Returns:
- true iff removal of clauses is possible
-
toString
Description copied from class:AbstractClausesDatabase
prints the content of the database in a nice way, each line being prefixed with- Overrides:
toString
in classAbstractClausesDatabase
- Parameters:
prefix
- prefix for printed line- Returns:
- a String representation of the database
-
initialize
Description copied from interface:WrapperComponent
connect the component to the wrapper- Specified by:
initialize
in interfaceWrapperComponent
- Parameters:
wrapper
- the wrapper
-
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
-