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\) 充足不可能

実装

使い方

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());
    }
}