Class CnfUtil

java.lang.Object
  CnfUtil

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.