org.sat4j.core
Class LiteralsUtils

java.lang.Object
  extended by org.sat4j.core.LiteralsUtils

public final class LiteralsUtils
extends Object

Utility methods to avoid using bit manipulation inside code. One should use Java 1.5 import static feature to use it without class qualification inside the code. In the DIMACS format, the literals are represented by signed integers, 0 denoting the end of the clause. In the solver, the literals are represented by positive integers, in order to use them as index in arrays for instance.

  int p : a literal (p>1)
  p ˆ 1 : the negation of the literal
  p >> 1 : the DIMACS number representing the variable.
  int v : a DIMACS variable (v>0)
  v << 1 : a positive literal for that variable in the solver.
  v << 1 ˆ 1 : a negative literal for that variable.
 

Author:
leberre

Method Summary
static int neg(int p)
          Returns the opposite literal.
static int negLit(int var)
          Returns the negative literal associated with a variable.
static int posLit(int var)
          Returns the positive literal associated with a variable.
static int toDimacs(int p)
          decode the internal representation of a literal in internal representation into Dimacs format.
static int toInternal(int x)
          encode the classical Dimacs representation (negated integers for negated literals) into the internal format.
static int var(int p)
          Returns the variable associated to the literal
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Method Detail

var

public static int var(int p)
Returns the variable associated to the literal

Parameters:
p - a literal in internal representation
Returns:
the Dimacs variable associated to that literal.

neg

public static int neg(int p)
Returns the opposite literal.

Parameters:
p - a literal in internal representation
Returns:
the opposite literal in internal representation

posLit

public static int posLit(int var)
Returns the positive literal associated with a variable.

Parameters:
var - a variable in Dimacs format
Returns:
the positive literal associated with this variable in internal representation

negLit

public static int negLit(int var)
Returns the negative literal associated with a variable.

Parameters:
var - a variable in Dimacs format
Returns:
the negative literal associated with this variable in internal representation

toDimacs

public static int toDimacs(int p)
decode the internal representation of a literal in internal representation into Dimacs format.

Parameters:
p - the literal in internal representation
Returns:
the literal in dimacs representation

toInternal

public static int toInternal(int x)
encode the classical Dimacs representation (negated integers for negated literals) into the internal format.

Parameters:
x - the literal in Dimacs format
Returns:
the literal in internal format.
Since:
2.2


Copyright © 2010 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.