Struct TwoSat 

pub struct TwoSat { /* private fields */ }

A 2-SAT Solver.

For variables $x_0, x_1, \ldots, x_{N - 1}$ and clauses with from

\[ (x_i = f) \lor (x_j = g) \]

it decides whether there is a truth assignment that satisfies all clauses.

Example

#![allow(clippy::many_single_char_names)]

use ac_library::TwoSat;
use proconio::{input, marker::Bytes, source::once::OnceSource};

input! {
    from OnceSource::from(
        "3\n\
         3\n\
         a b\n\
         !b c\n\
         !a !a\n",
    ),
    n: usize,
    pqs: [(Bytes, Bytes)],
}

let mut twosat = TwoSat::new(n);

for (p, q) in pqs {
    fn parse(s: &[u8]) -> (usize, bool) {
        match *s {
            [c] => ((c - b'a').into(), true),
            [b'!', c] => ((c - b'a').into(), false),
            _ => unreachable!(),
        }
    }
    let ((i, f), (j, g)) = (parse(&p), parse(&q));
    twosat.add_clause(i, f, j, g);
}

assert!(twosat.satisfiable());
assert_eq!(twosat.answer(), [false, true, true]);

Implementations

impl TwoSat

pub fn new(n: usize) -> Self

Creates a new TwoSat of n variables and 0 clauses.

Constraints

• $0 \leq n \leq 10^8$

Complexity

• $O(n)$

pub fn add_clause(&mut self, i: usize, f: bool, j: usize, g: bool)

Adds a clause $(x_i = f) \lor (x_j = g)$.

Constraints

• $0 \leq i < n$
• $0 \leq j < n$

Panics

Panics if the above constraints are not satisfied.

Complexity

• $O(1)$ amortized

pub fn satisfiable(&mut self) -> bool

Returns whether there is a truth assignment that satisfies all clauses.

Complexity

• $O(n + m)$ where $m$ is the number of added clauses

pub fn answer(&self) -> &[bool]

Returns a truth assignment that satisfies all clauses of the last call of satisfiable.

Constraints

• satisfiable is called after adding all clauses and it has returned true.

Complexity

• $O(n)$

Trait Implementations

impl Clone for TwoSat

fn clone(&self) -> TwoSat

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for TwoSat

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.