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.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
DefaultClausesDatabase()

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) 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 level
boolean	canRemove(int clauseId) It tells if the implementation of ClausesDatabase can remove clauses or not
void	ensureSize(int size) be sure that the database can contain @param size clauses
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 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

DefaultClausesDatabase

public DefaultClausesDatabase()

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 add

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

explanation - 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 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

backjump

public void backjump(int level)

returns to the given level

Parameters:

level - the level to return to. Must be < solver.getCurrentLevel().

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(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