org.sat4j.minisat.core
Class LiteralsUtils

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

public final class LiteralsUtils
extends java.lang.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 reresenting 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)
           
static int var(int p)
           
 
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)

neg

public static int neg(int p)


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