C D G I L M N R S T

C

CnfUtil - class CnfUtil.
This class includes several static methods which may be useful in processing CNF formulas.
CnfUtil() - Constructor for class CnfUtil
 
cnfToString(Literal[][]) - Static method in class CnfUtil
Converts a given CNF to a multi-line string representation suitable for printing.

D

DimacsFileGenerator - class DimacsFileGenerator.
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 Generator.
The interface for a CNF Generator.
getNext() - Method in class DimacsFileGenerator
Returns 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.
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 Literal.
An object of this class represents a literal (signed symbol)
Literal() - Constructor for class Literal
 

M

MyGenerator - class MyGenerator.
This is just a template of the MyGenerator class that must be turned in.
MyGenerator() - Constructor for class MyGenerator
Must have a constructor taking no arguments.
MySatSolver - class MySatSolver.
This is a dummy version of MySatSolver that simply generates random models and returns the best one when time runs out.
MySatSolver() - Constructor for class MySatSolver
A constructor for this class.
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.
modelToString(boolean[]) - Static method in class CnfUtil
Converts a given model (represented by a boolean array) to a string representation suitable for printing.

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

S

SatSolver - interface SatSolver.
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 dummy 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 Timer.
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.

C D G I L M N R S T