Class CnfUtil

java.lang.Object
  extended byCnfUtil

public class CnfUtil
extends java.lang.Object

This class includes several static methods which may be useful in processing CNF formulas. A CNF is represented as an array of arrays of Literals, where each of the component arrays represents a disjunction of literals.


Constructor Summary
CnfUtil()
           
 
Method Summary
static java.lang.String cnfToString(Literal[][] cnf)
          Converts a given CNF to a multi-line string representation suitable for printing.
static int getNumSymbols(Literal[][] cnf)
          Returns one plus the largest index of any symbol referenced by the given CNF.
static boolean isClauseSat(Literal[] clause, boolean[] model)
          Returns true if the given model satisfies the given clause.
static java.lang.String modelToString(boolean[] model)
          Converts a given model (represented by a boolean array) to a string representation suitable for printing.
static int numClauseUnsat(Literal[][] cnf, boolean[] model)
          Returns the number of clauses of the given CNF not satisfied by the given model.
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

CnfUtil

public CnfUtil()
Method Detail

getNumSymbols

public static int getNumSymbols(Literal[][] cnf)
Returns one plus the largest index of any symbol referenced by the given CNF.


cnfToString

public static java.lang.String cnfToString(Literal[][] cnf)
Converts a given CNF to a multi-line string representation suitable for printing.


modelToString

public static java.lang.String modelToString(boolean[] model)
Converts a given model (represented by a boolean array) to a string representation suitable for printing.


isClauseSat

public static boolean isClauseSat(Literal[] clause,
                                  boolean[] model)
Returns true if the given model satisfies the given clause.


numClauseUnsat

public static int numClauseUnsat(Literal[][] cnf,
                                 boolean[] model)
Returns the number of clauses of the given CNF not satisfied by the given model.