Struct nekolib::math::TwoSat

pub struct TwoSat { /* private fields */ }

2-SAT。

$f(x_1, \dots, x_n) = \bigwedge (\bullet \vee \bullet)$ の形の論理式を $\top$ にするような $x_1, \dots, x_n$ の割り当てがあるか判定する。 ただし、各々の $\bullet$ は $x_1, \dots, x_n, \lnot x_1, \dots \lnot x_n$ のうちのいずれかである。

Examples

use nekolib::math::TwoSat;

let mut ts = TwoSat::new(4);
ts.add_clause(1, 1);
ts.add_clause(-2, -2);
ts.add_clause(3, -4);

let w = ts.witness().unwrap();
assert!(w[1]);
assert!(!w[2]);
assert!(w[3] || !w[4]);

ts.add_clause(-1, -1);
assert_eq!(ts.witness(), None);

Implementations

impl TwoSat

pub fn new(n: usize) -> Self

$f(x_1, \dots, x_n) = \top$ で初期化する。

Examples

use nekolib::math::TwoSat;

let ts = TwoSat::new(1);
assert!(ts.witness().is_some());

pub fn add_clause(&mut self, i: isize, j: isize)

$f(x_1, \dots, x_n) \xleftarrow{\wedge} (x_i \vee x_j)$ で更新する。

ただし、$i \lt 0$ のとき $x_i$ は $\lnot x_{-i}$ を指すとする。

Examples

use nekolib::math::TwoSat;

let mut ts = TwoSat::new(3);
ts.add_clause(-1, 2);
ts.add_clause(1, 3);

pub fn witness(&self) -> Option<Vec<bool>>

充足可能性を判定し、可能なら解を返す。

Examples

use nekolib::math::TwoSat;

let mut ts = TwoSat::new(3);
ts.add_clause(-1, 2);
ts.add_clause(-2, 3);
ts.add_clause(-3, -2);
let w = ts.witness().unwrap();
assert!(!w[1] || w[2]);
assert!(!w[2] || w[3]);
assert!(!w[3] || !w[2]);
// w == [_, false, false, true], for example.

ts.add_clause(2, 1);
assert_eq!(ts.witness(), None);