splr 0.17.0

A modern CDCL SAT solver in Rust
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156

/// Decision var selection

#[cfg(feature = "rephase")]
use super::property;

use {
    super::{AssignStack, VarHeapIF},
    crate::types::*,
    std::collections::HashMap,
};

/// ```ignore
/// let x: Option<bool> = var_assign!(self, lit.vi());
/// ```
#[cfg(feature = "unsafe_access")]
macro_rules! var_assign {
    ($asg: expr, $var: expr) => {
        unsafe { *$asg.assign.get_unchecked($var) }
    };
}
#[cfg(not(feature = "unsafe_access"))]
macro_rules! var_assign {
    ($asg: expr, $var: expr) => {
        $asg.assign[$var]
    };
}

/// API for var selection, depending on an internal heap.
pub trait VarSelectIF {
    #[cfg(feature = "rephase")]
    /// return best phases
    fn best_phases_ref(&mut self, default_value: Option<bool>) -> HashMap<VarId, bool>;
    #[cfg(feature = "rephase")]
    /// force an assignment obtained by SLS
    fn override_rephasing_target(&mut self, assignment: &HashMap<VarId, bool>) -> usize;
    /// give rewards to vars selected by SLS
    fn reward_by_sls(&mut self, assignment: &HashMap<VarId, bool>) -> usize;
    #[cfg(feature = "rephase")]
    /// select rephasing target
    fn select_rephasing_target(&mut self);
    #[cfg(feature = "rephase")]
    /// check the consistency
    fn check_consistency_of_best_phases(&mut self);
    /// select a new decision variable.
    fn select_decision_literal(&mut self) -> Lit;
    /// update the internal heap on var order.
    fn update_order(&mut self, v: VarId);
    /// rebuild the internal var_order
    fn rebuild_order(&mut self);
}

impl VarSelectIF for AssignStack {
    #[cfg(feature = "rephase")]
    fn best_phases_ref(&mut self, default_value: Option<bool>) -> HashMap<VarId, bool> {
        self.var
            .iter()
            .enumerate()
            .filter_map(|(vi, v)| {
                if self.level[vi] == self.root_level || self.var[vi].is(FlagVar::ELIMINATED) {
                    default_value.map(|b| (vi, b))
                } else {
                    Some((
                        vi,
                        self.best_phases.get(&vi).map_or(
                            self.assign[vi].unwrap_or_else(|| v.is(FlagVar::PHASE)),
                            |(b, _)| *b,
                        ),
                    ))
                }
            })
            .collect::<HashMap<VarId, bool>>()
    }
    #[cfg(feature = "rephase")]
    fn override_rephasing_target(&mut self, assignment: &HashMap<VarId, bool>) -> usize {
        let mut num_flipped = 0;
        for (vi, b) in assignment.iter() {
            if !self.best_phases.get(vi).map_or(false, |(p, _)| *p == *b) {
                num_flipped += 1;
                self.best_phases.insert(*vi, (*b, AssignReason::None));
            }
        }
        num_flipped
    }
    fn reward_by_sls(&mut self, assignment: &HashMap<VarId, bool>) -> usize {
        let mut num_flipped = 0;
        for (vi, b) in assignment.iter() {
            let v = &mut self.var[*vi];
            if v.is(FlagVar::PHASE) != *b {
                num_flipped += 1;
                v.set(FlagVar::PHASE, *b);
                v.reward *= self.activity_decay;
                v.reward += self.activity_anti_decay;
                self.update_heap(*vi);
            }
        }
        num_flipped
    }
    #[cfg(feature = "rephase")]
    fn select_rephasing_target(&mut self) {
        if self.best_phases.is_empty() {
            return;
        }
        self.check_consistency_of_best_phases();
        if self.derefer(property::Tusize::NumUnassertedVar) <= self.best_phases.len() {
            self.best_phases.clear();
            return;
        }
        debug_assert!(self
            .best_phases
            .iter()
            .all(|(vi, b)| self.assign[*vi] != Some(!b.0)));
        self.num_rephase += 1;
        for (vi, (b, _)) in self.best_phases.iter() {
            let v = &mut self.var[*vi];
            v.set(FlagVar::PHASE, *b);
        }
    }
    #[cfg(feature = "rephase")]
    fn check_consistency_of_best_phases(&mut self) {
        if self
            .best_phases
            .iter()
            .any(|(vi, b)| self.assign[*vi] == Some(!b.0))
        {
            self.best_phases.clear();
            self.num_best_assign = self.num_asserted_vars + self.num_eliminated_vars;
        }
    }
    fn select_decision_literal(&mut self) -> Lit {
        let vi = self.select_var();
        Lit::from((vi, self.var[vi].is(FlagVar::PHASE)))
    }
    fn update_order(&mut self, v: VarId) {
        self.update_heap(v);
    }
    fn rebuild_order(&mut self) {
        self.clear_heap();
        for vi in 1..self.var.len() {
            if var_assign!(self, vi).is_none() && !self.var[vi].is(FlagVar::ELIMINATED) {
                self.insert_heap(vi);
            }
        }
    }
}

impl AssignStack {
    /// select a decision var
    fn select_var(&mut self) -> VarId {
        loop {
            let vi = self.get_heap_root();
            if var_assign!(self, vi).is_none() && !self.var[vi].is(FlagVar::ELIMINATED) {
                return vi;
            }
        }
    }
}