Struct TwoSatisfiability

Source

pub struct TwoSatisfiability {
    vsize: usize,
    edges: Vec<(usize, usize)>,
}

Fields§

§vsize: usize§edges: Vec<(usize, usize)>

Implementations§

Source §

impl TwoSatisfiability

Source

pub fn new(vsize: usize) -> Self

Examples found in repository ?

crates/library_checker/src/other/two_sat.rs (line 12)

5pub fn two_sat(reader: impl Read, writer: impl Write) {
6    prepare_io!(reader, writer);
7    sc!(_p: String,
8        _cnf: String,
9        n,
10        m,
11        ab: [(isize, isize, isize); iter m]);
12    let mut two_sat = TwoSatisfiability::new(n);
13    for (a, b, _) in ab {
14        two_sat.add_clause(a.unsigned_abs() - 1, a >= 0, b.unsigned_abs() - 1, b >= 0);
15    }
16    if let Some(v) = two_sat.two_satisfiability() {
17        let ans = v
18            .into_iter()
19            .enumerate()
20            .map(|(i, v)| if v { i as i32 + 1 } else { -(i as i32 + 1) });
21        pp!("s SATISFIABLE"; "v", @it ans, 0, !);
22    } else {
23        pp!("s UNSATISFIABLE");
24    }
25}

Source

pub fn add_clause(&mut self, x: usize, f: bool, y: usize, g: bool)

(p_x = f) | (p_y = g)

Examples found in repository ?

crates/competitive/src/graph/two_satisfiability.rs (line 22)

21    pub fn add_or(&mut self, x: usize, y: usize) {
22        self.add_clause(x, true, y, true);
23    }
24    pub fn add_nand(&mut self, x: usize, y: usize) {
25        self.add_clause(x, false, y, false);
26    }

More examples

Hide additional examples

crates/library_checker/src/other/two_sat.rs (line 14)

5pub fn two_sat(reader: impl Read, writer: impl Write) {
6    prepare_io!(reader, writer);
7    sc!(_p: String,
8        _cnf: String,
9        n,
10        m,
11        ab: [(isize, isize, isize); iter m]);
12    let mut two_sat = TwoSatisfiability::new(n);
13    for (a, b, _) in ab {
14        two_sat.add_clause(a.unsigned_abs() - 1, a >= 0, b.unsigned_abs() - 1, b >= 0);
15    }
16    if let Some(v) = two_sat.two_satisfiability() {
17        let ans = v
18            .into_iter()
19            .enumerate()
20            .map(|(i, v)| if v { i as i32 + 1 } else { -(i as i32 + 1) });
21        pp!("s SATISFIABLE"; "v", @it ans, 0, !);
22    } else {
23        pp!("s UNSATISFIABLE");
24    }
25}

Source

pub fn two_satisfiability(self) -> Option<Vec<bool>>

Examples found in repository ?

crates/library_checker/src/other/two_sat.rs (line 16)

5pub fn two_sat(reader: impl Read, writer: impl Write) {
6    prepare_io!(reader, writer);
7    sc!(_p: String,
8        _cnf: String,
9        n,
10        m,
11        ab: [(isize, isize, isize); iter m]);
12    let mut two_sat = TwoSatisfiability::new(n);
13    for (a, b, _) in ab {
14        two_sat.add_clause(a.unsigned_abs() - 1, a >= 0, b.unsigned_abs() - 1, b >= 0);
15    }
16    if let Some(v) = two_sat.two_satisfiability() {
17        let ans = v
18            .into_iter()
19            .enumerate()
20            .map(|(i, v)| if v { i as i32 + 1 } else { -(i as i32 + 1) });
21        pp!("s SATISFIABLE"; "v", @it ans, 0, !);
22    } else {
23        pp!("s UNSATISFIABLE");
24    }
25}