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
|
//! Watchlists to detect clauses that became unit.
//!
//! Each (long) clause has always two watches pointing to it. The watches are kept in the watchlists
//! of two different literals of the clause. Whenever the watches are moved to different literals
//! the litereals of the clause are permuted so the watched literals are in position 0 and 1.
//!
//! When a clause is not unit under the current assignment, the watched literals point at two
//! non-false literals. When a clause is unit and thus propagating, the true literal is watched and
//! in position 0, the other watched literal is the one with the largest decision level and kept in
//! position 1. When a clause becomes satisfied before becoming unit the watches can be kept as they
//! were.
//!
//! When a literal is assigned false that invariant can be invalidated. This can be detected by
//! scanning the watches of the assigned literal. When the assignment is processed the watches are
//! moved to restore that invariant. Unless there is a conflict, i.e. a clause with no non-false
//! literals, this can always be done. This also finds all clauses that became unit. The new unit
//! clauses are exactly those clauses where no two non-false literals can be found.
//!
//! There is no need to update watchlists on backtracking, as unassigning variables cannot
//! invalidate the invariant.
//!
//! See [Section 4.5.1 of the "Handbook of Satisfiability"][handbook-ch4] for more details and
//! references.
//!
//! As a further optimization we use blocking literals. This means that each watch stores a literal
//! of the clause that is different from the watched literal. It can be the other watched literal or
//! any unwatched literal. When that literal is true, the clause is already satisfied, meaning that
//! no watches need to be updated. This can be detected by just looking at the watch, avoiding
//! access of the clause database. This variant was introduced by [Niklas Sörensson and Niklas Eén
//! in "MINISAT 2.1 and MINISAT++1.0 — SAT Race 2008 Editions"][minisat-2.1].
//!
//! [handbook-ch4]: https://www.satassociation.org/articles/FAIA185-0131.pdf
//! [minisat-2.1]: https://www.cril.univ-artois.fr/SAT09/solvers/booklet.pdf
use partial_ref::{partial, PartialRef};
use varisat_formula::Lit;
use crate::{
clause::{db, ClauseRef},
context::{parts::*, Context},
};
/// A watch on a long clause.
#[derive(Copy, Clone)]
pub struct Watch {
/// Clause which has the referring lit in position 0 or 1.
pub cref: ClauseRef,
/// A lit of the clause, different from the referring lit.
pub blocking: Lit,
}
/// Watchlists to detect clauses that became unit.
pub struct Watchlists {
/// Contains only valid data for indices of assigned variables.
watches: Vec<Vec<Watch>>,
/// Whether watchlists are present
enabled: bool,
}
impl Default for Watchlists {
fn default() -> Watchlists {
Watchlists {
watches: vec![],
enabled: true,
}
}
}
impl Watchlists {
/// Update structures for a new variable count.
pub fn set_var_count(&mut self, count: usize) {
self.watches.resize(count * 2, vec![]);
}
/// Start watching a clause.
///
/// `lits` have to be the first two literals of the given clause.
pub fn watch_clause(&mut self, cref: ClauseRef, lits: [Lit; 2]) {
if !self.enabled {
return;
}
for i in 0..2 {
let watch = Watch {
cref,
blocking: lits[i ^ 1],
};
self.add_watch(!lits[i], watch);
}
}
/// Return watches for a given literal.
pub fn watched_by_mut(&mut self, lit: Lit) -> &mut Vec<Watch> {
&mut self.watches[lit.code()]
}
/// Make a literal watch a clause.
pub fn add_watch(&mut self, lit: Lit, watch: Watch) {
self.watches[lit.code()].push(watch)
}
/// Are watchlists enabled.
pub fn enabled(&self) -> bool {
self.enabled
}
/// Clear and disable watchlists.
///
/// Actual clearing of the watchlists is done on re-enabling of the watchlists.
pub fn disable(&mut self) {
self.enabled = false;
}
}
/// Enable and rebuild watchlists.
pub fn enable_watchlists(mut ctx: partial!(Context, mut WatchlistsP, ClauseAllocP, ClauseDbP)) {
let (watchlists, mut ctx) = ctx.split_part_mut(WatchlistsP);
if watchlists.enabled {
return;
}
for watchlist in watchlists.watches.iter_mut() {
watchlist.clear();
}
watchlists.enabled = true;
let (alloc, mut ctx) = ctx.split_part(ClauseAllocP);
for cref in db::clauses_iter(&ctx.borrow()) {
let lits = alloc.clause(cref).lits();
watchlists.watch_clause(cref, [lits[0], lits[1]]);
}
}
|
