Class Cnf

java.lang.Object
  Cnf

public class Cnf
extends java.lang.Object

This class provides a representation of a CNF, including methods for constructing the CNF, for converting it into an array of arrays of Literals, and for printing. The class also includes a number of static methods which may be useful in processing CNF formulas.

In most cases, a complete CNF can be created using the constructor (which constructs an empty CNF), and the methods addClause() (which adds a clause to the CNF), and addLiteral() (which adds a literal to one of the clauses, by default, the last clause). Other methods are provided for accessing or setting individual literals of individual clauses, and for removing literals or entire clauses.

Each clause has an index as in an array, the first having index 0, the next with index 1, etc. Similarly, within each clause, every literal has an index according to the order in which it was added. Clauses and literals can be accessed using these indices. In addition, the method toLiteralArray() returns an array of arrays of Literals containing all of the elements of the CNF in the correct order according to this indexing.

A literal is generally specified by a sign and a symbol. The sign is represented by a boolean which is false if the literal is negated, and true otherwise. Each symbol is given by an arbitrary String, and two such symbols are considered the same if and only if the corresponding Strings are equal. However, the components of the array of arrays returned by toLiteralArray() represent each symbol by its index, i.e., by an integer between 0 and getNumSymbols() - 1. The String corresponding to such an index can be accessed using the getSymbolName() method.

Constructor Summary

Cnf()
This is the constructor for the class.

Method Summary

void	addClause() Adds a new clause to this CNF.
void	addLiteral(int clause, java.lang.String symbol, boolean sign) Adds a new literal to a specified clause of this CNF.
void	addLiteral(java.lang.String symbol, boolean sign) Adds a new literal to the last clause that was added to the CNF.
int	getClauseLength(int clause) Returns the number of literals in the specified clause of this CNF.
int	getNumClauses() Returns the number of clauses in this CNF.
int	getNumSymbols() Returns the number of unique symbols appearing in literals that have been added to this CNF.
boolean	getSign(int clause, int index) Returns the sign for the literal in the specified position of this CNF.
java.lang.String	getSymbol(int clause, int index) Returns the symbol for the literal in the specified position of this CNF.
java.lang.String	getSymbolName(int index) Returns the name (as a String) of the symbol with the given index.
static boolean	isClauseSat(Literal[] clause, boolean[] model) Returns true if the given model satisfies the given clause.
static int	numClauseUnsat(Literal[][] cnf, boolean[] model) Returns the number of clauses of the given CNF not satisfied by the given model.
void	print() Prints this CNF to standard output.
void	printModel(boolean[] model) Prints a given model to standard output.
void	removeClause(int clause) Removes the entire specified clause from this CNF.
void	removeLiteral(int clause, int index) Removes the specified literal from the specified clause from this CNF.
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.
void	setLiteral(int clause, int index, java.lang.String symbol, boolean sign) Replaces the literal in the specified position of this CNF.
Literal[][]	toLiteralArray() Returns this CNF represented as an array of arrays of Literals.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Cnf

public Cnf()

This is the constructor for the class. It simply creates an empty CNF.

Method Detail

addClause

public void addClause()

Adds a new clause to this CNF.

addLiteral

public void addLiteral(java.lang.String symbol,
                       boolean sign)

Adds a new literal to the last clause that was added to the CNF.

Parameters:

symbol - the symbol of the new literal, as a String

sign - the sign of the new literal

Throws:

java.util.NoSuchElementException - if CNF is empty

addLiteral

public void addLiteral(int clause,
                       java.lang.String symbol,
                       boolean sign)

Adds a new literal to a specified clause of this CNF.

Parameters:

clause - index of clause to which literal is to be added

symbol - the symbol of the new literal, as a String

sign - the sign of the new literal

Throws:

java.lang.ArrayIndexOutOfBoundsException - if clause index is out of range

getNumSymbols

public int getNumSymbols()

Returns the number of unique symbols appearing in literals that have been added to this CNF.

getNumClauses

public int getNumClauses()

Returns the number of clauses in this CNF.

getClauseLength

public int getClauseLength(int clause)

Returns the number of literals in the specified clause of this CNF.

Parameters:

clause - index of specified clause

Throws:

java.lang.ArrayIndexOutOfBoundsException - if clause index is out of range

getSymbol

public java.lang.String getSymbol(int clause,
                                  int index)

Returns the symbol for the literal in the specified position of this CNF.

Parameters:

clause - index of specified clause

index - index of specified literal within that clause

Throws:

java.lang.ArrayIndexOutOfBoundsException - if either index is out of range

getSign

public boolean getSign(int clause,
                       int index)

Returns the sign for the literal in the specified position of this CNF.

Parameters:

clause - index of specified clause

index - index of specified literal within that clause

Throws:

java.lang.ArrayIndexOutOfBoundsException - if either index is out of range

setLiteral

public void setLiteral(int clause,
                       int index,
                       java.lang.String symbol,
                       boolean sign)

Replaces the literal in the specified position of this CNF.

Parameters:

clause - index of specified clause

index - index of specified literal within that clause

symbol - the symbol of the new literal, as a String

sign - the sign of the new literal

Throws:

java.lang.ArrayIndexOutOfBoundsException - if either index is out of range

removeClause

public void removeClause(int clause)

Removes the entire specified clause from this CNF. Shifts any subsequent clauses to the left (subtracts one from their indices).

Parameters:

clause - index of specified clause

Throws:

java.lang.ArrayIndexOutOfBoundsException - if clause index is out of range

removeLiteral

public void removeLiteral(int clause,
                          int index)

Removes the specified literal from the specified clause from this CNF. Shifts any subsequent literals of the clause to the left (subtracts one from their indices).

Parameters:

clause - index of specified clause

Throws:

java.lang.ArrayIndexOutOfBoundsException - if either index is out of range

getSymbolName

public java.lang.String getSymbolName(int index)

Returns the name (as a String) of the symbol with the given index.

Parameters:

index - index of specified symbol

Throws:

java.lang.IndexOutOfBoundsException - if index is out of range

toLiteralArray

public Literal[][] toLiteralArray()

Returns this CNF represented as an array of arrays of Literals.

print

public void print()

Prints this CNF to standard output.

printModel

public void printModel(boolean[] model)

Prints a given model to standard output. The given model is a boolean array representing a truth assignment to each of the symbols, and thus must have length equal to getNumSymbols().

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.

isClauseSat

public static boolean isClauseSat(Literal[] clause,
                                  boolean[] model)

Returns true if the given model satisfies the given clause. The given model is represented as a boolean array representing a truth assignment to a set of symbols. The given clause is an array of Literals over the same set of symbols.

numClauseUnsat

public static int numClauseUnsat(Literal[][] cnf,
                                 boolean[] model)

Returns the number of clauses of the given CNF not satisfied by the given model. The given model is represented as a boolean array representing a truth assignment to a set of symbols. The given cnf is an array of arrays of Literals over the same set of symbols.