A C D G I L M N R S T

A

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

cnfToString(Literal[][]) - Static method in class CnfUtil

Converts a given CNF to a multi-line string representation suitable for printing.

CnfUtil - Class in <Unnamed>

This class includes several static methods which may be useful in processing CNF formulas.

CnfUtil() - Constructor for class CnfUtil

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.

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 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.

getNumSymbols(Literal[][]) - Static method in class CnfUtil

Returns one plus the largest index of any symbol referenced by the given CNF.

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 CnfUtil

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() - Constructor for class Literal

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 RandomCnfGenerator

This is a simple main.

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

This is a simple main.

modelToString(boolean[]) - Static method in class CnfUtil

Converts a given model (represented by a boolean array) to a string representation suitable for printing.

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 CnfUtil

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

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.

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

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.

sign - Variable in class Literal

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

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

This is the method for solving satifiability problems.

solve(Literal[][], 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[][], 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, as well as 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.

A C D G I L M N R S T