1
require 'set'
2
3
# input = DATA.read
4
input = File.read('10.input')
5
6
def parse_z3(out)
7
state = :start
8
assertions = {}
9
fname = nil
10
out.scan(/[\w-]+|\(\)?|\)|\d+/).each do |x|
11
case state
12
when :start
13
if x == "sat"
14
state = :sat
15
else
16
raise "unknown token #{x} in start"
17
end
18
when :sat
19
if x == "("
20
state = :list
21
else
22
raise "unknown token #{x} in sat"
23
end
24
when :list
25
if x == "("
26
state = :assert
27
elsif x == ")"
28
state = :sat
29
else
30
raise "unknown token #{x} in list"
31
end
32
when :assert
33
if x == "define-fun"
34
state = :define_fun
35
else
36
raise "unknown token #{x} in assert"
37
end
38
when :define_fun
39
fname = x
40
state = :define_fun_args
41
when :define_fun_args
42
if x == "()"
43
state = :define_fun_type
44
else
45
raise "unknown token #{x} in define_fun_args"
46
end
47
when :define_fun_type
48
if x == "Int"
49
state = :define_fun_value
50
else
51
raise "unknown token #{x} in define_fun_type"
52
end
53
when :define_fun_value
54
assertions[fname] = x.to_i
55
state = :define_fun_end
56
when :define_fun_end
57
if x == ")"
58
state = :list
59
else
60
raise "unknown token #{x} in define_fun_end"
61
end
62
else
63
raise "unknown state #{state}"
64
end
65
end
66
if state != :sat
67
raise "unknown end state #{state}"
68
end
69
assertions
70
end
71
72
class MachineDescription
73
def self.parse(line)
74
md = line.match(%r{\A\[(?<lights>[.#]+)\] (?<buttons>(\([^)]+\) )+)\{(?<joltage>[^\}]+)\}\z})
75
new(
76
md[:lights].chars.map { |c| c == ?# },
77
md[:buttons].scan(/[0-9,]+/).map { |b| b.split(',').map(&:to_i) },
78
md[:joltage].split(',').map(&:to_i),
79
)
80
end
81
82
def initialize(lights, buttons, joltage)
83
@lights = lights
84
@buttons = buttons
85
@joltage = joltage
86
end
87
88
def solve!
89
z = +''
90
@buttons.each.with_index do |_b, bix|
91
z << "(declare-const #{(?a.ord + bix).chr} Int)\n"
92
z << "(assert (>= #{(?a.ord + bix).chr} 0))\n"
93
end
94
95
@joltage.each.with_index do |j, ix|
96
z << "(assert (= #{j} (+"
97
@buttons.each.with_index do |b, bix|
98
z << " #{(?a.ord + bix).chr}" if b.include?(ix)
99
end
100
z << ")))\n"
101
end
102
103
z << "(minimize (+"
104
@buttons.each.with_index do |_b, bix|
105
z << " #{(?a.ord + bix).chr}"
106
end
107
z << "))\n"
108
z << "(check-sat)\n"
109
z << "(get-model)\n"
110
111
File.write('tmp.smt', z)
112
start = Time.now
113
out = `z3 tmp.smt`
114
elapsed = Time.now - start
115
116
puts "==="
117
puts out
118
puts "==="
119
p elapsed
120
parsed = parse_z3(out)
121
p parsed
122
parsed.values.sum
123
end
124
end
125
126
descriptions = input.strip.split("\n").map { |l| MachineDescription.parse(l) }
127
128
s = descriptions.map.with_index do |d, ix|
129
puts "Solving #{ix}/#{descriptions.length}"
130
r = d.solve!
131
puts "=> #{r}"
132
r
133
end
134
p s
135
p s.sum
136
137
__END__
138
[.##.] (3) (1,3) (2) (2,3) (0,2) (0,1) {3,5,4,7}
139
[...#.] (0,2,3,4) (2,3) (0,4) (0,1,2) (1,2,3,4) {7,5,12,7,2}
140
[.###.#] (0,1,2,3,4) (0,3,4) (0,1,2,4,5) (1,2) {10,11,11,5,10,5}
141
