Sat Class Reference
[Example scripts (models)]
Example: CNF SAT solver More...
Public Member Functions
|Sat (const SatOptions &opt)|
|The actual problem. |
|Sat (bool share, Sat &s)|
|Constructor for cloning. |
|virtual Space *||copy (bool share)|
|Perform copying during cloning. |
|virtual void||print (std::ostream &os) const|
|Print solution. |
|void||parseDIMACS (const char *f)|
|Post constraints according to DIMACS file f. |
Example: CNF SAT solver
SAT finds assignments of Boolean variables such that a set of clauses is satisfied or shows that no such assignment exists.
This example parses a dimacs CNF file in which the constraints are specified. For each line of the file a clause propagator is posted.
Format of dimacs CNF files:
A dimacs file starts with comments (each line starts with c). The number of variables and the number of clauses is defined by the line
p cnf <variables> <clauses>
Each of the subsequent lines specifies a clause. A positive literal is denoted by a positive integer, a negative literal is denoted by the corresponding negative integer. Each line is terminated by 0.
c sample CNF file p cnf 3 2 3 -1 0 1 2 -1 0
Benchmarks on satlib.org, for instance, are in the dimacs CNF format.
Constructor & Destructor Documentation
|Sat::Sat||(||const SatOptions &||opt||)||
Member Function Documentation
|virtual Space* Sat::copy||(||bool||share||)||
|virtual void Sat::print||(||std::ostream &||os||)|| const
|void Sat::parseDIMACS||(||const char *||f||)||
The documentation for this class was generated from the following file:
- examples/sat.cpp (Revision: 15434)