Development

data/tiny-opt.opb

@@ -1,6 +1,7 @@
+* #variable= 4 #constraint= 3
 * A handwritten OPB sat instance for basic testing
-min: 1 x0 2 x1;
-min: 2 x2 -3 ~x3;
-5 x0 -3 x1 >= 4;
-5 x2 -3 x3 >= 2;
-5 ~x3 >= 4;
+min: 1 x1 2 x2;
+min: 2 x3 -3 ~x4;
+5 x1 -3 x2 >= 4;
+5 x3 -3 x4 >= 2;
+5 ~x4 >= 4;

data/tiny-sat.opb

@@ -1,4 +1,5 @@
+* #variable= 4 #constraint= 3
 * A handwritten OPB sat instance for basic testing
-5 x0 -3 x1 >= 4;
-5 x2 -3 x3 >= 2;
-5 ~x3 >= 4;
+5 x1 -3 x2 >= 4;
+5 x3 -3 x4 >= 2;
+5 ~x4 >= 4;

data/tiny-unsat.opb

@@ -1,5 +1,6 @@
+* #variable= 4 #constraint= 4
 * A handwritten OPB sat instance for basic testing
-5 x0 -3 x1 >= 4;
-5 x2 -3 x3 >= 2;
-5 ~x3 >= 4;
-3 ~x0 >= 2;
+5 x1 -3 x2 >= 4;
+5 x3 -3 x4 >= 2;
+5 ~x4 >= 4;
+3 ~x1 >= 2;

rustsat/src/encodings/card/dbtotalizer.rs

@@ -51,6 +51,15 @@ pub struct DbTotalizer {
 }
 
 impl DbTotalizer {
+    #[cfg(feature = "internals")]
+    fn from_raw(root: NodeId, db: TotDb) -> Self {
+        Self {
+            root: Some(root),
+            db,
+            ..Default::default()
+        }
+    }
+
     fn extend_tree(&mut self) {
         if self.lit_buffer.is_empty() {
             return;

rustsat/src/encodings/nodedb.rs

@@ -229,7 +229,7 @@ impl NodeCon {
 
     #[inline]
     pub fn offset(&self) -> usize {
-        self.offset.into()
+        self.offset
     }
 
     #[inline]
@@ -451,6 +451,50 @@ pub trait NodeById: IndexMut<NodeId, Output = Self::Node> {
 
         NodeCon::full(self.insert(Self::Node::internal(lcon, rcon, self)))
     }
+
+    /// Merges the given connections according to the following strategy: sort
+    /// the connections by multiplier, then merge connections with equal
+    /// multiplier, then merge resulting connections with
+    /// [`NodeById::merge_balanced`].
+    #[cfg(feature = "internals")]
+    fn merge_thorough(&mut self, cons: &mut [NodeCon]) -> NodeCon
+    where
+        Self: Sized,
+    {
+        debug_assert!(!cons.is_empty());
+        cons.sort_unstable_by_key(|con| con.multiplier());
+
+        // Detect sequences of connections of equal weight and merge them
+        let mut seg_begin = 0;
+        let mut seg_end = 0;
+        let mut merged_cons = vec![];
+        loop {
+            seg_end += 1;
+            if seg_end < cons.len() && cons[seg_end].multiplier() == cons[seg_begin].multiplier() {
+                continue;
+            }
+            if seg_end > seg_begin + 1 {
+                // merge lits of equal weight
+                let mut seg: Vec<_> = cons[seg_begin..seg_end]
+                    .iter()
+                    .map(|&con| con.reweight(1))
+                    .collect();
+                seg.sort_unstable_by_key(|&con| self.con_len(con));
+                let con = self.merge_balanced(&seg);
+                debug_assert_eq!(con.multiplier(), 1);
+                merged_cons.push(con.reweight(cons[seg_begin].multiplier()));
+            } else {
+                merged_cons.push(cons[seg_begin])
+            }
+            seg_begin = seg_end;
+            if seg_end >= cons.len() {
+                break;
+            }
+        }
+
+        merged_cons.sort_unstable_by_key(|&con| self.con_len(con));
+        self.merge_balanced(&merged_cons)
+    }
 }
 
 #[cfg(test)]

rustsat/src/encodings/pb/dbgte.rs

@@ -43,8 +43,6 @@ pub struct DbGte {
     /// Maximum weight of a leaf, needed for computing how much more than
     /// `max_rhs` to encode
     max_leaf_weight: usize,
-    /// Sum of all input weight
-    weight_sum: usize,
     /// The number of variables in the totalizer
     n_vars: u32,
     /// The number of clauses in the totalizer
@@ -54,6 +52,16 @@ pub struct DbGte {
 }
 
 impl DbGte {
+    #[cfg(feature = "internals")]
+    fn from_raw(root: NodeCon, db: TotDb, max_leaf_weight: usize) -> Self {
+        Self {
+            root: Some(root),
+            max_leaf_weight,
+            db,
+            ..Default::default()
+        }
+    }
+
     fn extend_tree(&mut self, max_weight: usize) {
         if !self.lit_buffer.is_empty() {
             let mut new_lits: Vec<(Lit, usize)> = self
@@ -110,7 +118,12 @@ impl DbGte {
 
 impl Encode for DbGte {
     fn weight_sum(&self) -> usize {
-        self.weight_sum
+        self.lit_buffer.iter().fold(0, |sum, (_, w)| sum + w)
+            + if let Some(root) = self.root {
+                root.map(self.db[root.id].max_val())
+            } else {
+                0
+            }
     }
 
     fn next_higher(&self, val: usize) -> usize {
@@ -159,7 +172,7 @@ impl BoundUpper for DbGte {
     }
 
     fn enforce_ub(&self, ub: usize) -> Result<Vec<Lit>, Error> {
-        if ub >= self.weight_sum {
+        if ub >= self.weight_sum() {
             return Ok(vec![]);
         }
 
@@ -252,10 +265,8 @@ impl EncodeStats for DbGte {
 
 impl From<RsHashMap<Lit, usize>> for DbGte {
     fn from(lits: RsHashMap<Lit, usize>) -> Self {
-        let weight_sum = lits.iter().fold(0, |sum, (_, w)| sum + *w);
         Self {
             lit_buffer: lits,
-            weight_sum,
             ..Default::default()
         }
     }
@@ -271,7 +282,6 @@ impl FromIterator<(Lit, usize)> for DbGte {
 impl Extend<(Lit, usize)> for DbGte {
     fn extend<T: IntoIterator<Item = (Lit, usize)>>(&mut self, iter: T) {
         iter.into_iter().for_each(|(l, w)| {
-            self.weight_sum += w;
             // Insert into buffer to be added to tree
             match self.lit_buffer.get_mut(&l) {
                 Some(old_w) => *old_w += w,

rustsat/src/instances/fio/opb.rs

@@ -68,7 +68,7 @@ impl Default for Options {
     /// Default options following the OPB specification
     fn default() -> Self {
         Self {
-            first_var_idx: 0,
+            first_var_idx: 1,
             no_negated_lits: true,
         }
     }
@@ -367,6 +367,12 @@ where
     W: Write,
     VM: ManageVars,
 {
+    writeln!(
+        writer,
+        "* #variable = {} #constraint= {}",
+        inst.var_manager.n_used(),
+        inst.n_clauses() + inst.cards.len() + inst.pbs.len()
+    )?;
     writeln!(writer, "* OPB file written by RustSAT")?;
     if let Some(max_var) = inst.var_manager.max_var() {
         writeln!(writer, "* maximum variable: {}", max_var)?;
@@ -403,6 +409,12 @@ where
     let pbs = constrs.pbs;
     let mut vm = constrs.var_manager;
     let (hardened, softs) = obj.as_soft_lits(&mut vm);
+    writeln!(
+        writer,
+        "* #variable = {} #constraint= {}",
+        vm.n_used(),
+        cnf.len() + cards.len() + pbs.len()
+    )?;
     writeln!(writer, "* OPB file written by RustSAT")?;
     if let Some(max_var) = vm.max_var() {
         writeln!(writer, "* maximum variable: {}", max_var)?;
@@ -449,6 +461,12 @@ where
         .into_iter()
         .map(|o| o.as_soft_lits(&mut vm))
         .unzip::<_, _, Vec<_>, Vec<_>>();
+    writeln!(
+        writer,
+        "* #variable = {} #constraint= {}",
+        vm.n_used(),
+        cnf.len() + cards.len() + pbs.len()
+    )?;
     writeln!(writer, "* OPB file written by RustSAT")?;
     if let Some(max_var) = vm.max_var() {
         writeln!(writer, "* maximum variable: {}", max_var)?;
@@ -706,21 +724,21 @@ mod test {
     fn parse_variable() {
         assert_eq!(
             variable("x5 test", Options::default()),
-            Ok((" test", var![5]))
+            Ok((" test", var![4]))
         );
         assert_eq!(
             variable(
                 "x5 test",
                 Options {
-                    first_var_idx: 1,
+                    first_var_idx: 0,
                     no_negated_lits: true
                 }
             ),
-            Ok((" test", var![4]))
+            Ok((" test", var![5]))
         );
         assert_eq!(
             variable("x2 test", Options::default()),
-            Ok((" test", var![2]))
+            Ok((" test", var![1]))
         );
         assert_eq!(
             variable(" test\n", Options::default()),
@@ -732,19 +750,19 @@ mod test {
     fn parse_literal() {
         assert_eq!(
             literal("x5 test", Options::default()),
-            Ok((" test", lit![5]))
+            Ok((" test", lit![4]))
         );
         assert_eq!(
             literal("x2 test", Options::default()),
-            Ok((" test", lit![2]))
+            Ok((" test", lit![1]))
         );
         assert_eq!(
             literal("~x5 test", Options::default()),
-            Ok((" test", !lit![5]))
+            Ok((" test", !lit![4]))
         );
         assert_eq!(
             literal("~x2 test", Options::default()),
-            Ok((" test", !lit![2]))
+            Ok((" test", !lit![1]))
         );
     }
 
@@ -768,27 +786,27 @@ mod test {
     fn parse_weighted_literal() {
         assert_eq!(
             weighted_literal("5 x1 test", Options::default()),
-            Ok(("test", (lit![1], 5)))
+            Ok(("test", (lit![0], 5)))
         );
         assert_eq!(
             weighted_literal("-5  x1 test", Options::default()),
-            Ok(("test", (lit![1], -5)))
+            Ok(("test", (lit![0], -5)))
         );
         assert_eq!(
             weighted_literal("5 ~x1  test", Options::default()),
-            Ok(("test", (!lit![1], 5)))
+            Ok(("test", (!lit![0], 5)))
         );
         assert_eq!(
             weighted_literal("-5 ~x1 test", Options::default()),
-            Ok(("test", (!lit![1], -5)))
+            Ok(("test", (!lit![0], -5)))
         );
     }
 
     #[test]
     fn parse_weighted_lit_sum() {
         assert_eq!(
             weighted_lit_sum("5  x1    -3 ~x2  test", Options::default()),
-            Ok(("test", vec![(lit![1], 5), (!lit![2], -3)]))
+            Ok(("test", vec![(lit![0], 5), (!lit![1], -3)]))
         );
     }
 
@@ -807,7 +825,7 @@ mod test {
                 PBConstraint::UB(constr) => {
                     assert_eq!(rest, "");
                     let (lits, b) = constr.decompose();
-                    let should_be_lits = vec![(lit![1], 3), (lit![2], 2)];
+                    let should_be_lits = vec![(lit![0], 3), (lit![1], 2)];
                     assert_eq!(lits, should_be_lits);
                     assert_eq!(b, 6);
                 }
@@ -825,8 +843,8 @@ mod test {
             Ok((rest, obj)) => {
                 assert_eq!(rest, "");
                 let mut should_be_obj = Objective::new();
-                should_be_obj.increase_soft_lit_int(3, lit![1]);
-                should_be_obj.increase_soft_lit_int(-2, !lit![2]);
+                should_be_obj.increase_soft_lit_int(3, lit![0]);
+                should_be_obj.increase_soft_lit_int(-2, !lit![1]);
                 assert_eq!(obj, should_be_obj);
             }
             Err(_) => panic!(),
@@ -861,7 +879,7 @@ mod test {
             opb_data("* test\n", Options::default()),
             Ok(("", OpbData::Cmt(String::from("* test\n"))))
         );
-        let lits = vec![(lit![1], 3), (!lit![2], -2)];
+        let lits = vec![(lit![0], 3), (!lit![1], -2)];
         let should_be_constr = PBConstraint::new_ub(lits, 4);
         assert_eq!(
             opb_data("3 x1 -2 ~x2 <= 4;\n", Options::default()),
@@ -873,20 +891,20 @@ mod test {
             obj.increase_soft_lit_int(-3, lit![0]);
             obj.increase_soft_lit_int(4, lit![1]);
             assert_eq!(
-                opb_data("min: -3 x0 4 x1;", Options::default()),
+                opb_data("min: -3 x1 4 x2;", Options::default()),
                 Ok(("", OpbData::Obj(obj)))
             );
             assert_eq!(
-                opb_data("min: x0;", Options::default()),
-                Err(nom::Err::Error(NomError::new("x0;", ErrorKind::Eof)))
+                opb_data("min: x1;", Options::default()),
+                Err(nom::Err::Error(NomError::new("x1;", ErrorKind::Eof)))
             );
         }
     }
 
     #[cfg(feature = "optimization")]
     #[test]
     fn multi_opb_data() {
-        let data = "* test\n5 x0 -3 x1 >= 4;\nmin: 1 x0;";
+        let data = "* test\n5 x1 -3 x2 >= 4;\nmin: 1 x1;";
         let reader = Cursor::new(data);
         let reader = BufReader::new(reader);
         match parse_opb_data(reader, Options::default()) {
@@ -906,12 +924,12 @@ mod test {
             }
             Err(_) => panic!(),
         }
-        let data = "* test\n5 x0 -3 x1 >= 4;\nmin: x0;";
+        let data = "* test\n5 x1 -3 x2 >= 4;\nmin: x1;";
         let reader = Cursor::new(data);
         let reader = BufReader::new(reader);
         assert_eq!(
             parse_opb_data(reader, Options::default()),
-            Err(Error::InvalidLine(String::from("min: x0;")))
+            Err(Error::InvalidLine(String::from("min: x1;")))
         );
     }
 

tools/src/bin/cnf2opb.rs

@@ -14,7 +14,7 @@ struct Args {
     /// The OPB output path. Writes to `stdout` if not given.
     out_path: Option<PathBuf>,
     /// The index in the OPB file to treat as the lowest variable
-    #[arg(long, default_value_t = 0)]
+    #[arg(long, default_value_t = 1)]
     first_var_idx: u32,
     /// Avoid negated literals in the OPB file by transforming constraints
     #[arg(long)]

tools/src/bin/gbmosplit.rs

@@ -346,7 +346,7 @@ fn gcd(mut a: usize, mut b: usize) -> usize {
 }
 
 fn get_sums_pot_splits_gcds(
-    sorted_clauses: &Vec<(Clause, usize)>,
+    sorted_clauses: &[(Clause, usize)],
 ) -> (Vec<usize>, Vec<usize>, Vec<usize>) {
     let mut sums = vec![];
     let mut pot_split_ends = vec![];