Expand description
DIMACS CNF/SAT parser based on the paper “Satisfiability Suggested Format”
The parsers perform some trivial simplifications on the CNF or the SAT
formula: CNFs with empty clauses become
Literal::FALSE, empty CNFs become
Literal::TRUE. Likewise, empty disjunctions,
conjunctions, etc., in SAT formulas are replaced by the respective constant.
Equivalence operators are replaced by XOR and negation (since
Circuits do not support equivalence). Conjunction,
disjunction, and XOR operators with just a single operand are discarded.
In addition to regular OR clauses, the CNF parser also supports XOR clauses (XCNF).
Functions§
- parse
- Parse a DIMACS CNF/SAT file