2-SAT

  1type twosat struct {
  2	scc *scc
  3	ans []bool
  4	n   int
  5}
  6
  7func newTwoSAT(n int) *twosat {
  8	return &twosat{
  9		newStronglyConnectedComponents(2 * n), make([]bool, n), n,
 10	}
 11}
 12
 13func (ts *twosat) AddClause(i int, f bool, j int, g bool) {
 14	p, q, a, b := 2*i, 2*j, 0, 0
 15	if f {
 16		a = 1
 17	}
 18	if g {
 19		b = 1
 20	}
 21	ts.scc.AddEdge(p+a^1, q+b)
 22	ts.scc.AddEdge(q+b^1, p+a)
 23}
 24
 25func (ts *twosat) Satisfiable() bool {
 26	ts.scc.Scc()
 27	cmp := ts.scc.cmp
 28	for i := 0; i < ts.n; i++ {
 29		if cmp[2*i] == cmp[2*i+1] {
 30			return false
 31		}
 32		ts.ans[i] = cmp[2*i] < cmp[2*i+1]
 33	}
 34	return true
 35}
 36
 37func (ts *twosat) Answer() []bool {
 38	return ts.ans
 39}
 40
 41type scc struct {
 42	g   [][]int
 43	rg  [][]int
 44	cmp []int
 45}
 46
 47func newStronglyConnectedComponents(n int) *scc {
 48	return &scc{
 49		make([][]int, n), make([][]int, n), make([]int, n),
 50	}
 51}
 52
 53func (s *scc) AddEdge(v, to int) {
 54	s.g[v] = append(s.g[v], to)
 55	s.rg[to] = append(s.rg[to], v)
 56}
 57
 58func (s *scc) Scc() [][]int {
 59	n := len(s.g)
 60	vs := make([]int, 0, n)
 61	vis := make([]bool, n)
 62
 63	var dfs func(v int)
 64	dfs = func(v int) {
 65		vis[v] = true
 66		for _, to := range s.g[v] {
 67			if !vis[to] {
 68				dfs(to)
 69			}
 70		}
 71		vs = append(vs, v)
 72	}
 73
 74	var rdfs func(v, k int)
 75	rdfs = func(v, k int) {
 76		vis[v] = true
 77		s.cmp[v] = k
 78		for _, to := range s.rg[v] {
 79			if !vis[to] {
 80				rdfs(to, k)
 81			}
 82		}
 83	}
 84
 85	for i := 0; i < n; i++ {
 86		if !vis[i] {
 87			dfs(i)
 88		}
 89	}
 90
 91	for i := 0; i < n; i++ {
 92		vis[i] = false
 93	}
 94
 95	k := 0
 96	for i := len(vs) - 1; i >= 0; i-- {
 97		if !vis[vs[i]] {
 98			rdfs(vs[i], k)
 99			k++
100		}
101	}
102
103	t := make([][]int, k)
104	for i := 0; i < n; i++ {
105		t[s.cmp[i]] = append(t[s.cmp[i]], i)
106	}
107
108	return t
109}
110