#sat-solver #sat #format #lexer #parser #file-format #input-file


Utilities to parse files in DIMACS .cnf or .sat format which is useful for participating in the DIMACS SAT solver competitions

2 unstable releases

Uses old Rust 2015

0.2.0 Mar 28, 2017
0.1.0 Mar 5, 2017

#33 in #sat

Download history 31/week @ 2024-03-12 62/week @ 2024-03-19 33/week @ 2024-03-26 80/week @ 2024-04-02 18/week @ 2024-04-09 49/week @ 2024-04-16 34/week @ 2024-04-23 20/week @ 2024-04-30 21/week @ 2024-05-07 28/week @ 2024-05-14 31/week @ 2024-05-21 27/week @ 2024-05-28 30/week @ 2024-06-04 25/week @ 2024-06-11 25/week @ 2024-06-18 24/week @ 2024-06-25

109 downloads per month


836 lines

Build Status MIT licensed Crates.io Version Doc.rs Badge


Utilities to parse files in DIMACS .cnf or .sat SAT format which is useful in participating in the DIMACS SAT solver competition.

Basically provides the following API:

fn parse_dimacs(input: &str) -> Result<Instance> { .. }


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.