Crate stalmarck 

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). Solver is the sequential pure-Rust reference implementation. With the scryer feature, scryer::ScryerSolver runs Dilemma branches in embedded Scryer Prolog and gives the same results and counters.

Modules

generate

Deterministic instance generators for tests and benchmarks (PRD §36, §40). The same seed and parameters always give the same instance, for a given GENERATOR_VERSION.

oracle

Truth-table oracles, independent of the proof procedure (PRD §36).

scryer

Implementation B: Rust with embedded Scryer Prolog (feature scryer, ADR-0005).

Structs

Cnf

A formula in conjunctive normal form, as in DIMACS: variables are 1..=variables, and a literal is ±i.

Config

Solver configuration. Start from Config::default and adjust it with the with_* methods:

Lit

A literal: a node together with a polarity (SPEC-D2).

Model

An assignment of truth values to the input variables.

ParseError

A syntax error with a 1-based position.

Report

A result together with counters and the final relation.

Solver

Stålmarck’s proof procedure with a fixed configuration.

Stats

Solver counters (SPEC-Z6, SPEC-K4).

Timing

Wall-clock time spent in the solver (ADR-0008 boundaries).

Triple

A triple x ↔ (a ∘ b) with output node x and operand literals.

Triples

A formula decomposed into triples.

Enums

BranchState

How a dilemma keeps its parent state while it explores the branches (PRD §10, ADR-0004).

CanonicalRelation

The canonical form of a formula relation (SPEC-R4).

Formula

A propositional formula over named variables.

ProofResult

Answer to “is the formula valid?”.

SatResult

Answer to “is the formula satisfiable?”.

TripleKind

The two triple kinds (SPEC-D3).

Unknown

Why no definite answer was reached.