Skip to content

Commit 9591c79

Browse files
committed
Implement 'twosat'
1 parent 6d1e6a7 commit 9591c79

File tree

2 files changed

+36
-0
lines changed

2 files changed

+36
-0
lines changed

src/lib.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,3 +31,4 @@ pub use string::{
3131
lcp_array, lcp_array_arbitrary, suffix_array, suffix_array_arbitrary, suffix_array_manual,
3232
z_algorithm, z_algorithm_arbitrary,
3333
};
34+
pub use twosat::TwoSAT;

src/twosat.rs

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1 +1,36 @@
1+
use crate::internal_scc;
12

3+
pub struct TwoSAT {
4+
n: usize,
5+
scc: internal_scc::SccGraph,
6+
answer: Vec<bool>,
7+
}
8+
impl TwoSAT {
9+
pub fn new(n: usize) -> Self {
10+
TwoSAT {
11+
n,
12+
answer: vec![false; n],
13+
scc: internal_scc::SccGraph::new(2 * n),
14+
}
15+
}
16+
pub fn add_clause(&mut self, i: usize, f: bool, j: usize, g: bool) {
17+
assert!(i < self.n && j < self.n);
18+
self.scc
19+
.add_edge(2 * i + if f { 0 } else { 1 }, 2 * j + if g { 1 } else { 0 });
20+
self.scc
21+
.add_edge(2 * j + if f { 0 } else { 1 }, 2 * i + if g { 1 } else { 0 });
22+
}
23+
pub fn satisfiable(&mut self) -> bool {
24+
let id = self.scc.scc_ids().1;
25+
for i in 0..self.n {
26+
if id[2 * i] == id[2 * i + 1] {
27+
return false;
28+
}
29+
self.answer[i] = id[2 * i] < id[2 * i + 1];
30+
}
31+
true
32+
}
33+
pub fn answer(&self) -> &Vec<bool> {
34+
&self.answer
35+
}
36+
}

0 commit comments

Comments
 (0)