varisat 0.2.2

A CDCL based SAT solver (library)
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

//! Propagation of binary clauses.
use partial_ref::{partial, PartialRef};

use varisat_formula::Lit;

use crate::context::{parts::*, Context};

use super::{enqueue_assignment, Conflict, Reason};

/// Propagate all literals implied by the given literal via binary clauses.
///
/// On conflict return the binary clause propgating the conflicting assignment.
pub fn propagate_binary(
    mut ctx: partial!(
        Context,
        mut AssignmentP,
        mut ImplGraphP,
        mut TrailP,
        BinaryClausesP,
    ),
    lit: Lit,
) -> Result<(), Conflict> {
    let (binary_clauses, mut ctx) = ctx.split_part(BinaryClausesP);

    for &implied in binary_clauses.implied(lit) {
        let assignment = ctx.part(AssignmentP);

        if assignment.lit_is_false(implied) {
            return Err(Conflict::Binary([implied, !lit]));
        } else if !assignment.lit_is_true(implied) {
            enqueue_assignment(ctx.borrow(), implied, Reason::Binary([!lit]));
        }
    }

    Ok(())
}