org.sat4j.minisat.core
Interface ILits

All Known Implementing Classes:

Lits

public interface ILits

That interface manages the solver's internal vocabulary. Everything related to variables and literals is available from here. For sake of efficiency, literals and variables are not object in SAT4J. They are represented by numbers. If the vocabulary contains n variables, then variables should be accessed by numbers from 1 to n and literals by numbers from 2 to 2*n+1. For a Dimacs variable v, the variable index in SAT4J is v, it's positive literal is 2*v (v << 1) and it's negative literal is 2*v+1 ((v<<1)^1). Note that one can easily access to the complementary literal of p by using bitwise operation ^. In SAT4J, literals are usualy denoted by p or q and variables by v or x.

Author:

leberre

Field Summary

static int

UNDEFINED

Method Summary

boolean	belongsToPool(int x) Returns true iff the variable is used in the set of constraints.
void	ensurePool(int howmany) Make sure that all data structures are ready to manage howmany boolean variables.
void	forgets(int var) Removes a variable from the formula.
int	getFromPool(int x) Translates a Dimacs literal into an internal representation literal.
int	getLevel(int lit) Returns the level at which that literal has been assigned a value, else -1.
Constr	getReason(int lit) Returns the reason of the assignment of a literal.
void	init(int nvar)
boolean	isFalsified(int lit) Check if a literal is falsified.
boolean	isImplied(int lit)
boolean	isSatisfied(int lit) Check if a literal is satisfied.
boolean	isUnassigned(int lit) Check if a literal is assigned a truth value.
int	nextFreeVarId(boolean reserve) Ask the solver for a free variable identifier, in Dimacs format (i.e. a positive number).
int	nVars() to obtain the max id of the variable
int	realnVars() to obtain the real number of variables appearing in the formula
void	reset(int lit) Reset a literal in the vocabulary.
void	resetPool() reset the vocabulary.
void	satisfies(int lit) Satisfies a boolean variable (truth value is TRUE).
void	setLevel(int lit, int l) Sets the decision level of a literal.
void	setReason(int lit, Constr r) Sets the reason of the assignment of a literal.
void	unassign(int lit) Unassigns a boolean variable (truth value if UNDEF).
IVec<Undoable>	undos(int lit) Retrieve the methods to call when the solver backtracks.
String	valueToString(int lit) Returns a textual representation of the truth value of that literal.
void	watch(int lit, Propagatable c) Record a new constraint to watch when a literal is satisfied.
IVec<Propagatable>	watches(int lit)

Field Detail

UNDEFINED

static final int UNDEFINED

See Also:

Constant Field Values

Method Detail

init

void init(int nvar)

getFromPool

int getFromPool(int x)

Translates a Dimacs literal into an internal representation literal.

Parameters:

x - the Dimacs literal (a non null integer).

Returns:

the literal in the internal representation.

belongsToPool

boolean belongsToPool(int x)

Returns true iff the variable is used in the set of constraints.

Parameters:

x -

Returns:

true iff the variable belongs to the formula.

resetPool

void resetPool()

reset the vocabulary.

ensurePool

void ensurePool(int howmany)

Make sure that all data structures are ready to manage howmany boolean variables.

Parameters:

howmany - the new capacity (in boolean variables) of the vocabulary.

unassign

void unassign(int lit)

Unassigns a boolean variable (truth value if UNDEF).

Parameters:

lit - a literal in internal format.

satisfies

void satisfies(int lit)

Satisfies a boolean variable (truth value is TRUE).

Parameters:

lit - a literal in internal format.

forgets

void forgets(int var)

Removes a variable from the formula. All occurrences of that variables are removed. It is equivalent in our implementation to falsify the two phases of that variable.

Parameters:

var - a variable in Dimacs format.

Since:

2.3.2

isSatisfied

boolean isSatisfied(int lit)

Check if a literal is satisfied.

Parameters:

lit - a literal in internal format.

Returns:

true if that literal is satisfied.

isFalsified

boolean isFalsified(int lit)

Check if a literal is falsified.

Parameters:

lit - a literal in internal format.

Returns:

true if the literal is falsified. Note that a forgotten variable will also see its literals as falsified.

isUnassigned

boolean isUnassigned(int lit)

Check if a literal is assigned a truth value.

Parameters:

lit - a literal in internal format.

Returns:

true if the literal is neither satisfied nor falsified.

isImplied

boolean isImplied(int lit)

Parameters:

lit -

Returns:

true iff the truth value of that literal is due to a unit propagation or a decision.

nVars

int nVars()

to obtain the max id of the variable

Returns:

the maximum number of variables in the formula

realnVars

int realnVars()

to obtain the real number of variables appearing in the formula

Returns:

the number of variables used in the pool

nextFreeVarId

int nextFreeVarId(boolean reserve)

Ask the solver for a free variable identifier, in Dimacs format (i.e. a positive number). Note that a previous call to ensurePool(max) will reserve in the solver the variable identifier from 1 to max, so nextFreeVarId() would return max+1, even if some variable identifiers smaller than max are not used.

Returns:

a variable identifier not in use in the constraints already inside the solver.

Since:

2.1

reset

void reset(int lit)

Reset a literal in the vocabulary.

Parameters:

lit - a literal in internal representation.

getLevel

int getLevel(int lit)

Returns the level at which that literal has been assigned a value, else -1.

Parameters:

lit - a literal in internal representation.

Returns:

-1 if the literal is unassigned, or the decision level of the literal.

setLevel

void setLevel(int lit,
              int l)

Sets the decision level of a literal.

Parameters:

lit - a literal in internal representation.

l - a decision level, or -1

getReason

Constr getReason(int lit)

Returns the reason of the assignment of a literal.

Parameters:

lit - a literal in internal representation.

Returns:

the constraint that propagated that literal, else null.

setReason

void setReason(int lit,
               Constr r)

Sets the reason of the assignment of a literal.

Parameters:

lit - a literal in internal representation.

r - the constraint that forces the assignment of that literal, null if there are none.

undos

IVec<Undoable> undos(int lit)

Retrieve the methods to call when the solver backtracks. Useful for counter based data structures.

Parameters:

lit - a literal in internal representation.

Returns:

a list of methods to call on bactracking.

watch

void watch(int lit,
           Propagatable c)

Record a new constraint to watch when a literal is satisfied.

Parameters:

lit - a literal in internal representation.

c - a constraint that contains the negation of that literal.

watches

IVec<Propagatable> watches(int lit)

Parameters:

lit - a literal in internal representation.

Returns:

the list of all the constraints that watch the negation of lit

valueToString

String valueToString(int lit)

Returns a textual representation of the truth value of that literal.

Parameters:

lit - a literal in internal representation.

Returns:

one of T for true, F for False or ? for unassigned.