ILits (SAT4J core 2.3.3 API)

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

Fields
Modifier and Type Field and Description

static int UNDEFINED

Fields
Modifier and Type	Field and Description
`static int`	`UNDEFINED`

Method Summary

Methods
Modifier and Type	Method and Description
`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.

Interface ILits

Field Summary

Method Summary

Field Detail

UNDEFINED

Method Detail

init

getFromPool

belongsToPool

resetPool

ensurePool

unassign

satisfies

forgets

isSatisfied

isFalsified

isUnassigned

isImplied

nVars

realnVars

nextFreeVarId

reset

getLevel

setLevel

getReason

setReason

undos

watch

watches

valueToString