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. | |
Detailed Description
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.
Definition at line 115 of file sat.cpp.
Constructor & Destructor Documentation
| Sat::Sat | ( | const SatOptions & | opt | ) | [inline] |
| Sat::Sat | ( | bool | share, | |
| Sat & | s | |||
| ) | [inline] |
Member Function Documentation
| virtual Space* Sat::copy | ( | bool | share | ) | [inline, virtual] |
| virtual void Sat::print | ( | std::ostream & | os | ) | const [inline, virtual] |
Print solution.
Reimplemented from Gecode::Driver::ScriptBase< BaseSpace >.
| void Sat::parseDIMACS | ( | const char * | f | ) | [inline] |
The documentation for this class was generated from the following file:
- examples/sat.cpp (Revision: 11473)