SAT Solvers in Rust

This crate contains implementations of various satisfiability solvers for the boolean satisfiability problem (SAT).

List of available solvers:

• crate::solvers::syntactic - A purely syntactic solver based on a user provided interpretation

This crate also contains some useful structs for working with propositional variables and formulas, viz:

• crate::notation::Formula - A struct for working with propositional formulas
• crate::notation::Clause - A struct for working with propositional clauses
• crate::notation::Literal - A struct for working with propositional literals (atoms)

Usage

The crate can be used as a library or as a binary. To use it as a binary, run the following command:

cargo run <CNF_FILE> <SOLVER>

OR

sat-rs <CNF_FILE> <SOLVER>