varisat_internal_proof/
lib.rs

1//! Internal proof format for the Varisat SAT solver.
2use varisat_formula::{Lit, Var};
3
4pub mod binary_format;
5
6mod vli_enc;
7
8// Integer type used to store a hash of a clause.
9pub type ClauseHash = u64;
10
11/// Hash a single literal.
12///
13/// Multiple literals can be combined with xor, as done in [`clause_hash`].
14pub fn lit_hash(lit: Lit) -> ClauseHash {
15    lit_code_hash(lit.code())
16}
17
18/// Hash a single literal from a code.
19///
20/// This doesn't require the code to correspond a valid literal.
21pub fn lit_code_hash(lit_code: usize) -> ClauseHash {
22    // Constant based on the golden ratio provides good mixing for the resulting upper bits
23    (!(lit_code as u64)).wrapping_mul(0x61c8864680b583ebu64)
24}
25
26/// A fast hash function for clauses (or other *sets* of literals).
27///
28/// This hash function interprets the given slice as a set and will not change when the input is
29/// permuted. It does not handle duplicated items.
30pub fn clause_hash(lits: &[Lit]) -> ClauseHash {
31    let mut hash = 0;
32    for &lit in lits {
33        hash ^= lit_hash(lit);
34    }
35    hash
36}
37
38/// Justifications for a simple clause deletion.
39#[derive(Copy, Clone, PartialEq, Eq, Debug)]
40pub enum DeleteClauseProof {
41    /// The clause is known to be redundant.
42    Redundant,
43    /// The clause is irred and subsumed by the clause added in the previous step.
44    Simplified,
45    /// The clause contains a true literal.
46    ///
47    /// Also used to justify deletion of tautological clauses.
48    Satisfied,
49}
50
51/// A single proof step.
52///
53/// Represents a mutation of the current formula and a justification for the mutation's validity.
54#[derive(Copy, Clone, Debug)]
55pub enum ProofStep<'a> {
56    /// Update the global to solver var mapping.
57    ///
58    /// For proof checking, the solver variable names are only used for hash computations.
59    SolverVarName { global: Var, solver: Option<Var> },
60    /// Update the global to user var mapping.
61    ///
62    /// A variable without user mapping is considered hidden by the checker. When a variable without
63    /// user mapping gets a user mapping, the sampling mode is initialized to witness.
64    ///
65    /// It's not allowed to change a variable from one user name to another when the variable is in
66    /// use.
67    ///
68    /// Clause additions and assumptions are only allowed to use variables with user mappings (and a
69    /// non-witness sampling mode).
70    UserVarName { global: Var, user: Option<Var> },
71    /// Delete a variable.
72    ///
73    /// This is only allowed for variables that are isolated and hidden.
74    DeleteVar { var: Var },
75    /// Changes the sampling mode of a variable.
76    ///
77    /// This is only used to change between Sample and Witness. Hidden is managed by adding or
78    /// removing a user var name.
79    ChangeSamplingMode { var: Var, sample: bool },
80    /// Add a new input clause.
81    ///
82    /// This is only emitted for clauses added incrementally after an initial solve call.
83    AddClause { clause: &'a [Lit] },
84    /// Add a clause that is an asymmetric tautoligy (AT).
85    ///
86    /// Assuming the negation of the clause's literals leads to a unit propagation conflict.
87    ///
88    /// The second slice contains the hashes of all clauses involved in the resulting conflict. The
89    /// order of hashes is the order in which the clauses propagate when all literals of the clause
90    /// are set false.
91    ///
92    /// When generating DRAT proofs the second slice is ignored and may be empty.
93    AtClause {
94        redundant: bool,
95        clause: &'a [Lit],
96        propagation_hashes: &'a [ClauseHash],
97    },
98    /// Unit clauses found by top-level unit-propagation.
99    ///
100    /// Pairs of unit clauses and the original clause that became unit. Clauses are in chronological
101    /// order. This is equivalent to multiple `AtClause` steps where the clause is unit and the
102    /// propagation_hashes field contains just one hash, with the difference that this is not output
103    /// for DRAT proofs.
104    ///
105    /// Ignored when generating DRAT proofs.
106    UnitClauses { units: &'a [(Lit, ClauseHash)] },
107    /// Delete a clause consisting of the given literals.
108    DeleteClause {
109        clause: &'a [Lit],
110        proof: DeleteClauseProof,
111    },
112    /// Change the number of clause hash bits used
113    ChangeHashBits { bits: u32 },
114    /// A (partial) assignment that satisfies all clauses and assumptions.
115    Model { assignment: &'a [Lit] },
116    /// Change the active set of assumptions.
117    ///
118    /// This is checked against future model or failed assumptions steps.
119    Assumptions { assumptions: &'a [Lit] },
120    /// A subset of the assumptions that make the formula unsat.
121    FailedAssumptions {
122        failed_core: &'a [Lit],
123        propagation_hashes: &'a [ClauseHash],
124    },
125    /// Signals the end of a proof.
126    ///
127    /// A varisat proof must end with this command or else the checker will complain about an
128    /// incomplete proof.
129    End,
130}
131
132impl<'a> ProofStep<'a> {
133    /// Does this proof step use clause hashes?
134    pub fn contains_hashes(&self) -> bool {
135        match self {
136            ProofStep::AtClause { .. }
137            | ProofStep::UnitClauses { .. }
138            | ProofStep::FailedAssumptions { .. } => true,
139
140            ProofStep::SolverVarName { .. }
141            | ProofStep::UserVarName { .. }
142            | ProofStep::DeleteVar { .. }
143            | ProofStep::ChangeSamplingMode { .. }
144            | ProofStep::AddClause { .. }
145            | ProofStep::DeleteClause { .. }
146            | ProofStep::ChangeHashBits { .. }
147            | ProofStep::Model { .. }
148            | ProofStep::Assumptions { .. }
149            | ProofStep::End => false,
150        }
151    }
152}
varisat_internal_proof/lib.rs

varisat_internal_proof/
lib.rs
