Precise proof checking for satisfiable instances

varisat-cli/src/check.rs

@@ -4,7 +4,7 @@ use std::io;
 use clap::{App, ArgMatches, SubCommand};
 use failure::Error;
 
-use varisat::checker::{Checker, WriteLrat};
+use varisat::checker::{Checker, CheckerError, WriteLrat};
 
 use super::{banner, init_logging};
 
@@ -66,6 +66,11 @@ pub fn check_main(matches: &ArgMatches) -> Result<i32, Error> {
         Ok(()) => println!("s VERIFIED"),
         Err(err) => {
             log::error!("{}", err);
+            if let CheckerError::CheckFailed { debug_step, .. } = err {
+                if !debug_step.is_empty() {
+                    log::error!("failed step was {}", debug_step)
+                }
+            }
             println!("s NOT VERIFIED");
             return Ok(1);
         }

varisat/src/binary.rs

@@ -3,7 +3,7 @@
 use partial_ref::{partial, PartialRef};
 
 use crate::context::{AssignmentP, BinaryClausesP, Context, ProofP, SolverStateP};
-use crate::proof::{self, ProofStep};
+use crate::proof::{self, DeleteClauseProof, ProofStep};
 
 use crate::lit::Lit;
 
@@ -57,7 +57,13 @@ pub fn simplify_binary<'a>(
                     // This check avoids deleting binary clauses twice if both literals are assigned.
                     if (!lit) < other_lit {
                         let lits = [!lit, other_lit];
-                        proof::add_step(ctx.borrow(), &ProofStep::DeleteClause(&lits[..]));
+                        proof::add_step(
+                            ctx.borrow(),
+                            &ProofStep::DeleteClause {
+                                clause: &lits[..],
+                                proof: DeleteClauseProof::Satisfied,
+                            },
+                        );
                     }
                 }
             }
@@ -69,7 +75,13 @@ pub fn simplify_binary<'a>(
                 // This check avoids deleting binary clauses twice if both literals are assigned.
                 if ctx.part(ProofP).is_active() && !retain && (!lit) < other_lit {
                     let lits = [!lit, other_lit];
-                    proof::add_step(ctx.borrow(), &ProofStep::DeleteClause(&lits[..]));
+                    proof::add_step(
+                        ctx.borrow(),
+                        &ProofStep::DeleteClause {
+                            clause: &lits[..],
+                            proof: DeleteClauseProof::Satisfied,
+                        },
+                    );
                 }
 
                 retain

varisat/src/cdcl.rs

@@ -10,6 +10,7 @@ use crate::context::{
 };
 use crate::decision::make_decision;
 use crate::incremental::{enqueue_assumption, EnqueueAssumption};
+use crate::lit::Lit;
 use crate::proof::{self, ProofStep};
 use crate::prop::{backtrack, enqueue_assignment, propagate, Conflict, Reason};
 use crate::simplify::{prove_units, simplify};
@@ -39,6 +40,21 @@ pub fn conflict_step<'a>(
 
     let conflict = match conflict {
         Ok(()) => {
+            if ctx.part(ProofP).models_in_proof() {
+                let (tmp, mut ctx) = ctx.split_part_mut(TmpDataP);
+                let model = &mut tmp.lits;
+                model.clear();
+                model.extend(
+                    ctx.part(AssignmentP)
+                        .assignment()
+                        .iter()
+                        .enumerate()
+                        .flat_map(|(index, assignment)| {
+                            assignment.map(|polarity| Lit::from_index(index, !polarity))
+                        }),
+                );
+                proof::add_step(ctx.borrow(), &ProofStep::Model(&model));
+            }
             ctx.part_mut(SolverStateP).sat_state = SatState::Sat;
             return;
         }
@@ -66,6 +82,7 @@ pub fn conflict_step<'a>(
     proof::add_step(
         ctx.borrow(),
         &ProofStep::AtClause {
+            redundant: clause.len() > 2,
             clause: clause.into(),
             propagation_hashes: analyze.clause_hashes(),
         },