logicaffeine_proof/
proof.rs

1//! Shared proof-step vocabulary for the certified checkers.
2//!
3//! A refutation is an ordered stream of clause *additions*, each carrying a justification a
4//! tiny independent checker can replay:
5//!
6//! - [`ProofStep::Rup`] — the clause follows by reverse unit propagation (the DRAT/RUP unit).
7//! - [`ProofStep::Pr`] — the clause is **propagation-redundant** with an explicit [`Witness`]
8//!   (Heule, Kiesl & Biere, *Short Proofs Without New Variables*, CADE 2017). This is the only
9//!   form that can certify a *model-removing* addition — exactly what a symmetry-breaking
10//!   predicate is — so it is the seam through which certified symmetry breaking flows.
11//!
12//! The witness may be an explicit partial [`Witness::Assignment`] or a literal
13//! [`Witness::Substitution`] (a permutation / automorphism). The substitution form is mere
14//! sugar: against a clause `C` whose falsifying assignment is `α = ¬C`, the substitution `σ`
15//! denotes the assignment witness `ω = { ¬σ(l) : l ∈ C }` — the image of the "bad" corner of
16//! the cube under the symmetry, which is the canonical PR witness for a lex-leader SBP. The
17//! checker ([`crate::pr`]) reduces every substitution to that assignment, so there is a single
18//! well-specified propagation-redundancy criterion to trust.
19
20use crate::cdcl::{Lit, Var};
21
22/// A literal permutation that respects negation: `σ(¬l) = ¬σ(l)`. Represented by the image of
23/// each variable's positive literal, so the negation invariant holds by construction.
24#[derive(Clone, Debug, PartialEq, Eq, Hash)]
25pub struct Perm {
26    /// `pos_image[v] = σ(+v)`. The negative literal's image is its negation.
27    pos_image: Vec<Lit>,
28}
29
30impl Perm {
31    /// The identity permutation over `num_vars` variables.
32    pub fn identity(num_vars: usize) -> Perm {
33        Perm {
34            pos_image: (0..num_vars as Var).map(Lit::pos).collect(),
35        }
36    }
37
38    /// Build from the image of each positive literal: `images[v] = σ(+v)`.
39    pub fn from_images(images: Vec<Lit>) -> Perm {
40        Perm { pos_image: images }
41    }
42
43    /// Apply `σ` to a literal, respecting sign: `σ(¬l) = ¬σ(l)`.
44    pub fn apply(&self, l: Lit) -> Lit {
45        let img = self.pos_image[l.var() as usize];
46        if l.is_positive() {
47            img
48        } else {
49            img.negated()
50        }
51    }
52
53    /// Apply `σ` to every literal of a clause.
54    pub fn apply_clause(&self, clause: &[Lit]) -> Vec<Lit> {
55        clause.iter().map(|&l| self.apply(l)).collect()
56    }
57
58    /// The number of variables the permutation is defined over.
59    pub fn num_vars(&self) -> usize {
60        self.pos_image.len()
61    }
62
63    /// Whether this is the identity permutation.
64    pub fn is_identity(&self) -> bool {
65        self.pos_image
66            .iter()
67            .enumerate()
68            .all(|(v, &img)| img == Lit::pos(v as Var))
69    }
70
71    /// Extend to `nv` variables, acting as the identity on the new (higher-indexed) variables.
72    /// Used to lift a base-formula symmetry over auxiliary variables it does not touch.
73    pub fn extended(&self, nv: usize) -> Perm {
74        let mut pos_image = self.pos_image.clone();
75        for v in pos_image.len()..nv {
76            pos_image.push(Lit::pos(v as Var));
77        }
78        Perm { pos_image }
79    }
80
81    /// Compose: `(self ∘ other)(l) = self(other(l))` — apply `other` first, then `self`.
82    pub fn compose(&self, other: &Perm) -> Perm {
83        Perm {
84            pos_image: (0..self.pos_image.len() as Var)
85                .map(|v| self.apply(other.apply(Lit::pos(v))))
86                .collect(),
87        }
88    }
89}
90
91/// A redundancy witness for a [`ProofStep::Pr`] clause.
92#[derive(Clone, Debug, PartialEq, Eq)]
93pub enum Witness {
94    /// An explicit partial assignment (the set of literals it sets true) — the classic PR
95    /// witness.
96    Assignment(Vec<Lit>),
97    /// A literal permutation / automorphism. Against the clause `C` it certifies, it denotes
98    /// the assignment `ω = { ¬σ(l) : l ∈ C }`.
99    Substitution(Perm),
100}
101
102/// One step of a refutation: add a clause with the justification a checker replays, or delete a
103/// clause from the working database (the DRAT deletion that inprocessing — vivification, BVE —
104/// relies on; deletions are unchecked, only additions carry a redundancy obligation).
105#[derive(Clone, Debug, PartialEq, Eq)]
106pub enum ProofStep {
107    /// Add a clause that is RUP w.r.t. the current database.
108    Rup(Vec<Lit>),
109    /// Add a clause that is propagation-redundant w.r.t. the current database, certified by
110    /// `witness`. May remove models; preserves satisfiability.
111    Pr { clause: Vec<Lit>, witness: Witness },
112    /// Remove a clause from the working database (a sound DRAT deletion).
113    Delete(Vec<Lit>),
114}
115
116impl ProofStep {
117    /// The clause this step adds or deletes.
118    pub fn clause(&self) -> &[Lit] {
119        match self {
120            ProofStep::Rup(c) | ProofStep::Delete(c) => c,
121            ProofStep::Pr { clause, .. } => clause,
122        }
123    }
124}
125
126#[cfg(test)]
127#[path = "../../logicaffeine_tests/unit/logicaffeine_proof/proof/perm_tests.rs"]
128mod perm_tests;
logicaffeine_proof/proof.rs

logicaffeine_proof/
proof.rs
