stalmarck 0.3.0

A crate implementing Stålmarck's method for efficiently proving propositional logic formulas and verifying logical validity.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57

//! Stålmarck's proof procedure for propositional logic.
//!
//! The crate decides satisfiability and validity of propositional formulas
//! with the Dilemma proof system of Sheeran and Stålmarck (FMCAD '98):
//!
//! 1. The formula is decomposed into *triples* `x ↔ (a ∧ b)` and
//!    `x ↔ (a ↔ b)` over literals ([`Triples`]).
//! 2. Equivalences between literals are kept in a *formula relation* and
//!    extended by the simple rules of each triple until nothing changes
//!    (0-saturation).
//! 3. The *Dilemma rule* branches on a node being ⊥ or ⊤, saturates both
//!    branches, and keeps what the two have in common. Repeating this up to
//!    nesting depth `k` is k-saturation.
//!
//! A formula is unsatisfiable when the relation becomes contradictory, and
//! satisfiable when all variables are determined and the resulting
//! assignment checks out. Otherwise the answer is *unknown* at the chosen
//! depth: the procedure is complete only when `k` is at least the number of
//! variables.
//!
//! ```
//! use stalmarck::{Formula, SatResult, Solver};
//!
//! let (p, q) = (Formula::var("p"), Formula::var("q"));
//! let f = (p.clone() | q.clone()) & !p & !q;
//! assert_eq!(Solver::default().check_sat(&f).result, SatResult::Unsat);
//! ```
//!
//! The procedure follows the project's formal specification
//! (`docs/formal-specification.md` in the repository). This release is the
//! sequential pure-Rust reference implementation.

#![forbid(unsafe_code)]
#![warn(missing_docs)]

mod cnf;
mod formula;
pub mod generate;
pub mod oracle;
mod parse;
mod relation;
mod rules;
mod saturate;
#[cfg(feature = "scryer")]
pub mod scryer;
mod solver;
mod triples;

pub use cnf::Cnf;
pub use formula::Formula;
pub use parse::ParseError;
pub use relation::CanonicalRelation;
pub use saturate::{BranchState, Stats};
pub use solver::{
    Config, Model, ProofResult, Report, SatResult, Solver, Timing, Unknown,
};
pub use triples::{Lit, Triple, TripleKind, Triples};