2-SAT
概要
\(n\) 個の真偽値変数 \(x_1, x_2, \ldots, x_n\) に関する 2-CNF とは次で表される論理式のこと: \[F = (v_1 \lor v_2) \land (v_3 \lor v_4) \land \cdots \land (v_{m-1} \lor v_m)\] ただしここで \(v_i\) は \(x_j\) または \(\lnot x_j\).
この式 \(F\) が適切な変数割当によって充足可能かどうか判定する問題を 2-SAT という.
充足判定
- \((A \lor B) \equiv (\lnot A \implies B) \equiv (\lnot B \implies A)\) であることを用いて 2-CNF を \(\land\) と \(\implies\) の式に変換する.
- 都合上 \((A \lor B)\) を \((\lnot A \implies B) \land (\lnot B \implies A)\) に置き換える.
- implication graph を構築する
- \(x_i\) 及び \(\lnot x_i\) が頂点
- \(A \implies B\) のときに有向エッジ \(A \to B\) を張る
- SCC したとき各連結成分は同値を表す
- その中に \(x_i\) と \(\lnot x_i\) が同時に属するかどうかが充足可能性
- 属する \(\iff\) 充足不可能
- その中に \(x_i\) と \(\lnot x_i\) が同時に属するかどうかが充足可能性
実装
使い方
let mut sat = TwoSAT::new(n); // 2CNF 上の変数 [0, 1, ..., n-1]
sat += and!(0 or 1); // AND 条件の追加: ... and (0 or 1)
sat += and!(not 1 or 2); // AND 条件の追加: ... and (not 1 or 2)
sat += and!(2 => not 1); // AND 条件の追加: ... and (2 => not 1)
let res = sat.solve(); // 充足可能かどうか
// and! に書けるもの
and!([not] x or [not] y)
and!([not] x => [not] y)
and!([not] x)use crate::graph::directed::scc::*;
pub struct TwoSAT {
n: usize,
graph: Vec<Vec<usize>>,
}
impl TwoSAT {
pub fn new(n: usize) -> Self {
let graph = vec![vec![]; n * 2];
Self { n, graph }
}
/// 充足判定
pub fn solve(&self) -> bool {
let (cmp, _) = scc(&self.graph);
for i in 0..self.n {
if cmp[i * 2] == cmp[i * 2 + 1] {
return false;
}
}
true
}
}
#[derive(Debug, Clone, Copy)]
pub struct TwoSATTerm(usize, bool);
impl TwoSATTerm {
fn val(&self) -> usize {
self.0 * 2 + if self.1 { 0 } else { 1 }
}
fn negate(&self) -> Self {
Self(self.0, true ^ self.1)
}
}
#[derive(Debug, Clone, Copy)]
pub enum TwoSATLogic {
Or(TwoSATTerm, TwoSATTerm),
Implies(TwoSATTerm, TwoSATTerm),
Iff(TwoSATTerm, TwoSATTerm),
}
impl std::ops::AddAssign<TwoSATLogic> for TwoSAT {
fn add_assign(&mut self, and: TwoSATLogic) {
match and {
TwoSATLogic::Implies(u, v) => {
self.graph[u.val()].push(v.val());
self.graph[v.negate().val()].push(u.negate().val());
}
TwoSATLogic::Or(u, v) => {
self.graph[u.negate().val()].push(v.val());
self.graph[v.negate().val()].push(u.val());
}
TwoSATLogic::Iff(u, v) => {
self.graph[u.val()].push(v.val());
self.graph[v.val()].push(u.val());
self.graph[u.negate().val()].push(v.negate().val());
self.graph[v.negate().val()].push(u.negate().val());
}
}
}
}
#[macro_export]
macro_rules! and {
(not $i:tt or not $j:tt) => {
TwoSATLogic::Or(TwoSATTerm($i, false), TwoSATTerm($j, false))
};
(not $i:tt or $j:tt) => {
TwoSATLogic::Or(TwoSATTerm($i, false), TwoSATTerm($j, true))
};
($i:tt or not $j:tt) => {
TwoSATLogic::Or(TwoSATTerm($i, true), TwoSATTerm($j, false))
};
($i:tt or $j:tt) => {
TwoSATLogic::Or(TwoSATTerm($i, true), TwoSATTerm($j, true))
};
(not $i:tt => not $j:tt) => {
TwoSATLogic::Implies(TwoSATTerm($i, false), TwoSATTerm($j, false))
};
(not $i:tt => $j:tt) => {
TwoSATLogic::Implies(TwoSATTerm($i, false), TwoSATTerm($j, true))
};
($i:tt => not $j:tt) => {
TwoSATLogic::Implies(TwoSATTerm($i, true), TwoSATTerm($j, false))
};
($i:tt => $j:tt) => {
TwoSATLogic::Implies(TwoSATTerm($i, true), TwoSATTerm($j, true))
};
(not $i:tt <=> not $j:tt) => {
TwoSATLogic::Iff(TwoSATTerm($i, false), TwoSATTerm($j, false))
};
(not $i:tt <=> $j:tt) => {
TwoSATLogic::Iff(TwoSATTerm($i, false), TwoSATTerm($j, true))
};
($i:tt <=> not $j:tt) => {
TwoSATLogic::Iff(TwoSATTerm($i, true), TwoSATTerm($j, false))
};
($i:tt <=> $j:tt) => {
TwoSATLogic::Iff(TwoSATTerm($i, true), TwoSATTerm($j, true))
};
(not $i:tt) => {
TwoSATLogic::Or(TwoSATTerm($i, false), TwoSATTerm($i, false))
};
($i:tt) => {
TwoSATLogic::Or(TwoSATTerm($i, true), TwoSATTerm($i, true))
};
}
#[cfg(test)]
mod test_two_sat {
use crate::misc::two_sat::*;
#[test]
fn test_two_sat_1() {
let mut sat = TwoSAT::new(3);
sat += and!(0 => 1);
sat += and!(1 => 2);
sat += and!(2 => 0);
assert!(sat.solve());
}
#[test]
fn test_two_sat_2() {
let mut sat = TwoSAT::new(2);
sat += and!(0 or 1);
sat += and!(0 => not 1);
sat += and!(1 => not 0);
assert!(sat.solve());
}
#[test]
fn test_two_sat_3() {
let mut sat = TwoSAT::new(2);
sat += and!(0 or 1);
sat += and!(not 0 or 1);
sat += and!(0 or not 1);
sat += and!(not 1 or not 0);
assert!(!sat.solve());
}
#[test]
fn test_two_sat_4() {
let mut sat = TwoSAT::new(2);
sat += and!(0 => 1);
sat += and!(1 => 0);
sat += and!(0 or 1);
sat += and!(not 0 or not 1);
assert!(!sat.solve());
}
#[test]
fn test_two_sat_5() {
let mut sat = TwoSAT::new(2);
sat += and!(0);
sat += and!(1);
assert!(sat.solve());
}
#[test]
fn test_two_sat_6() {
let mut sat = TwoSAT::new(2);
sat += and!(0);
sat += and!(not 0);
assert!(!sat.solve());
}
#[test]
fn test_iff_1() {
let mut sat = TwoSAT::new(3);
sat += and!(0 <=> 1);
sat += and!(not 1 <=> not 2);
sat += and!(2 <=> 0);
assert!(sat.solve());
}
#[test]
fn test_iff_2() {
let mut sat = TwoSAT::new(3);
sat += and!(0 <=> 1);
sat += and!(not 1 <=> 2);
sat += and!(2 <=> 0);
assert!(!sat.solve());
}
}