feat!: Monotone trait for encodings

and requiring it for solution-improving search

Author: chrjabs

src/algs/maxsat.rs

@@ -7,7 +7,7 @@
 use std::marker::PhantomData;
 
 use crate::{
-    encodings::pb,
+    encodings::{pb, Monotone},
     instances::BasicVarManager,
     solvers::{SolveIncremental, SolveStats, SolverResult},
     types::{Assignment, Lit, TernaryVal},
@@ -57,7 +57,7 @@ pub struct SolutionImprovingSearch<Solver, PbEnc> {
 impl<Solver, PbEnc> Solve for SolutionImprovingSearch<Solver, PbEnc>
 where
     Solver: SolveIncremental + SolveStats,
-    PbEnc: FromIterator<(Lit, usize)> + pb::BoundUpperIncremental,
+    PbEnc: FromIterator<(Lit, usize)> + pb::BoundUpperIncremental + Monotone,
 {
     type Solver = Solver;
 

src/encodings.rs

@@ -65,6 +65,12 @@ pub enum ConstraintEncodingError {
     OutOfMemory(#[from] crate::OutOfMemory),
 }
 
+/// Marker trait for "monotone" incremental encodings, i.e., encodings for which enforcing `sum <=
+/// k` (as hard clauses) does not conflict with enforcing `sum <= k - x` later.
+///
+/// The [`pb::DynamicPolyWatchdog`] is a notable exception to this, because of its tare variables.
+pub trait Monotone {}
+
 /// Trait for encodings that track statistics.
 pub trait EncodeStats {
     /// Gets the number of clauses in the encoding

src/encodings/card/totalizer.rs

@@ -8,7 +8,7 @@ use std::{cmp, ops::RangeBounds};
 use crate::{
     encodings::{
         nodedb::{NodeById, NodeCon, NodeId, NodeLike},
-        totdb, CollectClauses, EncodeStats, EnforceError, NotEncoded,
+        totdb, CollectClauses, EncodeStats, EnforceError, Monotone, NotEncoded,
     },
     instances::ManageVars,
     types::Lit,
@@ -335,6 +335,8 @@ impl BoundBoth for Totalizer {
 
 impl BoundBothIncremental for Totalizer {}
 
+impl Monotone for Totalizer {}
+
 impl EncodeStats for Totalizer {
     fn n_clauses(&self) -> usize {
         self.n_clauses

src/encodings/pb/adder.rs

@@ -19,7 +19,7 @@ use std::collections::VecDeque;
 
 use crate::{
     clause,
-    encodings::{CollectClauses, EncodeStats, EnforceError},
+    encodings::{CollectClauses, EncodeStats, EnforceError, Monotone},
     instances::ManageVars,
     types::{Clause, Lit, RsHashMap},
     OutOfMemory,
@@ -420,6 +420,8 @@ impl EncodeIncremental for BinaryAdder {
     }
 }
 
+impl Monotone for BinaryAdder {}
+
 impl EncodeStats for BinaryAdder {
     fn n_clauses(&self) -> usize {
         self.n_clauses

src/encodings/pb/gte.rs

@@ -8,7 +8,7 @@ use std::ops::RangeBounds;
 use crate::{
     encodings::{
         nodedb::{NodeById, NodeCon, NodeLike},
-        totdb, CollectClauses, EncodeStats, EnforceError,
+        totdb, CollectClauses, EncodeStats, EnforceError, Monotone,
     },
     instances::ManageVars,
     types::{Lit, RsHashMap},
@@ -326,6 +326,8 @@ impl BoundUpperIncremental for GeneralizedTotalizer {
     }
 }
 
+impl Monotone for GeneralizedTotalizer {}
+
 impl EncodeStats for GeneralizedTotalizer {
     fn n_clauses(&self) -> usize {
         self.n_clauses

tests/maxsat.rs

@@ -1,7 +1,7 @@
 use rustsat::{algs::maxsat, encodings::pb, instances::OptInstance};
 
 #[test]
-fn sis_small() {
+fn sis_small_gte() {
     type Alg =
         maxsat::SolutionImprovingSearch<rustsat_minisat::core::Minisat, pb::GeneralizedTotalizer>;
     let inst: OptInstance = OptInstance::from_dimacs_path("./data/inc-sis-fails.wcnf").unwrap();
@@ -11,7 +11,7 @@ fn sis_small() {
 }
 
 #[test]
-fn sis() {
+fn sis_gte() {
     type Alg =
         maxsat::SolutionImprovingSearch<rustsat_minisat::core::Minisat, pb::GeneralizedTotalizer>;
     let inst: OptInstance =
@@ -20,3 +20,22 @@ fn sis() {
     dbg!(&sol);
     assert!(matches!(sol, Some((_, 61169))));
 }
+
+#[test]
+fn sis_small_adder() {
+    type Alg = maxsat::SolutionImprovingSearch<rustsat_minisat::core::Minisat, pb::BinaryAdder>;
+    let inst: OptInstance = OptInstance::from_dimacs_path("./data/inc-sis-fails.wcnf").unwrap();
+    let sol = inst.solve_maxsat::<Alg>();
+    dbg!(&sol);
+    assert!(matches!(sol, Some((_, 8632))));
+}
+
+#[test]
+fn sis_adder() {
+    type Alg = maxsat::SolutionImprovingSearch<rustsat_minisat::core::Minisat, pb::BinaryAdder>;
+    let inst: OptInstance =
+        OptInstance::from_dimacs_path("./data/auctions_wt-cat_sched_60_70_0003.txt.wcnf").unwrap();
+    let sol = inst.solve_maxsat::<Alg>();
+    dbg!(&sol);
+    assert!(matches!(sol, Some((_, 61169))));
+}