org.jacop.jasat.core.clauses

Class UnaryClausesDatabase

java.lang.Object

org.jacop.jasat.core.clauses.AbstractClausesDatabase

org.jacop.jasat.core.clauses.UnaryClausesDatabase

All Implemented Interfaces:

ClauseDatabaseInterface, SolverComponent

public final class UnaryClausesDatabase
extends AbstractClausesDatabase

A database for unit clauses (length 1). It only accepts those.

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

Method Summary

Modifier and Type	Method and Description
int	addClause(int[] clause, boolean isModel) TODO: Radek,
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.
String	toString(String prefix) prints the content of the database in a nice way, each line being prefixed with

Methods inherited from class org.jacop.jasat.core.clauses.AbstractClausesDatabase

addWatch, doesWatch, ensureWatch, getDatabaseIndex, indexToUniqueId, initialize, removeWatch, setDatabaseIndex, swap, toString, uniqueIdToIndex

Methods inherited from class java.lang.Object

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

Constructor Detail

UnaryClausesDatabase

public UnaryClausesDatabase()

Method Detail

addClause

public int addClause(int[] clause,
                     boolean isModel)

TODO: Radek,

why would you bother with having any code for removal when nothing is being actually removed. Why not disallow removal altogether and call it StaticUnaryClausesDatabase?

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

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

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

toString

public String toString(String prefix)

Description copied from class: AbstractClausesDatabase

prints the content of the database in a nice way, each line being prefixed with

Overrides:

toString in class AbstractClausesDatabase

Parameters:

prefix - prefix for printed line

Returns:

a String representation of the database

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