sat_rs/
lib.rs

1//! # SAT Solvers in Rust
2//! This crate contains implementations of various satisfiability solvers for the boolean satisfiability problem (SAT).
3//!
4//! List of available solvers:
5//! * [`crate::solvers::syntactic`] - A purely syntactic solver based on a user provided interpretation
6//!
7//! This crate also contains some useful structs for working with propositional variables and formulas, viz:
8//! * [`crate::notation::Formula`] - A struct for working with propositional formulas
9//! * [`crate::notation::Clause`] - A struct for working with propositional clauses
10//! * [`crate::notation::Literal`] - A struct for working with propositional literals (atoms)
11//!
12//! # Usage
13//! The crate can be used as a library or as a binary. To use it as a binary, run the following command:
14//! ```text
15//! cargo run <CNF_FILE> <SOLVER>
16//! ```
17//! OR
18//! ```text
19//! sat-rs <CNF_FILE> <SOLVER>
20//! ```
21pub mod notation;
22pub mod cnfparser;
23pub mod solvers;