You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
30 lines
672 B
30 lines
672 B
places = (0..).lazy.map { 5 ** _1 }
|
|
digits = { ?- => -1, ?= => -2 }
|
|
|
|
sum = ARGF.read.lines(chomp: true)
|
|
.map {|snafu|
|
|
snafu.reverse.chars
|
|
.map { digits.fetch(_1, _1.to_i) }
|
|
.zip(places)
|
|
.map { _1 * _2 }
|
|
.sum
|
|
}.sum
|
|
|
|
n_places = places.slice_after { 2*_1 >= sum }.take(1).to_a.flatten.reverse
|
|
|
|
require "z3"
|
|
|
|
solver = Z3::Solver.new
|
|
|
|
n_places.each do |place|
|
|
solver.assert Z3.Int(place.to_s) <= 2
|
|
solver.assert Z3.Int(place.to_s) >= -2
|
|
end
|
|
solver.assert n_places.map { _1 * Z3.Int(_1.to_s) }.sum == sum
|
|
|
|
fail unless solver.satisfiable?
|
|
p n_places
|
|
.map { solver.model[Z3.Int(_1.to_s)].to_i }
|
|
.map { digits.invert.fetch(_1, _1) }
|
|
.join
|