From cd81b697a05f8a51c5c9c7ae483bc41a0c991263 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Tue, 25 Nov 2025 16:23:48 +0100 Subject: [PATCH] fix(sat): A clause violated at root level could be forgotten on a subsequent call of the solver. This caused a potential bug where calling the solver multiple time on a trivially UNSAT instance could eventually result in a SAT result. --- solver/src/reasoners/sat/clauses/mod.rs | 5 +++++ solver/src/reasoners/sat/sat_solver.rs | 3 +++ 2 files changed, 8 insertions(+) diff --git a/solver/src/reasoners/sat/clauses/mod.rs b/solver/src/reasoners/sat/clauses/mod.rs index 95d77e24..c5df694d 100644 --- a/solver/src/reasoners/sat/clauses/mod.rs +++ b/solver/src/reasoners/sat/clauses/mod.rs @@ -44,6 +44,11 @@ impl Display for ClauseId { write!(f, "{}", usize::from(*self)) } } +impl std::fmt::Debug for ClauseId { + fn fmt(&self, f: &mut Formatter) -> Result<(), Error> { + write!(f, "{}", usize::from(*self)) + } +} #[derive(Clone)] pub struct ClauseDb { diff --git a/solver/src/reasoners/sat/sat_solver.rs b/solver/src/reasoners/sat/sat_solver.rs index eb51f6bf..0a549dcd 100644 --- a/solver/src/reasoners/sat/sat_solver.rs +++ b/solver/src/reasoners/sat/sat_solver.rs @@ -347,6 +347,9 @@ impl SatSolver { // process all clauses that have been added since last propagation while let Some(PendingClause { clause }) = self.pending_clauses.pop_front() { if let Some(conflict) = self.process_arbitrary_clause(clause, model) { + // the clause returned is violated before being properly set up. + // Add it back to the queue so that it is not forgotten if one is calling the solver again + self.pending_clauses.push_front(PendingClause { clause }); return Err(conflict); } }