|
Class Summary |
| CnfUtil |
This class includes several static methods which may be useful in
processing CNF formulas. |
| 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, as well as
how much time remains until the end of a specified period. |