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
/// Implementation of Stochastic Local Search
use {
crate::{assign::AssignIF, types::*},
std::collections::HashMap,
};
pub trait StochasticLocalSearchIF {
/// returns the decision level of the given assignment and the one of the final assignment.
/// Note: the lower level a set of clauses make a conflict at,
/// the higher learning rate a solver can keep and the better learnt clauses we will have.
/// This would be a better criteria that can be used in CDCL solvers.
fn stochastic_local_search(
&mut self,
asg: &impl AssignIF,
start: &mut HashMap<VarId, bool>,
limit: usize,
) -> (usize, usize);
}
impl StochasticLocalSearchIF for ClauseDB {
fn stochastic_local_search(
&mut self,
_asg: &impl AssignIF,
assignment: &mut HashMap<VarId, bool>,
limit: usize,
) -> (usize, usize) {
let mut returns: (usize, usize) = (0, 0);
let mut last_flip = self.num_clause;
let mut seed = 721_109;
for step in 1..=limit {
let mut unsat_clauses = 0;
// let mut level: DecisionLevel = 0;
// CONSIDER: counting only given (permanent) clauses.
let mut flip_target: HashMap<VarId, usize> = HashMap::new();
let mut target_clause: Option<&Clause> = None;
for c in self.clause.iter().skip(1).filter(|c| !c.is_dead()) {
// let mut cls_lvl: DecisionLevel = 0;
if c.is_falsified(assignment, &mut flip_target) {
unsat_clauses += 1;
// for l in c.lits.iter() {
// cls_lvl = cls_lvl.max(asg.level(l.vi()));
// }
// level = level.max(cls_lvl);
if target_clause.is_none() || unsat_clauses == step {
target_clause = Some(c);
for l in c.lits.iter() {
flip_target.entry(l.vi()).or_insert(0);
}
}
}
}
if step == 1 {
returns.0 = unsat_clauses;
// returns.0 = level as usize;
}
returns.1 = unsat_clauses;
// returns.1 = level as usize;
if unsat_clauses == 0 || step == limit {
break;
}
seed = ((((!seed & 0x0000_0000_ffff_ffff) * 1_304_003) % 2_003_819)
^ ((!last_flip & 0x0000_0000_ffff_ffff) * seed))
% 3_754_873;
if let Some(c) = target_clause {
let beta: f64 = 3.2 - 2.1 / (1.0 + unsat_clauses as f64).log(2.0);
// let beta: f64 = if unsat_clauses <= 3 { 1.0 } else { 3.0 };
let factor = |vi| beta.powf(-(*flip_target.get(vi).unwrap() as f64));
let vars = c.lits.iter().map(|l| l.vi()).collect::<Vec<_>>();
let index = ((seed % 100) as f64 / 100.0) * vars.iter().map(factor).sum::<f64>();
let mut sum: f64 = 0.0;
for vi in vars.iter() {
sum += factor(vi);
if index <= sum {
assignment.entry(*vi).and_modify(|e| *e = !*e);
last_flip = *vi;
break;
}
}
} else {
break;
}
}
returns
}
}
impl Clause {
fn is_falsified(
&self,
assignment: &HashMap<VarId, bool>,
flip_target: &mut HashMap<VarId, usize>,
) -> bool {
let mut num_sat = 0;
let mut sat_vi = 0;
for l in self.iter() {
let vi = l.vi();
match assignment.get(&vi) {
Some(b) if *b == l.as_bool() => {
if num_sat == 1 {
return false;
}
num_sat += 1;
sat_vi = vi;
}
None => unreachable!(),
_ => (),
}
}
if num_sat == 0 {
true
} else {
*flip_target.entry(sat_vi).or_insert(0) += 1;
false
}
}
}