CNF Parser

Continuous Integration	Documentation	Crates.io

An efficient and customizable parser for the .cnf (Conjunctive Normal Form) file format used by SAT solvers.

• No unsafe Rust!
• No dependencies!
• No heap allocations while parsing!
• no_std compatible!

Usage

For parsing use the parse_cnf function. It requires some input source that is expected to be .cnf encoded as well as a &mut to a customizable output. This output needs to implement the Output trait and is most probably your solver or something that initializes your solver from the given .cnf input.

Example

In order to use parse_cnf you first have to define your own Output type:

#[derive(Default)]
pub struct MyOutput {
    head_clause: Vec<Literal>,
    clauses: Vec<Vec<Literal>>,
}

impl Output for MyOutput {
    type Error = &'static str;

    fn problem(
        &mut self, num_variables: u32, num_clauses: u32
    ) -> Result<(), Self::Error> {
        Ok(())
    }

    fn literal(&mut self, literal: Literal) -> Result<(), Self::Error> {
        self.head_clause.push(literal); Ok(())
    }

    fn finalize_clause(&mut self) -> Result<(), Self::Error> {
        if self.head_clause.is_empty() {
            return Err("encountered empty clause")
        }
        self.clauses.push(
            core::mem::replace(&mut self.head_clause, Vec::new())
        );
        Ok(())
    }

    fn finish(&mut self) -> Result<(), Self::Error> {
        if !self.head_clause.is_empty() {
            self.finalize_clause()?
        }
        Ok(())
    }
}

Then use parse_cnf as follows:

let my_input: &[u8] = br"
    c This is my input .cnf file with 3 variables and 2 clauses.
    p cnf 3 2
    1 -2 3 0
    1 -3 0
";
let mut my_output = MyOutput::default();
cnf_parser::parse_cnf(&mut my_input.as_ref(), &mut my_output)
    .expect("encountered invalid .cnf input");

License

Licensed under either of

• Apache license, Version 2.0, (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
• MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)

at your option.

Dual licence:

Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.