오픈 소스 모험: 에피소드 72: 도미노사 퍼즐용 Crystal Z3 솔버
늘 그렇듯이 퍼즐을 몇 번 플레이하여 좋은 느낌을 받는 것이 좋습니다. 쉽게 따라하실 수 있습니다.
이전 에피소드에서 설명한 대로 업데이트된 Crystal Z3 샤드를 사용하겠습니다.
일반 텍스트 입력
다음은 입력 예입니다.
77525629349
49071866039
82294832830
98723812246
50186000647
61556354899
56113420383
04114737281
06552340497
79171576958
솔버
#!/usr/bin/env crystal
require "z3"
class DominosaSolver
@board : Array(Array(Int32))
@xsize : Int32
def initialize(path)
@board = File.read_lines(path).map(&.chars.map(&.to_i))
@ysize = @board.size
@xsize = @board[0].size
@solver = Z3::Solver.new
@horizontal = {} of Tuple(Int32, Int32) => Z3::BoolExpr
@vertical = {} of Tuple(Int32, Int32) => Z3::BoolExpr
@dominos = {} of Tuple(Int32, Int32) => Array(Z3::BoolExpr)
end
def each_coord
@xsize.times do |x|
@ysize.times do |y|
yield(x,y)
end
end
end
def connections(x,y)
[
@horizontal[{x,y}]?,
@horizontal[{x-1,y}]?,
@vertical[{x,y}]?,
@vertical[{x,y-1}]?,
].compact
end
def add_domino(x1, y1, x2, y2, var)
v1 = @board[y1][x1]
v2 = @board[y2][x2]
v1, v2 = [v1, v2].sort
@dominos[{v1,v2}] ||= [] of Z3::BoolExpr
@dominos[{v1,v2}].push var
end
def call
# Setup horizontal variables
each_coord do |x,y|
next if x == @xsize - 1
@horizontal[{x,y}] = var = Z3.bool("h #{x},#{y}")
add_domino x, y, x+1, y, var
end
# Setup vertical variables
each_coord do |x,y|
next if y == @ysize - 1
@vertical[{x,y}] = var = Z3.bool("v #{x},#{y}")
add_domino x, y, x, y+1, var
end
# Each number belongs to exactly one domino
each_coord do |x,y|
@solver.assert 1 == Z3.add(connections(x,y).map{|v| v.ite(1,0)})
end
# Every type of domino has exactly one instance
@dominos.each do |type, vars|
@solver.assert 1 == Z3.add(vars.map{|v| v.ite(1,0)})
end
if @solver.satisfiable?
model = @solver.model
@ysize.times do |y|
@xsize.times do |x|
print @board[y][x]
next if x == @xsize - 1
print model[@horizontal[{x,y}]].to_b ? "*" : " "
end
print "\n"
next if y == @ysize - 1
@xsize.times do |x|
print model[@vertical[{x,y}]].to_b ? "*" : " "
next if x == @xsize - 1
print " "
end
print "\n"
end
else
puts "No solution"
end
end
end
DominosaSolver.new(ARGV[0]).call
우리는 확실히
Z3.add
와 적절하게 입력된Model#[]
을 활용하고 있습니다.솔버의 중요한 부분은
add_domino
방법과 인쇄입니다. Z3 솔버를 사용하면 입력 및 출력이 솔버 로직보다 더 복잡하다는 것이 상당히 일반적입니다.아마도 모든
next if x == @xsize - 1
블록은 적절한 이름의 도우미로 대체될 수 있습니다. 너무 복잡하지 않기를 바랍니다.결과
$ ./dominosa 1.txt
7*7 5*2 5 6*2 9*3 4*9
*
4 9 0 7 1 8 6*6 0 3 9
* * * * * * * *
8 2 2 9 4 8 3*2 8 3 0
*
9 8*7 2 3 8*1 2*2 4 6
* * * *
5 0*1 8 6*0 0*0 6 4 7
*
6*1 5*5 6*3 5*4 8 9*9
5 6 1 1*3 4*2 0*3 8*3
* * *
0 4 1 1*4 7*3 7*2 8 1
* *
0 6*5 5 2 3 4 0*4 9 7
* * * * *
7 9*1 7 1 5 7 6*9 5*8
지금까지의 이야기
All the code is on GitHub .
다음에 온다
다음 에피소드에서는 퍼즐 해결사를 하나 더 하고 다른 프로젝트로 넘어갈 시간입니다.
Reference
이 문제에 관하여(오픈 소스 모험: 에피소드 72: 도미노사 퍼즐용 Crystal Z3 솔버), 우리는 이곳에서 더 많은 자료를 발견하고 링크를 클릭하여 보았다 https://dev.to/taw/open-source-adventures-episode-72-crystal-z3-solver-for-dominosa-puzzle-1cca텍스트를 자유롭게 공유하거나 복사할 수 있습니다.하지만 이 문서의 URL은 참조 URL로 남겨 두십시오.
우수한 개발자 콘텐츠 발견에 전념 (Collection and Share based on the CC Protocol.)