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.
static void	runSat(Generator generator, SatSolver sat_solver, int num_reps, int time_limit) Repeatedly calls a given sat-solver on CNF's generated by the given generator.

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.

runSat

public static void runSat(Generator generator,
                          SatSolver sat_solver,
                          int num_reps,
                          int time_limit)

Repeatedly calls a given sat-solver on CNF's generated by the given generator. The process is repeated num_reps times. Each call to the sat-solver is limited to time_limit seconds.