-
Notifications
You must be signed in to change notification settings - Fork 12
/
two_sat.cr
95 lines (83 loc) · 2.47 KB
/
two_sat.cr
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
# ac-library.cr by hakatashi https://github.com/google/ac-library.cr
#
# Copyright 2023 Google LLC
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
# https://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.
require "./scc.cr"
module AtCoder
# Implements [atcoder::two_sat](https://atcoder.github.io/ac-library/master/document_en/twosat.html)
#
# ```
# twosat = AtCoder::TwoSat.new(2_i64)
# twosat.add_clause(0, true, 1, false)
# twosat.add_clause(1, true, 0, false)
# twosat.add_clause(0, false, 1, false)
# twosat.satisfiable? # => true
# twosat.answer # => [false, false]
# ```
class TwoSat
getter size : Int64
class NotSatisfiableError < Exception
def initialize
super("The formula is not satisfiable")
end
end
def initialize(@size)
@scc = AtCoder::SCC.new(@size * 2)
@solved = false
@satisfiable = false
@group_list = Array(Int64).new(@size * 2, 0_i64)
end
@[AlwaysInline]
private def var(i, f)
if f
i.to_i64
else
i.to_i64 + @size
end
end
# Implements atcoder::two_sat.add_clause(i, f, j, g).
def add_clause(i, f, j, g)
@scc.add_edge(var(i, !f), var(j, g))
@scc.add_edge(var(j, !g), var(i, f))
end
# Implements atcoder::two_sat.satisfiable().
def satisfiable?
@satisfiable = false
groups = @scc.scc
@group_list = Array(Int64).new(@size * 2, 0_i64)
groups.each_with_index do |group, i|
group.each do |item|
@group_list[item] = i.to_i64
end
end
@size.times do |i|
if @group_list[i] == @group_list[i + @size]
return false
end
end
@satisfiable = true
end
# Implements atcoder::two_sat.answer().
#
# This method will raise `NotSatisfiableError` if it's not satisfiable.
def answer
unless @satisfiable
raise NotSatisfiableError.new
end
Array(Bool).new(@size) do |i|
@group_list.not_nil![i] > @group_list.not_nil![i + @size]
end
end
end
end