Struct TwoSatisfiability

Source

pub struct TwoSatisfiability { /* private fields */ }

Implementations§

Source §

impl TwoSatisfiability

Source

pub fn new(vsize: usize) -> Self

Examples found in repository ?

crates/library_checker/src/math/two_sat.rs (line 17)

6pub fn two_sat(reader: impl Read, mut writer: impl Write) {
7    let s = read_all_unchecked(reader);
8    let mut scanner = Scanner::new(&s);
9    scan!(
10        scanner,
11        _p: String,
12        _cnf: String,
13        n,
14        m,
15        ab: [(isize, isize, isize)]
16    );
17    let mut two_sat = TwoSatisfiability::new(n);
18    for (a, b, _) in ab.take(m) {
19        two_sat.add_clause(a.unsigned_abs() - 1, a >= 0, b.unsigned_abs() - 1, b >= 0);
20    }
21    if let Some(v) = two_sat.two_satisfiability() {
22        writeln!(writer, "s SATISFIABLE").ok();
23        write!(writer, "v").ok();
24        for (i, v) in v.into_iter().enumerate() {
25            write!(
26                writer,
27                " {}",
28                if v { i as i32 + 1 } else { -(i as i32 + 1) }
29            )
30            .ok();
31        }
32        write!(writer, " 0").ok();
33    } else {
34        writeln!(writer, "s UNSATISFIABLE").ok();
35    }
36}

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/math/two_sat.rs (line 19)

6pub fn two_sat(reader: impl Read, mut writer: impl Write) {
7    let s = read_all_unchecked(reader);
8    let mut scanner = Scanner::new(&s);
9    scan!(
10        scanner,
11        _p: String,
12        _cnf: String,
13        n,
14        m,
15        ab: [(isize, isize, isize)]
16    );
17    let mut two_sat = TwoSatisfiability::new(n);
18    for (a, b, _) in ab.take(m) {
19        two_sat.add_clause(a.unsigned_abs() - 1, a >= 0, b.unsigned_abs() - 1, b >= 0);
20    }
21    if let Some(v) = two_sat.two_satisfiability() {
22        writeln!(writer, "s SATISFIABLE").ok();
23        write!(writer, "v").ok();
24        for (i, v) in v.into_iter().enumerate() {
25            write!(
26                writer,
27                " {}",
28                if v { i as i32 + 1 } else { -(i as i32 + 1) }
29            )
30            .ok();
31        }
32        write!(writer, " 0").ok();
33    } else {
34        writeln!(writer, "s UNSATISFIABLE").ok();
35    }
36}

Source

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

Examples found in repository ?

crates/library_checker/src/math/two_sat.rs (line 21)

6pub fn two_sat(reader: impl Read, mut writer: impl Write) {
7    let s = read_all_unchecked(reader);
8    let mut scanner = Scanner::new(&s);
9    scan!(
10        scanner,
11        _p: String,
12        _cnf: String,
13        n,
14        m,
15        ab: [(isize, isize, isize)]
16    );
17    let mut two_sat = TwoSatisfiability::new(n);
18    for (a, b, _) in ab.take(m) {
19        two_sat.add_clause(a.unsigned_abs() - 1, a >= 0, b.unsigned_abs() - 1, b >= 0);
20    }
21    if let Some(v) = two_sat.two_satisfiability() {
22        writeln!(writer, "s SATISFIABLE").ok();
23        write!(writer, "v").ok();
24        for (i, v) in v.into_iter().enumerate() {
25            write!(
26                writer,
27                " {}",
28                if v { i as i32 + 1 } else { -(i as i32 + 1) }
29            )
30            .ok();
31        }
32        write!(writer, " 0").ok();
33    } else {
34        writeln!(writer, "s UNSATISFIABLE").ok();
35    }
36}