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 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
//! Internal proof format for the Varisat SAT solver. use varisat_formula::Lit; pub mod binary_format; mod vli_enc; // Integer type used to store a hash of a clause. pub type ClauseHash = u64; /// Hash a single literal. /// /// Multiple literals can be combined with xor, as done in [`clause_hash`]. pub fn lit_hash(lit: Lit) -> ClauseHash { // Constant based on the golden ratio provides good mixing for the resulting upper bits (!(lit.code() as u64)).wrapping_mul(0x61c8864680b583ebu64) } /// A fast hash function for clauses (or other *sets* of literals). /// /// This hash function interprets the given slice as a set and will not change when the input is /// permuted. It does not handle duplicated items. pub fn clause_hash(lits: &[Lit]) -> ClauseHash { let mut hash = 0; for &lit in lits { hash ^= lit_hash(lit); } hash } /// Justifications for a simple clause deletion. #[derive(Copy, Clone, PartialEq, Eq, Debug)] pub enum DeleteClauseProof { /// The clause is known to be redundant. Redundant, /// The clause is irred and subsumed by the clause added in the previous step. Simplified, /// The clause contains a true literal. /// /// Also used to justify deletion of tautological clauses. Satisfied, } /// A single proof step. /// /// Represents a mutation of the current formula and a justification for the mutation's validity. #[derive(Copy, Clone, Debug)] pub enum ProofStep<'a> { /// Add a new input clause. /// /// This is only emitted for clauses added incrementally after an initial solve call. AddClause { clause: &'a [Lit] }, /// Add a clause that is an asymmetric tautoligy (AT). /// /// Assuming the negation of the clause's literals leads to a unit propagation conflict. /// /// The second slice contains the hashes of all clauses involved in the resulting conflict. The /// order of hashes is the order in which the clauses propagate when all literals of the clause /// are set false. /// /// When generating DRAT proofs the second slice is ignored and may be empty. AtClause { redundant: bool, clause: &'a [Lit], propagation_hashes: &'a [ClauseHash], }, /// Unit clauses found by top-level unit-propagation. /// /// Pairs of unit clauses and the original clause that became unit. Clauses are in chronological /// order. This is equivalent to multiple `AtClause` steps where the clause is unit and the /// propagation_hashes field contains just one hash, with the difference that this is not output /// for DRAT proofs. /// /// Ignored when generating DRAT proofs. UnitClauses(&'a [(Lit, ClauseHash)]), /// Delete a clause consisting of the given literals. DeleteClause { clause: &'a [Lit], proof: DeleteClauseProof, }, /// Change the number of clause hash bits used ChangeHashBits(u32), /// A (partial) assignment that satisfies all clauses and assumptions. Model(&'a [Lit]), /// Change the active set of assumptions. /// /// This is checked against future model or failed assumptions steps. Assumptions(&'a [Lit]), /// A subset of the assumptions that make the formula unsat. FailedAssumptions { failed_core: &'a [Lit], propagation_hashes: &'a [ClauseHash], }, /// Signals the end of a proof. /// /// A varisat proof must end with this command or else the checker will complain about an /// incomplete proof. End, }