Example: CNF SAT solver More...
Public Member Functions | |
Sat (const SatOptions &opt) | |
The actual problem. More... | |
Sat (bool share, Sat &s) | |
Constructor for cloning. More... | |
virtual Space * | copy (bool share) |
Perform copying during cloning. More... | |
virtual void | print (std::ostream &os) const |
Print solution. More... | |
void | parseDIMACS (const char *f) |
Post constraints according to DIMACS file f. More... | |
![]() | |
ScriptBase (void) | |
Default constructor. More... | |
ScriptBase (bool share, ScriptBase &e) | |
Constructor used for cloning. More... | |
virtual void | compare (const Space &, std::ostream &os) const |
Compare with s. More... | |
Additional Inherited Members | |
![]() | |
static std::ostream & | select_ostream (const char *name, std::ofstream &ofs) |
Choose output stream according to name. More... | |
template<class Script , template< class > class Engine, class Options > | |
static void | run (const Options &opt, Script *s=NULL) |
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.
|
inline |
|
inline |
|
inlinevirtual |
|
inlinevirtual |
Print solution.
Reimplemented from Gecode::Driver::ScriptBase< BaseSpace >.
|
inline |