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)
int	getFromPool(int x) Translates a Dimacs literal into an internal representation literal.
int	getLevel(int lit)
Constr	getReason(int lit)
void	init(int nvar)
boolean	isFalsified(int lit)
boolean	isImplied(int lit)
boolean	isSatisfied(int lit)
boolean	isUnassigned(int lit)
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)
void	resetPool()
void	satisfies(int lit)
void	setLevel(int lit, int l)
void	setReason(int lit, Constr r)
void	unassign(int lit)
IVec<Undoable>	undos(int lit)
String	valueToString(int lit)
void	watch(int lit, Propagatable c)
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()

ensurePool

void ensurePool(int howmany)

unassign

void unassign(int lit)

satisfies

void satisfies(int lit)

isSatisfied

boolean isSatisfied(int lit)

isFalsified

boolean isFalsified(int lit)

isUnassigned

boolean isUnassigned(int lit)

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

not

int not(int lit)

reset

void reset(int lit)

getLevel

int getLevel(int lit)

setLevel

void setLevel(int lit,
              int l)

getReason

Constr getReason(int lit)

setReason

void setReason(int lit,
               Constr r)

undos

IVec<Undoable> undos(int lit)

watch

void watch(int lit,
           Propagatable c)

watches

IVec<Propagatable> watches(int lit)

Parameters:

lit - a literal

Returns:

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

valueToString

String valueToString(int lit)