A C D G I L M N P R S T

A

addClause() - Method in class Cnf

Adds a new clause to this CNF.

addLiteral(String, boolean) - Method in class Cnf

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

addLiteral(int, String, boolean) - Method in class Cnf

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

author() - Method in class DimacsFileGenerator

The author of this generator.

author() - Method in interface Generator

This method should simply return the "author" of this program as you would like it to appear on a class website.

author() - Method in class MyGenerator

This method should simply return the "author" of this program as you would like it to appear on a class website.

author() - Method in class MySatSolver

This method should simply return the "author" of this program as you would like it to appear on a class website.

author() - Method in class RandomCnfGenerator

The author of this generator.

author() - Method in class RandomSatisfiedCnfGenerator

The author of this generator.

author() - Method in class RandomSearchSatSolver

The author of this sat-solver.

author() - Method in interface SatSolver

This method should simply return the "author" of this program as you would like it to appear on a class website.

C

Cnf - Class in <Unnamed>

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.

Cnf() - Constructor for class Cnf

This is the constructor for the class.

D

description() - Method in class DimacsFileGenerator

A brief description of this generator.

description() - Method in interface Generator

This method should return a very brief (1-3 sentence) description (appropriate for posting on the class website) of how the CNF formulas are generated by this generator.

description() - Method in class MyGenerator

This method should return a very brief (1-3 sentence) description (appropriate for posting on the class website) of how the CNF formulas are generated by this generator.

description() - Method in class MySatSolver

This method should return a very brief (1-3 sentence) description of the algorithm and implementational improvements that are being used, appropriate for posting on the class website.

description() - Method in class RandomCnfGenerator

A brief description of this generator.

description() - Method in class RandomSatisfiedCnfGenerator

A brief description of this generator.

description() - Method in class RandomSearchSatSolver

A brief description of this sat-solver.

description() - Method in interface SatSolver

This method should return a very brief (1-3 sentence) description of the algorithm and implementational improvements that are being used, appropriate for posting on the class website.

DimacsFileGenerator - Class in <Unnamed>

A Generator that simply reads a file representing a CNF in the style used in the DIMACS implementation challenge.

DimacsFileGenerator(String) - Constructor for class DimacsFileGenerator

Constructor for this generator.

G

Generator - Interface in <Unnamed>

The interface for a CNF Generator.

getClauseLength(int) - Method in class Cnf

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

getNext() - Method in class DimacsFileGenerator

Returns (a clone of) the CNF read in from the named DIMACS file.

getNext() - Method in interface Generator

This method returns a new CNF formula each time it is called.

getNext() - Method in class MyGenerator

This is the method that generates CNF formulas, represented by Cnf objects, each time it is called.

getNext() - Method in class RandomCnfGenerator

Generates another CNF of the specified form.

getNext() - Method in class RandomSatisfiedCnfGenerator

Generates another CNF of the specified form.

getNumClauses() - Method in class Cnf

Returns the number of clauses in this CNF.

getNumSymbols() - Method in class Cnf

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

getSign(int, int) - Method in class Cnf

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

getSymbol(int, int) - Method in class Cnf

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

getSymbolName(int) - Method in class Cnf

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

getTimeElapsed() - Method in class Timer

Returns the time (in milliseconds) that has elapsed since the creation of this object.

getTimeRemaining() - Method in class Timer

Returns the time (in milliseconds) that remains until the timer object reaches the end of the period specified at its creation.

I

isClauseSat(Literal[], boolean[]) - Static method in class Cnf

Returns true if the given model satisfies the given clause.

L

Literal - Class in <Unnamed>

An object of this class represents a literal (signed symbol)

Literal(int, boolean) - Constructor for class Literal

constructor for creating a literal with the given sign and symbol index

M

main(String[]) - Static method in class DimacsFileGenerator

This is a simple main which runs MySatSolver on the CNF stored in the file named in the first argument within the time limit specified by the second argument.

main(String[]) - Static method in class MyGenerator

This is a simple main.

main(String[]) - Static method in class RandomCnfGenerator

This is a simple main.

main(String[]) - Static method in class RandomSatisfiedCnfGenerator

This is a simple main.

MyGenerator - Class in <Unnamed>

This is a template of the MyGenerator class that must be turned in.

MyGenerator() - Constructor for class MyGenerator

A constructor for this class.

MySatSolver - Class in <Unnamed>

This is a template of the MySatSolver class that must be turned in.

MySatSolver() - Constructor for class MySatSolver

A constructor for this class.

N

numClauseUnsat(Literal[][], boolean[]) - Static method in class Cnf

Returns the number of clauses of the given CNF not satisfied by the given model.

P

print() - Method in class Cnf

Prints this CNF to standard output.

printModel(boolean[]) - Method in class Cnf

Prints a given model to standard output.

R

RandomCnfGenerator - Class in <Unnamed>

This Generator generates random CNF formulas of a fixed size over a fixed number of symbols and with a fixed number of literals per clause.

RandomCnfGenerator(int, int, int) - Constructor for class RandomCnfGenerator

Constructor for this object.

RandomSatisfiedCnfGenerator - Class in <Unnamed>

This Generator generates random satisfiable CNF formulas of a fixed size over a fixed number of symbols and with a fixed number of literals per clause.

RandomSatisfiedCnfGenerator(int, int, int) - Constructor for class RandomSatisfiedCnfGenerator

Constructor for this object.

RandomSearchSatSolver - Class in <Unnamed>

This is a trivial implementation of SatSolver that simply generates random models and returns the best one when time runs out.

RandomSearchSatSolver() - Constructor for class RandomSearchSatSolver

A constructor for this class.

removeClause(int) - Method in class Cnf

Removes the entire specified clause from this CNF.

removeLiteral(int, int) - Method in class Cnf

Removes the specified literal from the specified clause from this CNF.

runSat(Generator, SatSolver, int, int) - Static method in class Cnf

Repeatedly calls a given sat-solver on CNF's generated by the given generator.

S

SatSolver - Interface in <Unnamed>

This is the interface defining a SatSolver object.

setLiteral(int, int, String, boolean) - Method in class Cnf

Replaces the literal in the specified position of this CNF.

sign - Variable in class Literal

sign of the literal: true = unnegated, false = negated

solve(Literal[][], int, Timer) - Method in class MySatSolver

This is the method for solving satifiability problems.

solve(Literal[][], int, Timer) - Method in class RandomSearchSatSolver

This routine attempts to solve the satisfaction problem by trying random models until time runs out and returning the best one.

solve(Literal[][], int, Timer) - Method in interface SatSolver

This is the method for solving satifiability problems.

symbol - Variable in class Literal

index of proposition symbol

T

Timer - Class in <Unnamed>

An object in this class acts as a timer, indicating both how much time has elapsed from the time the object was created, and how much time remains until the end of a specified period.

Timer(long) - Constructor for class Timer

This constructor begins a timer which will run for a period specified by the max_time parameter.

toLiteralArray() - Method in class Cnf

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

A C D G I L M N P R S T