org.sat4j.minisat.constraints.cnf
Class Lits

java.lang.Object
  org.sat4j.minisat.constraints.cnf.Lits

All Implemented Interfaces:

Serializable, ILits

public final class Lits
extends Object
implements Serializable, ILits

Author:

laihem, leberre

See Also:

Serialized Form

Field Summary

Fields inherited from interface org.sat4j.minisat.core.ILits

UNDEFINED

Constructor Summary

Lits()

Method Summary

boolean	belongsToPool(int x) Returns true iff the variable is used in the set of constraints.
protected int	capacity() To get the capacity of the current vocabulary.
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	not(int lit)
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.
static String	toString(int lit)
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)

Methods inherited from class java.lang.Object

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

Constructor Detail

Lits

public Lits()

Method Detail

init

public final void init(int nvar)

Specified by:

init in interface ILits

getFromPool

public int getFromPool(int x)

Description copied from interface: ILits

Translates a Dimacs literal into an internal representation literal.

Specified by:

getFromPool in interface ILits

Parameters:

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

Returns:

the literal in the internal representation.

belongsToPool

public boolean belongsToPool(int x)

Description copied from interface: ILits

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

Specified by:

belongsToPool in interface ILits

Returns:

true iff the variable belongs to the formula.

resetPool

public void resetPool()

Description copied from interface: ILits

reset the vocabulary.

Specified by:

resetPool in interface ILits

ensurePool

public void ensurePool(int howmany)

Description copied from interface: ILits

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

Specified by:

ensurePool in interface ILits

Parameters:

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

unassign

public void unassign(int lit)

Description copied from interface: ILits

Unassigns a boolean variable (truth value if UNDEF).

Specified by:

unassign in interface ILits

Parameters:

lit - a literal in internal format.

satisfies

public void satisfies(int lit)

Description copied from interface: ILits

Satisfies a boolean variable (truth value is TRUE).

Specified by:

satisfies in interface ILits

Parameters:

lit - a literal in internal format.

forgets

public void forgets(int var)

Description copied from interface: ILits

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.

Specified by:

forgets in interface ILits

Parameters:

var - a variable in Dimacs format.

isSatisfied

public boolean isSatisfied(int lit)

Description copied from interface: ILits

Check if a literal is satisfied.

Specified by:

isSatisfied in interface ILits

Parameters:

lit - a literal in internal format.

Returns:

true if that literal is satisfied.

isFalsified

public final boolean isFalsified(int lit)

Description copied from interface: ILits

Check if a literal is falsified.

Specified by:

isFalsified in interface ILits

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

public boolean isUnassigned(int lit)

Description copied from interface: ILits

Check if a literal is assigned a truth value.

Specified by:

isUnassigned in interface ILits

Parameters:

lit - a literal in internal format.

Returns:

true if the literal is neither satisfied nor falsified.

valueToString

public String valueToString(int lit)

Description copied from interface: ILits

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

Specified by:

valueToString in interface ILits

Parameters:

lit - a literal in internal representation.

Returns:

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

nVars

public int nVars()

Description copied from interface: ILits

to obtain the max id of the variable

Specified by:

nVars in interface ILits

Returns:

the maximum number of variables in the formula

not

public int not(int lit)

toString

public static String toString(int lit)

reset

public void reset(int lit)

Description copied from interface: ILits

Reset a literal in the vocabulary.

Specified by:

reset in interface ILits

Parameters:

lit - a literal in internal representation.

getLevel

public int getLevel(int lit)

Description copied from interface: ILits

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

Specified by:

getLevel in interface ILits

Parameters:

lit - a literal in internal representation.

Returns:

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

setLevel

public void setLevel(int lit,
                     int l)

Description copied from interface: ILits

Sets the decision level of a literal.

Specified by:

setLevel in interface ILits

Parameters:

lit - a literal in internal representation.

l - a decision level, or -1

getReason

public Constr getReason(int lit)

Description copied from interface: ILits

Returns the reason of the assignment of a literal.

Specified by:

getReason in interface ILits

Parameters:

lit - a literal in internal representation.

Returns:

the constraint that propagated that literal, else null.

setReason

public void setReason(int lit,
                      Constr r)

Description copied from interface: ILits

Sets the reason of the assignment of a literal.

Specified by:

setReason in interface ILits

Parameters:

lit - a literal in internal representation.

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

undos

public IVec<Undoable> undos(int lit)

Description copied from interface: ILits

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

Specified by:

undos in interface ILits

Parameters:

lit - a literal in internal representation.

Returns:

a list of methods to call on bactracking.

watch

public void watch(int lit,
                  Propagatable c)

Description copied from interface: ILits

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

Specified by:

watch in interface ILits

Parameters:

lit - a literal in internal representation.

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

watches

public IVec<Propagatable> watches(int lit)

Specified by:

watches in interface ILits

Parameters:

lit - a literal in internal representation.

Returns:

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

isImplied

public boolean isImplied(int lit)

Specified by:

isImplied in interface ILits

Returns:

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

realnVars

public int realnVars()

Description copied from interface: ILits

to obtain the real number of variables appearing in the formula

Specified by:

realnVars in interface ILits

Returns:

the number of variables used in the pool

capacity

protected int capacity()

To get the capacity of the current vocabulary.

Returns:

the total number of variables that can be managed by the vocabulary.

nextFreeVarId

public int nextFreeVarId(boolean reserve)

Description copied from interface: ILits

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.

Specified by:

nextFreeVarId in interface ILits

Returns:

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

Since:

2.1