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.9

Author:

Simon Cruanes and Radoslaw Szymanek

Field Summary

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 and Description
TernaryClausesDatabase()

Method Summary

Modifier and Type	Method and 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 not
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.
MapClause	resolutionWith(int clauseId, MapClause clause) It returns the clause obtained by resolution between clauseIndex and clause.
int	size() number of clauses in the database
void	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

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

TernaryClausesDatabase

public TernaryClausesDatabase()

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 add

isModel - 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 clause

clause - 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 class AbstractClausesDatabase

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 interface ClauseDatabaseInterface

Specified by:

size in class AbstractClausesDatabase

Returns:

the number of clauses in the database

toCNF

public void toCNF(BufferedWriter output)
           throws IOException

Description copied from class: AbstractClausesDatabase

It creates a CNF description of the clauses stored in this database.

Specified by:

toCNF in interface ClauseDatabaseInterface

Specified by:

toCNF in class AbstractClausesDatabase

Parameters:

output - it specifies the target to which the description will be written.

Throws:

IOException - execption from java.io package