JigSAT: Better preproc + remove panics on cnf with <3 clauses

JigSAT/src/decision.rs

@@ -272,6 +272,10 @@ impl Heap {
     // Requires a new to have been created with n or larger before
     // TODO: Add support for turning off decision variables (eliminating variables entirely)
     pub(crate) fn build(&mut self, n: usize) {
+        if n == 0 {
+            return;
+        }
+
         for e in &self.heap {
             self.indices[*e] = INVALID;
         }
@@ -282,6 +286,10 @@ impl Heap {
             self.heap.push(i);
         }
 
+        if n == 1 {
+            return;
+        }
+
         let mut i = self.len() / 2 - 1;
         loop {
             self.percolate_down(i);

JigSAT/src/lit.rs

@@ -2,7 +2,7 @@ use ::std::ops;
 
 use crate::assignments::*;
 
-#[derive(Clone, Copy, Eq, PartialEq)]
+#[derive(Clone, Copy, Eq, PartialEq, PartialOrd, Ord)]
 pub struct Lit {
     code: u32,
 }

JigSAT/src/parser.rs

@@ -32,15 +32,17 @@ pub fn parse_cnf(infile: &str) -> Result<(Clauses, usize), String> {
     let mut curr_clause = vec![];
     let mut line_cntr = 0;
     let mut max_literal: usize = 0;
+    let mut seen = HashSet::new();
+    let mut tautology = false;
     if let Ok(lines) = read_lines(infile) {
         for line in lines {
             line_cntr += 1;
             if let Ok(line) = line {
                 let split = line.split(' ').filter(|e| e != &"").collect::<Vec<_>>();
                 if split.len() > 0 {
                     match split[0].chars().next().unwrap() {
-                        'c' => {}
-                        'p' => match split[2].parse::<usize>() {
+                        'c' => {},
+                        'p' => {/*match split[2].parse::<usize>() {
                             Ok(n) => {
                                 if num_lits_set {
                                     return Err("Error in input file - multiple p lines".to_string());
@@ -51,18 +53,24 @@ pub fn parse_cnf(infile: &str) -> Result<(Clauses, usize), String> {
                             Err(_) => {
                                 return Err("Error in input file".to_string());
                             }
+                            */
                         },
                         '%' => {
                             break;
                         } // The Satlib files follow this convention
                         _ => {
-                            let mut seen = HashSet::new();
                             for e in split {
                                 match e.parse::<i32>() {
                                     Ok(n) => {
                                         if n == 0 {
-                                            out_clauses.push(curr_clause);
+                                            if !tautology {
+                                                out_clauses.push(curr_clause);
+                                            }
+                                            tautology = false;
+                                            seen = HashSet::new();
                                             curr_clause = vec![];
+                                        } else if seen.contains(&-n) {
+                                            tautology = true;
                                         } else {
                                             let n_abs = n.unsigned_abs() as usize;
                                             if n_abs > max_literal {

JigSAT/src/preprocess.rs

@@ -9,7 +9,7 @@ use log::debug;
 use std::collections::VecDeque;
 //use std::collections::BinaryHeap;
 
-use crate::{clause::*, formula::*, lit::*, solver_types::*, trail::*, decision::*};
+use crate::{clause::*, formula::*, lit::*, solver_types::*, trail::*, decision::*, watches::*, unit_prop::unit_propagate};
 
 #[derive(PartialEq)]
 pub(crate) enum SubsumptionRes {
@@ -156,7 +156,7 @@ impl Preprocess {
     // Corresponds to SimpSolver::eliminate in Glucose
     // Glucose passes turn_off_elim as true, which means that it always cleans up fully afterwards
     // We just pass Preprocess as `mut self`, to have it drop at function exit
-    pub(crate) fn preprocess(mut self, formula: &mut Formula, trail: &mut Trail, decisions: &mut impl Decisions) -> bool {
+    pub(crate) fn preprocess(mut self, formula: &mut Formula, trail: &mut Trail, decisions: &mut impl Decisions, watches: &mut Watches) -> bool {
         self.init(formula);
 
         // This should be uncommented.
@@ -173,10 +173,12 @@ impl Preprocess {
         while self.n_touched > 0 || self.bwdsub_assigns < trail.trail.len() || self.elim_heap.len() > 0 {
             self.gather_touched_clauses(formula);
 
-            if (self.subsumption_queue.len() > 0 || self.bwdsub_assigns < trail.trail.len())
-                && !self.backward_subsumption_check(formula, trail)
-            {
-                return false;
+            if self.subsumption_queue.len() > 0 || self.bwdsub_assigns < trail.trail.len() {
+                match self.backward_subsumption_check(formula, trail, watches) {
+                    Some(false) => return false,
+                    Some(true)  => {},
+                    None        => break,
+                }
             }
 
             while !self.elim_heap.is_empty() {
@@ -190,8 +192,10 @@ impl Preprocess {
 
                 // We always do elim (and therefore dont have to check if has become set by assym)
                 // !frozen[elim] &&  // We dont support frozen vars (only for assumptions -> we are not incremental)
-                if !self.eliminate_var(elim, formula, trail) {
-                    return false;
+                match self.eliminate_var(elim, formula, trail, watches) {
+                    Some(false) => return false,
+                    Some(true)  => {},
+                    None        => break,
                 }
             }
         }
@@ -201,6 +205,10 @@ impl Preprocess {
             }
         }
         formula.remove_deleted();
+
+        *watches = Watches::new(&formula);
+        watches.init_watches(&formula);
+
         true
     }
 
@@ -226,15 +234,15 @@ impl Preprocess {
 
     // Backward subsumption + backward subsumption resolution
     //bool SimpSolver::backwardSubsumptionCheck(bool v) {
-    fn backward_subsumption_check(&mut self, formula: &mut Formula, trail: &mut Trail) -> bool {
+    fn backward_subsumption_check(&mut self, formula: &mut Formula, trail: &mut Trail, watches: &mut Watches) -> Option<bool> {
         //assert(decisionLevel() == 0);
 
         while self.subsumption_queue.len() > 0 || self.bwdsub_assigns < trail.trail.len() {
             // Check top-level assignments by creating a dummy clause and placing it in the queue:
             if self.subsumption_queue.len() == 0 && self.bwdsub_assigns < trail.trail.len() {
-                debug!("sub_q.len() == 0 and bwdsub_assigns < trail.len()");
+                println!("c sub_q.len() == 0 and bwdsub_assigns < trail.len()");
                 //panic!();
-                return false;
+                return None;
                 // I dunno what is supposed to happen here.
                 // If we are not done somehow, then add a dummy clause consisting of the lit
                 // on the current index of the trail, and then enqueue that. Why?
@@ -289,13 +297,13 @@ impl Preprocess {
                             //println!("Removed");
                             //deleted_literals += 1;
 
-                            if !self.strengthen_clause(self.occurs[best][j], !l, formula, trail) {
-                                return false;
+                            if !self.strengthen_clause(self.occurs[best][j], !l, formula, trail, watches) {
+                                return Some(false);
                             }
 
                             // Did current candidate get deleted from cs? Then check candidate at index j again:
                             if l.index() == best {
-                                //println!("Best");
+                                //println!("c Best");
                             } else {
                                 j += 1;
                             }
@@ -307,12 +315,12 @@ impl Preprocess {
             }
         }
 
-        return true;
+        Some(true)
     }
 
     // What happens if we ever try to strengthen a unit?
     // I would not be surprised if we are unsound, and have to init watches + do unit prop both beforehand and during preprocessing.
-    fn strengthen_clause(&mut self, cref: usize, lit: Lit, formula: &mut Formula, trail: &mut Trail) -> bool {
+    fn strengthen_clause(&mut self, cref: usize, lit: Lit, formula: &mut Formula, trail: &mut Trail, watches: &mut Watches) -> bool {
         let c = &mut formula[cref];
         //assert(decisionLevel() == 0);
 
@@ -333,9 +341,13 @@ impl Preprocess {
             let unit_lit = c[0];
             formula.mark_clause_as_deleted(cref);
             trail.learn_unit_in_preprocessing(unit_lit, &formula);
-            // Okay maybe we have to do this.
+            let mut mock = 0;
+            return match unit_propagate(formula, trail, watches, &mut mock) {
+                Err(_) => false,
+                _ => true
+            };
+
             // return enqueue(c[0]) && propagate() == CRef_Undef
-            return true;
         } else {
             //self.subsumption_queue.push_back(cref);
             // No need to detach + attach: we are not watched, and do not use a clause arena.
@@ -354,7 +366,7 @@ impl Preprocess {
     }
 
     // v is the index of the var to be removed
-    fn eliminate_var(&mut self, v: usize, formula: &mut Formula, trail: &mut Trail) -> bool {
+    fn eliminate_var(&mut self, v: usize, formula: &mut Formula, trail: &mut Trail, watches: &mut Watches) -> Option<bool> {
         /*
         assert(!frozen[v]);
         assert(!isEliminated(v));
@@ -384,7 +396,7 @@ impl Preprocess {
                 if self.merge(&formula[pos[i]], &formula[neg[j]], v, &mut clause_size)
                     && (cnt > self.occurs[v].len() + self.grow || clause_size > self.clause_lim)
                 {
-                    return true;
+                    return Some(true);
                 }
             }
         }
@@ -425,7 +437,7 @@ impl Preprocess {
                     debug!("Resolved {} and {} to get {:?}", &formula[*p], &formula[*n], &resolvent);
 
                     if !self.add_clause(formula, resolvent) {
-                        return false;
+                        return Some(false);
                     }
                 }
             }
@@ -443,7 +455,7 @@ impl Preprocess {
         //if(watches[mkLit(v)].size() == 0) watches[mkLit(v)].clear(true);
         //if(watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
 
-        return self.backward_subsumption_check(formula, trail);
+        return self.backward_subsumption_check(formula, trail, watches);
     }
 
     // v is the index of the literal which we are trying to eliminate

JigSAT/src/solver.rs

@@ -185,7 +185,7 @@ impl Solver {
         &mut self, formula: &mut Formula, decisions: &mut impl Decisions, trail: &mut Trail, watches: &mut Watches,
         target_phase: &mut TargetPhase,
     ) -> ConflictResult {
-        match unit_propagate(formula, trail, watches, self) {
+        match unit_propagate(formula, trail, watches, &mut self.ticks) {
             Ok(_) => ConflictResult::Ok,
             Err(cref) => {
                 self.num_conflicts += 1;
@@ -303,34 +303,28 @@ impl Solver {
 }
 
 pub fn solver(mut formula: Formula) -> SatResult {
-    /*
-    // TODO: Rewrite the way the formula is built
-    match formula.check_formula_invariant() {
-        SatResult::Unknown => {}
-        o => return o,
-    }
-    */
     let mut trail = Trail::new(&formula, Assignments::new(&formula));
 
-    let mut decisions: VSIDS = Decisions::new(&formula);
-    Preprocess::new().preprocess(&mut formula, &mut trail, &mut decisions);
-    debug!("done with preproc");
-    debug!("{:?}", &trail.trail);
-
     match trail.learn_units(&mut formula) {
         Some(_) => {
-            debug!("UNSAT due to learn_units");
+            println!("c UNSAT due to learn_units");
             return SatResult::Unsat;
         }
         None => {}
     }
-    // Not sure if this is really needed.
-    if formula.len() == 0 {
-        return SatResult::Sat(Vec::new());
-    }
 
     let mut watches = Watches::new(&formula);
     watches.init_watches(&formula);
+
+    let mut decisions: VSIDS = Decisions::new(&formula);
+
+    if !Preprocess::new().preprocess(&mut formula, &mut trail, &mut decisions, &mut watches) {
+        println!("c UNSAT by preprocess");
+        return SatResult::Unsat;
+    }
+    debug!("done with preproc");
+    debug!("{:?}", &trail.trail);
+
     let target_phase = TargetPhase::new(formula.num_vars);
     let solver = Solver::new(&formula);
 

JigSAT/src/trail.rs

@@ -164,8 +164,8 @@ impl Trail {
 
 impl Trail {
     #[inline]
-    pub(crate) fn learn_unit_in_preprocessing(&mut self, lit: Lit, f: &Formula) {
+    pub(crate) fn learn_unit_in_preprocessing(&mut self, lit: Lit, formula: &Formula) {
         debug!("Learned unit: {} in preproc", lit);
-        self.enq_assignment(lit, f, UNIT);
+        self.enq_assignment(lit, formula, UNIT);
     }
 }

JigSAT/src/unit_prop.rs

@@ -29,7 +29,7 @@ fn swap(f: &mut Formula, _trail: &Trail, _watches: &Watches, cref: usize, j: usi
 // The solver is included so that we can update ticks.
 #[inline]
 fn unit_prop_do_outer(
-    formula: &mut Formula, trail: &mut Trail, watches: &mut Watches, cref: usize, lit: Lit, j: usize, solver: &mut Solver,
+    formula: &mut Formula, trail: &mut Trail, watches: &mut Watches, cref: usize, lit: Lit, j: usize, ticks: &mut usize,
 ) -> Result<bool, usize> {
     let clause = &formula[cref];
 
@@ -56,7 +56,7 @@ fn unit_prop_do_outer(
         }
         k += 1;
     }
-    solver.ticks += 1;
+    *ticks += 1;
     if other_lit.lit_unsat(&trail.assignments) {
         return Err(cref);
     }
@@ -72,7 +72,7 @@ fn unit_prop_do_outer(
 
 #[inline]
 fn unit_prop_current_level(
-    formula: &mut Formula, trail: &mut Trail, watches: &mut Watches, lit: Lit, solver: &mut Solver,
+    formula: &mut Formula, trail: &mut Trail, watches: &mut Watches, lit: Lit, ticks: &mut usize,
 ) -> Result<(), usize> {
     let mut j = 0;
     let watchidx = lit.to_watchidx();
@@ -82,7 +82,7 @@ fn unit_prop_current_level(
             j += 1;
         } else {
             let cref = curr_watch.cref;
-            match unit_prop_do_outer(formula, trail, watches, cref, lit, j, solver) {
+            match unit_prop_do_outer(formula, trail, watches, cref, lit, j, ticks) {
                 Ok(true) => {
                     j += 1;
                 }
@@ -98,14 +98,15 @@ fn unit_prop_current_level(
 
 #[inline]
 pub(crate) fn unit_propagate(
-    formula: &mut Formula, trail: &mut Trail, watches: &mut Watches, solver: &mut Solver,
+    formula: &mut Formula, trail: &mut Trail, watches: &mut Watches, ticks: &mut usize,
 ) -> Result<(), usize> {
     let mut i = trail.curr_i;
     while i < trail.trail.len() {
         let lit = trail.trail[i];
-        match unit_prop_current_level(formula, trail, watches, lit, solver) {
+        match unit_prop_current_level(formula, trail, watches, lit, ticks) {
             Ok(_) => {}
             Err(cref) => {
+                println!("c err");
                 return Err(cref);
             }
         }