summaryrefslogtreecommitdiffstats
path: root/vendor/varisat/src/analyze_conflict.rs
blob: 16f918782003aa637e1710316c0ee810f0196f40 (plain)
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
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
//! Learns a new clause by analyzing a conflict.
use std::mem::swap;

use partial_ref::{partial, split_borrow, PartialRef};

use vec_mut_scan::VecMutScan;

use varisat_formula::{lit::LitIdx, Lit, Var};
use varisat_internal_proof::{clause_hash, lit_hash, ClauseHash};

use crate::{
    clause::ClauseRef,
    context::{parts::*, Context},
    prop::{Conflict, Reason},
};

/// Temporaries for conflict analysis
#[derive(Default)]
pub struct AnalyzeConflict {
    /// This is the learned clause after analysis finishes.
    clause: Vec<Lit>,
    /// Number of literals in the current clause at the current level.
    current_level_count: usize,
    /// Variables in the current clause.
    var_flags: Vec<bool>,
    /// Entries to clean in `var_flags`.
    to_clean: Vec<Var>,
    /// Clauses to bump.
    involved: Vec<ClauseRef>,
    /// Hashes of all involved clauses needed to proof the minimized clause.
    clause_hashes: Vec<ClauseHash>,
    /// Clause hashes paired with the trail depth of the propagated lit.
    unordered_clause_hashes: Vec<(LitIdx, ClauseHash)>,
    /// Stack for recursive minimization.
    stack: Vec<Lit>,
}

impl AnalyzeConflict {
    /// Update structures for a new variable count.
    pub fn set_var_count(&mut self, count: usize) {
        self.var_flags.resize(count, false);
    }

    /// The learned clause.
    pub fn clause(&self) -> &[Lit] {
        &self.clause
    }

    /// Long clauses involved in the conflict.
    pub fn involved(&self) -> &[ClauseRef] {
        &self.involved
    }

    /// Hashes of clauses involved in the proof of the learned clause.
    ///
    /// Hashes are in clause propagation order.
    pub fn clause_hashes(&self) -> &[ClauseHash] {
        &self.clause_hashes
    }
}

/// Learns a new clause by analyzing a conflict.
///
/// Returns the lowest decision level that makes the learned clause asserting.
pub fn analyze_conflict<'a>(
    mut ctx: partial!(
        Context<'a>,
        mut AnalyzeConflictP,
        mut VsidsP,
        ClauseAllocP,
        ImplGraphP,
        ProofP<'a>,
        TrailP,
    ),
    conflict: Conflict,
) -> usize {
    split_borrow!(lit_ctx = &(ClauseAllocP) ctx);

    {
        let analyze = ctx.part_mut(AnalyzeConflictP);

        analyze.clause.clear();
        analyze.involved.clear();
        analyze.clause_hashes.clear();
        analyze.unordered_clause_hashes.clear();
        analyze.current_level_count = 0;
    }

    // We start with all the literals of the conflicted clause
    let conflict_lits = conflict.lits(&lit_ctx);

    if ctx.part(ProofP).clause_hashes_required() {
        ctx.part_mut(AnalyzeConflictP)
            .clause_hashes
            .push(clause_hash(conflict_lits));
    }

    if ctx.part(TrailP).current_level() == 0 {
        // Conflict with no decisions, generate empty clause
        return 0;
    }

    for &lit in conflict_lits {
        add_literal(ctx.borrow(), lit);
    }

    if let Conflict::Long(cref) = conflict {
        ctx.part_mut(AnalyzeConflictP).involved.push(cref);
    }

    // To get rid of all but one literal of the current level, we resolve the clause with the reason
    // for those literals. The correct order for this is reverse chronological.

    split_borrow!(ctx_trail = &(TrailP) ctx);
    // split_borrow!(ctx_analyze = &(mut AnalyzeConflictP) ctx);

    for &lit in ctx_trail.part(TrailP).trail().iter().rev() {
        let analyze = ctx.part_mut(AnalyzeConflictP);
        let lit_present = &mut analyze.var_flags[lit.index()];
        // Is the lit present in the current clause?
        if *lit_present {
            *lit_present = false;
            analyze.current_level_count -= 1;
            if analyze.current_level_count == 0 {
                // lit is the last literal of the current level present in the current clause,
                // therefore the resulting clause will assert !lit so we put in position 0
                analyze.clause.push(!lit);
                let end = analyze.clause.len() - 1;
                analyze.clause.swap(0, end);

                break;
            } else {
                // We removed the literal and now add its reason.
                let (graph, mut ctx) = ctx.split_part(ImplGraphP);

                let reason = graph.reason(lit.var());

                let lits = reason.lits(&lit_ctx);

                if ctx.part(ProofP).clause_hashes_required() && !reason.is_unit() {
                    let hash = clause_hash(lits) ^ lit_hash(lit);
                    ctx.part_mut(AnalyzeConflictP).clause_hashes.push(hash);
                }

                for &lit in lits {
                    add_literal(ctx.borrow(), lit);
                }

                if let Reason::Long(cref) = reason {
                    ctx.part_mut(AnalyzeConflictP).involved.push(*cref);
                }
            }
        }
    }

    // This needs var_flags set and keeps some var_fags set.
    minimize_clause(ctx.borrow());

    let (analyze, mut ctx) = ctx.split_part_mut(AnalyzeConflictP);

    if ctx.part(ProofP).clause_hashes_required() {
        // Clause minimization cannot give us clause hashes in propagation order, so we need to sort
        // them. Clauses used during minimization propagte before clauses used during initial
        // analysis. The clauses during initial analysis are discovered in reverse propagation
        // order. This means we can sort the minimization clauses in reverse order, append them to
        // the initial clauses and then reverse the order of all clauses.
        analyze
            .unordered_clause_hashes
            .sort_unstable_by_key(|&(depth, _)| !depth);

        analyze
            .unordered_clause_hashes
            .dedup_by_key(|&mut (depth, _)| depth);

        analyze.clause_hashes.extend(
            analyze
                .unordered_clause_hashes
                .iter()
                .map(|&(_, hash)| hash),
        );
        analyze.clause_hashes.reverse();
    }

    for var in analyze.to_clean.drain(..) {
        analyze.var_flags[var.index()] = false;
    }

    // We find the highest level literal besides the asserted literal and move it into position 1.
    // This is important to ensure the watchlist constraints are not violated on backtracking.
    let mut backtrack_to = 0;

    if analyze.clause.len() > 1 {
        let (prefix, rest) = analyze.clause.split_at_mut(2);
        let lit_1 = &mut prefix[1];
        backtrack_to = ctx.part(ImplGraphP).level(lit_1.var());
        for lit in rest.iter_mut() {
            let lit_level = ctx.part(ImplGraphP).level(lit.var());
            if lit_level > backtrack_to {
                backtrack_to = lit_level;
                swap(lit_1, lit);
            }
        }
    }

    ctx.part_mut(VsidsP).decay();

    backtrack_to
}

/// Add a literal to the current clause.
fn add_literal(
    mut ctx: partial!(
        Context,
        mut AnalyzeConflictP,
        mut VsidsP,
        ImplGraphP,
        TrailP
    ),
    lit: Lit,
) {
    let (analyze, mut ctx) = ctx.split_part_mut(AnalyzeConflictP);
    let lit_level = ctx.part(ImplGraphP).level(lit.var());
    // No need to add literals that are set by unit clauses or already present
    if lit_level > 0 && !analyze.var_flags[lit.index()] {
        ctx.part_mut(VsidsP).bump(lit.var());

        analyze.var_flags[lit.index()] = true;
        if lit_level == ctx.part(TrailP).current_level() {
            analyze.current_level_count += 1;
        } else {
            analyze.clause.push(lit);
            analyze.to_clean.push(lit.var());
        }
    }
}

/// A Bloom filter of levels.
#[derive(Default)]
struct LevelAbstraction {
    bits: u64,
}

impl LevelAbstraction {
    /// Add a level to the Bloom filter.
    pub fn add(&mut self, level: usize) {
        self.bits |= 1 << (level % 64)
    }

    /// Test whether a level could be in the Bloom filter.
    pub fn test(&self, level: usize) -> bool {
        self.bits & (1 << (level % 64)) != 0
    }
}

/// Performs recursive clause minimization.
///
/// **Note:** Requires AnalyzeConflict's var_flags to be set for exactly the variables of the
/// unminimized claused. This also sets some more var_flags, but lists them in to_clean.
///
/// This routine tries to remove some redundant literals of the learned clause. The idea is to
/// detect literals of the learned clause that are already implied by other literals of the clause.
///
/// This is done by performing a DFS in the implication graph (following edges in reverse) for each
/// literal (apart from the asserting one). The search doesn't expand literals already known to be
/// implied by literals of the clause. When a decision literal that is not in the clause is found,
/// it means that the literal is not redundant.
///
/// There are two optimizations used here: The first one is to stop the search as soon as a literal
/// of a decision level not present in the clause is found. If the DFS would be continued it would
/// at some point reach the decision of that level. That decision belongs to a level not in the
/// clause and thus itself can't be in the clause. Checking whether the decision level is among the
/// clause's decision levels is done approximately using a Bloom filter.
///
/// The other optimization is to avoid duplicating work during the DFS searches. When one literal is
/// found to be redundant that means the whole search stayed within the implied literals. We
/// remember this and will not expand any of these literals for the following DFS searches.
///
/// In this implementation the var_flags array here has two purposes. At the beginning it is set for
/// all the literals of the clause. It is also used to mark the literals visited during the DFS.
/// This allows us to combine the already-visited-check with the literal-present-in-clause check. It
/// also allows for a neat implementation of the second optimization. When the search finds the
/// literal to be non-redundant, we clear var_flags for the literals we visited, resetting it to the
/// state at the beginning of the DFS. When the literal was redundant we keep it as is. This means
/// the following DFS will not expand these literals.
fn minimize_clause<'a>(
    mut ctx: partial!(
        Context<'a>,
        mut AnalyzeConflictP,
        mut VsidsP,
        ClauseAllocP,
        ImplGraphP,
        ProofP<'a>,
        TrailP,
    ),
) {
    let (analyze, mut ctx) = ctx.split_part_mut(AnalyzeConflictP);
    split_borrow!(lit_ctx = &(ClauseAllocP) ctx);
    let impl_graph = ctx.part(ImplGraphP);

    let mut involved_levels = LevelAbstraction::default();

    for &lit in analyze.clause.iter() {
        involved_levels.add(impl_graph.level(lit.var()));
    }

    let mut scan = VecMutScan::new(&mut analyze.clause);

    // we always keep the first literal
    scan.next();

    'next_lit: while let Some(lit) = scan.next() {
        if impl_graph.reason(lit.var()) == &Reason::Unit {
            continue;
        }

        // Start the DFS
        analyze.stack.clear();
        analyze.stack.push(!*lit);

        // Used to remember which var_flags are set during this DFS
        let top = analyze.to_clean.len();

        // Used to remember which clause hashes were added during the DFS, so we can remove them in
        // case the literal is not redundant.
        let hashes_top = analyze.unordered_clause_hashes.len();

        while let Some(lit) = analyze.stack.pop() {
            let reason = impl_graph.reason(lit.var());
            let lits = reason.lits(&lit_ctx);

            if ctx.part(ProofP).clause_hashes_required() && !reason.is_unit() {
                let depth = impl_graph.depth(lit.var()) as LitIdx;
                let hash = clause_hash(lits) ^ lit_hash(lit);
                analyze.unordered_clause_hashes.push((depth, hash));
            }

            for &reason_lit in lits {
                let reason_level = impl_graph.level(reason_lit.var());

                if !analyze.var_flags[reason_lit.index()] && reason_level > 0 {
                    // We haven't established reason_lit to be redundant, haven't visited it yet and
                    // it's not implied by unit clauses.

                    if impl_graph.reason(reason_lit.var()) == &Reason::Unit
                        || !involved_levels.test(reason_level)
                    {
                        // reason_lit is a decision not in the clause or in a decision level known
                        // not to be in the clause. Abort the search.

                        // Reset the var_flags set during _this_ DFS.
                        for lit in analyze.to_clean.drain(top..) {
                            analyze.var_flags[lit.index()] = false;
                        }
                        // Remove clauses not needed to justify the minimized clause.
                        analyze.unordered_clause_hashes.truncate(hashes_top);
                        continue 'next_lit;
                    } else {
                        analyze.var_flags[reason_lit.index()] = true;
                        analyze.to_clean.push(reason_lit.var());
                        analyze.stack.push(!reason_lit);
                    }
                }
            }
        }

        lit.remove();
    }
}