fix: complete proof when adding clause results in unsat

drcp-format/src/writer/mod.rs

@@ -74,6 +74,13 @@ impl<W: Write, Literals> ProofWriter<W, Literals> {
     }
 }
 
+impl<W: Write, Literals> ProofWriter<W, Literals> {
+    /// Get the encountered literals instance to be mutated.
+    pub fn literals_mut(&mut self) -> &mut Literals {
+        &mut self.encountered_literals
+    }
+}
+
 impl<W, Literals> ProofWriter<W, Literals>
 where
     W: Write,

pumpkin-py/examples/testing.py

@@ -0,0 +1,15 @@
+from pumpkin_py import Model, constraints, Comparator
+
+model = Model()
+
+iv = model.new_integer_variable(0,1)
+a = model.new_boolean_variable(name="a")
+b = model.new_boolean_variable(name="b")
+c = model.new_boolean_variable(name="c")
+
+model.add_constraint(constraints.Clause([a, b]))          # a \/ b
+model.add_constraint(constraints.Clause([b.negate(),c]))  # b -> c
+model.add_constraint(constraints.Clause([model.predicate_as_boolean(iv, Comparator.Equal, 1)])) # iv == 1
+model.add_implication(constraints.Equals([iv], 0), c)  # c -> iv == 0
+
+model.satisfy(proof="test")

pumpkin-py/test

@@ -0,0 +1,10 @@
+i 1 -1
+n 2 1 0 1
+i 3 1 2
+n 4 -2 0 2 3
+i 5 -2 -3
+n 6 3 0 4 5
+i 7 3 -4
+n 8 4 0 6 7
+i 9 4 5
+n 10 -5 0 8 9

pumpkin-py/test.drcp

@@ -0,0 +1,24 @@
+i 1 1 2
+i 2 4 0 -3
+i 3 4 0 -5
+i 4 4 0 -6
+i 5 4 0 -7
+n 6 -8 0 5 4 3 2 1
+i 7 9 1
+i 8 1 0 -10
+n 9 11 0 8 6 7
+i 10 9 7
+i 11 9 0 -5
+n 12 -12 0 6 11 9 10
+i 13 10 3
+n 14 -3 0 12 13
+i 15 10 5
+n 16 -5 0 12 15
+i 17 10 6
+n 18 -6 0 12 17
+i 19 7 2
+i 20 10 0 -6
+i 21 10 0 -5
+i 22 10 0 -3
+n 23 0 9 12 22 21 20 19
+c UNSAT

pumpkin-py/test.lits

@@ -0,0 +1,12 @@
+8 [q0 <= 0]
+7 [q1 == 0]
+10 [q0 == 2]
+2 [q2 == 1]
+4 [q0 == 0]
+5 [q1 == 1]
+3 [q2 == 2]
+9 [q0 == 1]
+6 [q2 == 0]
+1 [q1 == 2]
+11 [q1 <= 1]
+12 [q0 <= 1]

pumpkin-solver/Cargo.toml

@@ -18,7 +18,7 @@ rand = { version = "0.8.5", features = [ "small_rng", "alloc" ] }
 signal-hook = "0.3.17"
 once_cell = "1.19.0"
 downcast-rs = "1.2.1"
-drcp-format = { version = "0.2.0" }
+drcp-format = { path = "../drcp-format" }
 convert_case = "0.6.0"
 itertools = "0.13.0"
 flatzinc = "0.3.21"

pumpkin-solver/src/engine/conflict_analysis/conflict_analysis_context.rs

@@ -138,7 +138,7 @@ impl<'a> ConflictAnalysisContext<'a> {
         current_nogood: CurrentNogood<'_>,
         reason_store: &'a mut ReasonStore,
         propagators: &'a mut PropagatorStore,
-        proof_log: &'a mut ProofLog,
+        proof_log: &mut ProofLog,
         unit_nogood_step_ids: &HashMap<Predicate, StepId>,
     ) -> &'a [Predicate] {
         // TODO: this function could be put into the reason store

pumpkin-solver/src/engine/conflict_analysis/resolvers/resolution_resolver.rs

@@ -1,5 +1,8 @@
+use std::num::NonZero;
+
 use super::ConflictResolver;
 use crate::basic_types::moving_averages::MovingAverage;
+use crate::basic_types::HashMap;
 use crate::basic_types::PredicateId;
 use crate::basic_types::PredicateIdGenerator;
 use crate::branching::Brancher;
@@ -12,6 +15,7 @@ use crate::engine::conflict_analysis::LearnedNogood;
 use crate::engine::propagation::CurrentNogood;
 use crate::engine::Assignments;
 use crate::predicates::Predicate;
+use crate::proof::ProofLog;
 use crate::pumpkin_assert_advanced;
 use crate::pumpkin_assert_moderate;
 use crate::pumpkin_assert_simple;
@@ -75,6 +79,8 @@ impl ConflictResolver for ResolutionResolver {
             self.add_predicate_to_conflict_nogood(
                 *predicate,
                 context.assignments,
+                context.proof_log,
+                context.unit_nogood_step_ids,
                 context.brancher,
                 self.mode,
                 context.is_completing_proof,
@@ -244,6 +250,8 @@ impl ConflictResolver for ResolutionResolver {
                 self.add_predicate_to_conflict_nogood(
                     *predicate,
                     context.assignments,
+                    context.proof_log,
+                    context.unit_nogood_step_ids,
                     context.brancher,
                     self.mode,
                     context.is_completing_proof,
@@ -273,13 +281,19 @@ impl ResolutionResolver {
         self.to_process_heap.clear();
     }
 
+    #[allow(
+        clippy::too_many_arguments,
+        reason = "borrow checker complains if passing through the context"
+    )]
     fn add_predicate_to_conflict_nogood(
         &mut self,
         predicate: Predicate,
         assignments: &Assignments,
+        proof_log: &mut ProofLog,
+        unit_nogood_step_ids: &HashMap<Predicate, NonZero<u64>>,
         brancher: &mut dyn Brancher,
         mode: AnalysisMode,
-        is_logging_complete_proof: bool,
+        is_completing_proof: bool,
     ) {
         let dec_level = assignments
             .get_decision_level_for_predicate(&predicate)
@@ -290,18 +304,39 @@ impl ResolutionResolver {
                     assignments.get_upper_bound(predicate.get_domain()),
                 )
             });
-        // Ignore root level predicates.
-        if !is_logging_complete_proof && dec_level == 0 {
-            // do nothing
+
+        // Log all non-initial bounds to the proof.
+        if dec_level == 0 && !is_completing_proof {
+            if !assignments.is_initial_bound(predicate) && proof_log.is_logging_inferences() {
+                let trail_index = assignments
+                    .get_trail_position(&predicate)
+                    .expect("all predicates in reason are true");
+                let trail_entry = assignments.get_trail_entry(trail_index);
+
+                // We do indicate their usage in the proof.
+                let step_id = unit_nogood_step_ids
+                    .get(&trail_entry.predicate)
+                    .copied()
+                    .unwrap_or_else(|| {
+                        panic!(
+                            "Failed to get step id for unit clause {:?}. Available steps: {:?}",
+                            trail_entry.predicate, unit_nogood_step_ids
+                        )
+                    });
+                proof_log.add_propagation(step_id);
+            }
+
+            return;
         }
+
         // 1UIP
         // If the variables are from the current decision level then we want to potentially add
         // them to the heap, otherwise we add it to the predicates from lower-decision levels
         //
         // All-decision Learning
         // If the variables are not decisions then we want to potentially add them to the heap,
         // otherwise we add it to the decision predicates which have been discovered previously
-        else if match mode {
+        if match mode {
             AnalysisMode::OneUIP => dec_level == assignments.get_decision_level(),
             AnalysisMode::AllDecision => !assignments.is_decision_predicate(&predicate),
         } {