JigSAT: Add target phases

JigSAT/Cargo.toml

@@ -43,6 +43,7 @@ rpath = false
 [dependencies]
 clap = "2.33.3"
 log = "0.4"
+rand = "0.8.5"
 
 [dev-dependencies]
 termcolor = "1.1"

JigSAT/src/clause.rs

@@ -73,7 +73,15 @@ impl Clause {
     // Does not set lbd !
     // Inits search to 1 and mark to 0. Sets abstraction.
     pub(crate) fn new(lits: Vec<Lit>) -> Clause {
-        Clause { deleted: false, can_be_deleted: true, lbd: 0, search: 1, mark: 0, abstraction: calc_abstraction(&lits), lits }
+        Clause {
+            deleted: false,
+            can_be_deleted: true,
+            lbd: 0,
+            search: 1,
+            mark: 0,
+            abstraction: calc_abstraction(&lits),
+            lits,
+        }
     }
 
     pub(crate) fn swap(&mut self, i: usize, j: usize) {
@@ -143,7 +151,15 @@ impl Clause {
     }
 
     pub(crate) fn clause_from_vec(vec: &Vec<Lit>) -> Clause {
-        Clause { deleted: false, can_be_deleted: true, lbd: 0, search: 1, mark: 0, abstraction: calc_abstraction(vec), lits: vec.clone() }
+        Clause {
+            deleted: false,
+            can_be_deleted: true,
+            lbd: 0,
+            search: 1,
+            mark: 0,
+            abstraction: calc_abstraction(vec),
+            lits: vec.clone(),
+        }
     }
 
     #[inline(always)]

JigSAT/src/conflict_analysis.rs

@@ -1,6 +1,14 @@
 use core::panic;
 
-use crate::{clause::*, decision::*, formula::*, lit::*, minimize::*, solver::{Solver, SearchMode}, trail::*};
+use crate::{
+    clause::*,
+    decision::*,
+    formula::*,
+    lit::*,
+    minimize::*,
+    solver::{SearchMode, Solver},
+    trail::*,
+};
 
 #[derive(Debug)]
 pub enum Conflict {
@@ -9,7 +17,9 @@ pub enum Conflict {
     Learned(u32, Clause),
 }
 
-pub(crate) fn analyze_conflict(f: &Formula, trail: &Trail, cref: usize, decisions: &mut impl Decisions, s: &mut Solver) -> Conflict {
+pub(crate) fn analyze_conflict(
+    f: &Formula, trail: &Trail, cref: usize, decisions: &mut impl Decisions, s: &mut Solver,
+) -> Conflict {
     let decisionlevel = trail.decision_level();
     if decisionlevel == 0 {
         return Conflict::Ground;

JigSAT/src/decision.rs

@@ -1,9 +1,14 @@
-use crate::{assignments::*, formula::*, util::*, trail::*};
-use std::{ops::{Index, IndexMut}, collections::BinaryHeap};
+use crate::{assignments::*, formula::*, trail::*, util::*};
+use std::{
+    collections::BinaryHeap,
+    ops::{Index, IndexMut},
+};
 
 const INVALID: usize = usize::MAX;
 pub(crate) trait Decisions {
-    fn new(f: &Formula) -> Self where Self:Sized;
+    fn new(f: &Formula) -> Self
+    where
+        Self: Sized;
 
     fn bump_vec_of_vars(&mut self, f: &Formula, v: Vec<usize>);
 
@@ -27,7 +32,6 @@ pub struct Node {
     pub ts: usize,
 }
 
-
 impl Default for Node {
     fn default() -> Self {
         Node { next: usize::MAX, prev: usize::MAX, ts: 0 }
@@ -90,7 +94,6 @@ impl VMTF {
         VMTF { linked_list, timestamp: f.num_vars + 1, start: head, search: head }
     }
 
-
     fn rescore(&mut self, _f: &Formula) {
         let mut curr_score = self.linked_list.len();
         let mut curr = self.start;
@@ -253,11 +256,7 @@ impl IndexMut<usize> for Heap {
 
 impl Default for Heap {
     fn default() -> Self {
-        Heap {
-            activity: Vec::new(),
-            heap: Vec::new(),
-            indices: Vec::new(),
-        }
+        Heap { activity: Vec::new(), heap: Vec::new(), indices: Vec::new() }
     }
 }
 
@@ -365,7 +364,6 @@ impl Heap {
         }
         self[idx] = x;
         self.indices[x] = idx;
-
     }
 
     fn remove_min(&mut self) -> usize {
@@ -405,7 +403,6 @@ impl VSIDS {
     }
 }
 
-
 impl Decisions for VSIDS {
     fn new(formula: &Formula) -> Self {
         let mut vsids = VSIDS::default();
@@ -414,7 +411,7 @@ impl Decisions for VSIDS {
         vsids
     }
 
-   fn get_next(&mut self, a: &Assignments, _f: &Formula) -> Option<usize> {
+    fn get_next(&mut self, a: &Assignments, _f: &Formula) -> Option<usize> {
         while !self.empty() {
             let next = self.remove_min();
             if a[next] >= 2 {
@@ -468,7 +465,6 @@ impl Decisions for VSIDS {
     fn bump_vec_of_vars(&mut self, f: &Formula, v: Vec<usize>) {}
 }
 
-
 /*
 impl Decisions {
     pub(crate) fn new(formula: &Formula) -> Self {
@@ -502,4 +498,4 @@ impl Decisions {
     }
 }
 
-*/
+*/

JigSAT/src/formula.rs

@@ -1,7 +1,7 @@
-use crate::{assignments::*, clause::*, solver::*, trail::*, watches::*, solver_types::*, lit::*};
+use crate::{assignments::*, clause::*, lit::*, solver::*, solver_types::*, trail::*, watches::*};
 
 use log::debug;
-use std::{ops::{Index, IndexMut}};
+use std::ops::{Index, IndexMut};
 pub struct Formula {
     pub clauses: Vec<Clause>,
     learnt_core: Vec<Cref>,
@@ -164,7 +164,7 @@ impl Formula {
         if self.learnt_core.len() == 0 {
             return;
         }
-        self.learnt_core.sort_unstable_by(|a , b | self.clauses[*a].less_than(&self.clauses[*b]));
+        self.learnt_core.sort_unstable_by(|a, b| self.clauses[*a].less_than(&self.clauses[*b]));
         //s.max_len += self.len() + 300;
         //self.num_reduced += 1;
         if self[self.learnt_core[self.learnt_core.len() / 2]].lbd <= 3 {
@@ -189,7 +189,6 @@ impl Formula {
                 clause.can_be_deleted = true;
                 i += 1;
             }
-
         }
 
         /*

JigSAT/src/lib.rs

@@ -8,13 +8,14 @@ mod decision;
 mod formula;
 mod lit;
 mod minimize;
+mod modes;
 pub mod parser;
 mod preprocess;
+mod restart;
 mod solver;
+mod solver_types;
+mod target_phase;
 mod trail;
 mod unit_prop;
 mod util;
 mod watches;
-mod modes;
-mod restart;
-mod solver_types;

JigSAT/src/lit.rs

@@ -78,11 +78,6 @@ impl Lit {
         (!self).code as usize
     }
 
-    #[inline(always)]
-    pub fn phase_saved(idx: usize, assignments: &Assignments) -> Lit {
-        Lit { code: (idx << 1) as u32 | ((assignments[idx] == 1) as u32) }
-    }
-
     // This is only called in the parser
     pub fn new(idx: usize, polarity: bool) -> Lit {
         Lit { code: (idx << 1) as u32 | (polarity as u32) }

JigSAT/src/modes.rs

@@ -1,6 +1,11 @@
 // An attempt to separate out the modes and phases stuff
 
-use crate::{solver::*, restart::*, decision::*};
+use crate::{
+    decision::*,
+    restart::*,
+    solver::*,
+    target_phase::{self, TargetPhase},
+};
 
 pub(crate) fn adapt_solver(solver: &mut Solver, decisions: &mut impl Decisions) -> bool {
     solver.adapt_strategies = false;
@@ -23,19 +28,21 @@ pub(crate) fn adapt_solver(solver: &mut Solver, decisions: &mut impl Decisions)
     false
 }
 
-pub(crate) fn change_mode(solver: &mut Solver, decisions: &mut impl Decisions) {
+pub(crate) fn change_mode(solver: &mut Solver, decisions: &mut impl Decisions, target_phase: &mut TargetPhase) {
     match solver.search_mode {
         SearchMode::Stable => {
+            println!("c Changing mode to Focus mode");
             solver.restart.swap_mode();
             decisions.set_var_decay(0.95);
             solver.search_mode = SearchMode::Focus;
-        },
+        }
         SearchMode::Focus => {
+            println!("c Changing mode to Stable mode");
             solver.restart.swap_mode();
             decisions.set_var_decay(0.75);
             solver.search_mode = SearchMode::Stable;
-            // TODO: reset target_phase
-        },
-        _ => {},
+            target_phase.reset();
+        }
+        _ => {}
     }
-}
+}

JigSAT/src/preprocess.rs

@@ -9,7 +9,7 @@ use log::debug;
 use std::collections::VecDeque;
 //use std::collections::BinaryHeap;
 
-use crate::{clause::*, formula::*, lit::*, trail::*, solver_types::*};
+use crate::{clause::*, formula::*, lit::*, solver_types::*, trail::*};
 
 #[derive(PartialEq)]
 pub(crate) enum SubsumptionRes {

JigSAT/src/restart.rs

@@ -1,4 +1,3 @@
-
 use crate::solver::*;
 
 pub(crate) enum RestartMode {
@@ -14,7 +13,6 @@ struct EMA {
     period: usize,
 }
 
-
 impl EMA {
     fn update(&mut self, next: f64) {
         self.value += self.beta * (next - self.value);
@@ -30,13 +28,7 @@ impl EMA {
         }
     }
     fn new(alpha: f64) -> Self {
-        EMA {
-            value: 1.0,
-            alpha,
-            beta: 1.0,
-            wait: 1,
-            period: 1,
-        }
+        EMA { value: 1.0, alpha, beta: 1.0, wait: 1, period: 1 }
     }
 }
 
@@ -51,7 +43,6 @@ pub(crate) struct Glucose {
     block: f64,
     num_restarts: usize,
     num_blocked: usize,
-
 }
 
 impl Default for Glucose {
@@ -92,7 +83,9 @@ impl Glucose {
     }
 
     pub(crate) fn block_restart(&mut self, curr_confl: usize) -> bool {
-        if self.last_trail_size as f64 > self.block as f64 * self.ema_trail_wide.value && curr_confl >= self.minimum_conflicts_for_blocking_restarts {
+        if self.last_trail_size as f64 > self.block as f64 * self.ema_trail_wide.value
+            && curr_confl >= self.minimum_conflicts_for_blocking_restarts
+        {
             self.minimum_conflicts = curr_confl + 50;
             self.num_blocked += 1;
             return true;
@@ -110,12 +103,7 @@ struct Luby {
 
 impl Default for Luby {
     fn default() -> Self {
-        Luby {
-            num_restarts: 0,
-            step: 100,
-            curr_restarts: 0,
-            limit: 100,
-        }
+        Luby { num_restarts: 0, step: 100, curr_restarts: 0, limit: 100 }
     }
 }
 
@@ -152,16 +140,12 @@ impl Luby {
 pub(crate) struct Restart {
     restart: RestartMode,
     luby: Luby,
-    pub(crate) glucose: Glucose
+    pub(crate) glucose: Glucose,
 }
 
 impl Restart {
     pub(crate) fn new() -> Restart {
-        Restart {
-            restart: RestartMode::Glucose,
-            luby: Luby::default(),
-            glucose: Glucose::default(),
-        }
+        Restart { restart: RestartMode::Glucose, luby: Luby::default(), glucose: Glucose::default() }
     }
 
     pub(crate) fn set_restart_mode(&mut self, mode: RestartMode) {
@@ -185,7 +169,7 @@ impl Restart {
     pub(crate) fn block_restart(&mut self, curr_confl: usize) -> bool {
         match self.restart {
             RestartMode::Glucose => self.glucose.block_restart(curr_confl),
-            RestartMode::Luby => { true },
+            RestartMode::Luby => true,
         }
     }
 }