|
| 1 | +use super::strongly_connected_components::StronglyConnectedComponents as SCCs; |
| 2 | + |
| 3 | +pub type Condition = (i64, i64); |
| 4 | +type Graph = Vec<Vec<usize>>; |
| 5 | + |
| 6 | +#[inline] |
| 7 | +fn variable(var: i64) -> usize { |
| 8 | + if var < 0 { |
| 9 | + (((-var) << 1) + 1) as usize |
| 10 | + } else { |
| 11 | + (var << 1) as usize |
| 12 | + } |
| 13 | +} |
| 14 | + |
| 15 | +/// Returns an assignment that satisfies all the constraints, or a variable |
| 16 | +/// that makes such an assignment impossible. Variables should be numbered |
| 17 | +/// from 1 to n, and a negative number -m corresponds to the negated variable |
| 18 | +/// m. For more information about this problem, please visit: |
| 19 | +/// https://en.wikipedia.org/wiki/2-satisfiability |
| 20 | +pub fn solve_two_satisfiability( |
| 21 | + expression: &[Condition], |
| 22 | + num_variables: usize, |
| 23 | +) -> Result<Vec<bool>, i64> { |
| 24 | + let num_verts = (num_variables + 1) << 1; |
| 25 | + let mut result = Vec::new(); |
| 26 | + let mut sccs = SCCs::new(num_verts); |
| 27 | + let mut adj = Graph::new(); |
| 28 | + adj.resize(num_verts, vec![]); |
| 29 | + expression.iter().for_each(|cond| { |
| 30 | + let v1 = variable(cond.0); |
| 31 | + let v2 = variable(cond.1); |
| 32 | + adj[v1 ^ 1].push(v2); |
| 33 | + adj[v2 ^ 1].push(v1); |
| 34 | + }); |
| 35 | + sccs.find_components(&adj); |
| 36 | + result.resize(num_variables + 1, false); |
| 37 | + for var in (2..num_verts).step_by(2) { |
| 38 | + if sccs.component[var] == sccs.component[var ^ 1] { |
| 39 | + return Err((var >> 1) as i64); |
| 40 | + } |
| 41 | + // if a variable isn't |
| 42 | + if sccs.component[var] < sccs.component[var ^ 1] { |
| 43 | + result[var >> 1] = true; |
| 44 | + } |
| 45 | + } |
| 46 | + Ok(result) |
| 47 | +} |
| 48 | + |
| 49 | +#[cfg(test)] |
| 50 | +mod tests { |
| 51 | + use std::thread; |
| 52 | + |
| 53 | + use super::*; |
| 54 | + |
| 55 | + fn check_answer(expression: &[Condition], answers: &[bool]) -> bool { |
| 56 | + let mut ok = true; |
| 57 | + for &(c1, c2) in expression { |
| 58 | + let mut cv = false; |
| 59 | + if c1 < 0 { |
| 60 | + cv |= !answers[-c1 as usize]; |
| 61 | + } else { |
| 62 | + cv |= answers[c1 as usize]; |
| 63 | + } |
| 64 | + if c2 < 0 { |
| 65 | + cv |= !answers[-c2 as usize]; |
| 66 | + } else { |
| 67 | + cv |= answers[c2 as usize]; |
| 68 | + } |
| 69 | + ok &= cv; |
| 70 | + } |
| 71 | + ok |
| 72 | + } |
| 73 | + #[test] |
| 74 | + fn basic_test() { |
| 75 | + let conds = vec![(1, 1), (2, 2)]; |
| 76 | + let res = solve_two_satisfiability(&conds, 2); |
| 77 | + assert!(res.is_ok()); |
| 78 | + assert!(check_answer(&conds, &res.unwrap())); |
| 79 | + |
| 80 | + let conds = vec![(1, 2), (-2, -2)]; |
| 81 | + let res = solve_two_satisfiability(&conds, 2); |
| 82 | + assert!(res.is_ok()); |
| 83 | + assert!(check_answer(&conds, &res.unwrap())); |
| 84 | + |
| 85 | + let conds = vec![]; |
| 86 | + let res = solve_two_satisfiability(&conds, 2); |
| 87 | + assert!(res.is_ok()); |
| 88 | + assert!(check_answer(&conds, &res.unwrap())); |
| 89 | + |
| 90 | + let conds = vec![(-1, -1), (-2, -2), (1, 2)]; |
| 91 | + let res = solve_two_satisfiability(&conds, 2); |
| 92 | + assert!(res.is_err()); |
| 93 | + } |
| 94 | + |
| 95 | + #[test] |
| 96 | + #[ignore] |
| 97 | + fn big_test() { |
| 98 | + // We should spawn a new thread and set its stack size to something |
| 99 | + // big (256MB in this case), because doing DFS (for finding SCCs) is |
| 100 | + // a stack-intensive operation. 256MB should be enough for 3e5 |
| 101 | + // variables though. |
| 102 | + let builder = thread::Builder::new().stack_size(256 * 1024 * 1024); |
| 103 | + let handler = builder |
| 104 | + .spawn(|| { |
| 105 | + let num_conds = 3e5 as i64; |
| 106 | + let mut conds = vec![]; |
| 107 | + for i in 1..num_conds { |
| 108 | + conds.push((i, -(i + 1))); |
| 109 | + } |
| 110 | + conds.push((num_conds, num_conds)); |
| 111 | + let res = solve_two_satisfiability(&conds, num_conds as usize); |
| 112 | + assert!(res.is_ok()); |
| 113 | + assert!(check_answer(&conds, &res.unwrap())); |
| 114 | + }) |
| 115 | + .unwrap(); |
| 116 | + handler.join().unwrap(); |
| 117 | + } |
| 118 | +} |
0 commit comments