Crate dimacs

The parser facility for parsing .cnf and .sat files as specified in the DIMACS format specification.

The DIMACS format was specified for the DIMACS SAT solver competitions as input file format. Many other DIMACS file formats exist for other competitions, however, this crate currently only supports the formats that are relevant for SAT solvers.

In .cnf the entire SAT formula is encoded as a conjunction of disjunctions and so mainly stores a list of clauses consisting of literals.

The .sat format is slightly more difficult as the formula can be of a different shape and thus a .sat file internally looks similar to a Lisp file.

Structs

Clause

Represents a clause instance within a .cnf file.

Extensions

Possible extensions for .sat file SAT instances.

Lit

Represents a literal within clauses of formulas of a SAT instance.

Loc

Represents a source line and column of an error. Used to provide the user of this parser facility with necesary information to debug their input files formats.

ParseError

Represents an error that occured while parsing.

Var

Represents a variable within a SAT instance.

Enums

ErrorKind

Different kinds of errors that may occure while parsing.

Formula

Represents the structure of formulas of .sat files.

Instance

Represents a SAT instance for .cnf or .sat files.

Sign

Represents the sign of a literal.

Functions

parse_dimacs

Parses a the given string as .cnf or .sat file as specified in DIMACS format specification.

Type Aliases

FormulaBox

An indirection to a Formula via Box.

FormulaList

An immutable list of Formulas.

Result

The result type used within this crate while parsing.