|
Class Summary |
| Cnf |
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. |
| DimacsFileGenerator |
A Generator that simply reads a file representing a CNF
in the style used in the DIMACS implementation challenge. |
| Literal |
An object of this class represents a literal (signed symbol) |
| MyGenerator |
This is a template of the MyGenerator class that must be
turned in. |
| MySatSolver |
This is a template of the MySatSolver class that must be
turned in. |
| 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. |
| RandomSatisfiedCnfGenerator |
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. |
| RandomSearchSatSolver |
This is a trivial implementation of SatSolver that simply
generates random models and returns the best one when time runs
out. |
| Timer |
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. |