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

Field Summary

Fields

Modifier and Type	Field	Description
private int[]	propagationCauses
private SatWrapper	wrapper

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

Method Summary

Modifier and Type	Method	Description
int	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 not
private void	clear()	clear everything (no more propagations or ignored literals)
void	initialize(SatWrapper wrapper)	connect the component to the wrapper
void	propagate(int literal, int assertedLiteral)	propagates the literal directly in the SAT solver
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 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 database
void	toCNF(java.io.BufferedWriter output)	It creates a CNF description of the clauses stored in this database.
java.lang.String	toString(java.lang.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

Field Detail

wrapper

private SatWrapper wrapper

propagationCauses

private int[] propagationCauses

Constructor Detail

DomainClausesDatabase

public DomainClausesDatabase()

Method Detail

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

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 propagate

assertedLiteral - the literal that has been the origin of the propagation

clear

private void clear()

clear everything (no more propagations or ignored literals)

resolutionWith

public MapClause resolutionWith(int clauseIndex,
                                MapClause clause)

to get a real clause to resolve with, we seek for the clause at the origin of the propagation.

Specified by:

resolutionWith in interface ClauseDatabaseInterface

Parameters:

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

Specified by:

backjump in interface ClauseDatabaseInterface

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

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

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.

Specified by:

removeClause in interface ClauseDatabaseInterface

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

Parameters:

clauseId - the unique Id of the clause

Returns:

true iff removal of clauses is possible

toString

public java.lang.String toString(java.lang.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

initialize

public void initialize(SatWrapper wrapper)

Description copied from interface: WrapperComponent

connect the component to the wrapper

Specified by:

initialize in interface WrapperComponent

Parameters:

wrapper - the wrapper

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

Specified by:

toCNF in class AbstractClausesDatabase

Parameters:

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

Throws:

java.io.IOException - execption from java.io package