오픈 소스 모험: 에피소드 67: 텐트 퍼즐용 Crystal Z3 솔버

더 복잡한 퍼즐을 풀어봅시다 - Tents .

규칙은 다음과 같습니다.

셀 그리드가 있습니다. 텐트가 포함된 셀을 찾아야 합니다

.

퍼즐이 그리드 크기, 행 힌트, 열 힌트 및 트리 위치를 지정함

모든 행에는 해당 행에 몇 개의 텐트가 있는지에 대한 힌트가 있습니다

.

모든 열에는 해당 열에 몇 개의 텐트가 있는지 힌트가 있습니다

.

텐트 두 개는 닿지 않고, 대각선으로도 닿지 않는다

각 텐트는 1:1 대응

에서 옆에 있는 특정 나무에 속합니다(수평 또는 수직, 대각선 아님).

이 퍼즐을 한 번도 해본 적이 없다면 지금 몇 가지 작고 쉬운 퍼즐을 해보는 것이 좋습니다. 그러면 게시물을 더 쉽게 따라갈 수 있습니다.

대부분의 규칙은 솔버 코드로 변환하기에 매우 간단하지만 마지막 규칙은 약간 까다로울 것입니다.

퍼즐의 일반 텍스트 표현

매우 큰 퍼즐에는 여러 자리 힌트가 있을 수 있지만 간단하게 하기 위해 이 솔버는 힌트0 - 9 로 제한하겠습니다.

맨 위 행과 왼쪽 열은 힌트용입니다. 다른 모든 것은 빈 공간을 위한 .이고 나무를 위한 T입니다.

 151613232341607
5.T.T....T.T....
1.T.......T....T
4......T......T.
2...T..T........
4..T........TTT.
2T....T.T.......
2.........T..T..
3..T..........T.
2.T.........T..T
2........T...T..
4....TTT.T.....T
3.T.T..T........
4...........T.T.
1.T.T.T.T....T.T
6.T.........T...

수입자

물론 실수를 할 수도 있기 때문에 엄청난 수의 무작위 문자를 입력하고 싶지는 않습니다. 따라서 Importer를 작성하여 Puzzle Team 내부 형식을 일반 텍스트 표현으로 전환했습니다.

#!/usr/bin/env crystal

puzzle = ARGV[0].split(",")
size = (puzzle.size - 1) // 2
top = puzzle[1, size]
left = puzzle[-size..-1]
trees = puzzle[0]
map = trees.chars.map{|c| "." * ['_', *'a'..'z'].index(c).not_nil! }.join("T").scan(/.{#{top.size}}/).map(&.[0])
puts [" #{top.join}\n", left.zip(map).map{|a,b| "#{a}#{b}\n"}.join].join

$ crystal ./import_puzzle 'aadaegdffdbjh__adapbdjbibhcf__aeaabsabaaadaaic,1,5,1,6,1,3,2,3,2,3,4,1,6,0,7,5,1,4,2,4,2,2,3,2,2,4,3,4,1,6'  > 1.txt

형식은 매우 간단합니다. 첫 번째 섹션은 트리 사이에 얼마나 많은 공간이 있는지에 대한 기호 문자열입니다(0의 경우 _, 1의 경우 a, 2의 경우 b 등), 쉼표로 구분된 힌트입니다.

변수

그리드의 모든 공간에 대해 하나의 변수가 확실히 필요합니다. 그곳에 텐트가 있으면 true, 그렇지 않으면 false입니다. 이것은 마지막 규칙을 제외한 대부분의 규칙을 다룹니다.

트리에 대한 규칙에는 추가 변수가 필요합니다. 각 셀에 대한 숫자 0-4. 트리가 없으면 0입니다. 북쪽에 천막이 있는 나무가 있으면 1, 동쪽에 2, 남쪽에 3, 서쪽에 4입니다. 정확한 값은 여기에서 중요하지 않습니다. 각 방향에 대해 다른 값을 사용하는 한 여기에서는 단순성을 위해 시계 방향으로 진행합니다.

그것으로 우리는 코딩을 할 수 있습니다!

솔버

이제 접근 방식이 있으므로 솔버를 작성해 보겠습니다.

#!/usr/bin/env crystal

require "z3"

class TentsSolver
  @ysize : Int32
  @xsize : Int32
  @row_hints : Array(Int32)
  @col_hints : Array(Int32)
  @trees : Array(Array(Bool))

  def initialize(path)
    lines = File.read_lines(path)
    @col_hints = lines.shift[1..-1].chars.map(&.to_i)
    @xsize = @col_hints.size
    @row_hints = lines.map(&.[0].to_i)
    @ysize = @row_hints.size
    @trees = lines.map{|l| l[1..-1].chars.map{|c| c == 'T'}}
    @solver = Z3::Solver.new
    @tent_vars = {} of Tuple(Int32, Int32) => Z3::BoolExpr
    @tree_vars = {} of Tuple(Int32, Int32) => Z3::IntExpr
  end

  def each_coord
    @xsize.times do |x|
      @ysize.times do |y|
        yield(x, y)
      end
    end
  end

  def row_tent_count(y)
    (0...@xsize).map{|x| @tent_vars[{x,y}].ite(1, 0)}.reduce{|a,b| a+b}
  end

  def col_tent_count(x)
    (0...@ysize).map{|y| @tent_vars[{x,y}].ite(1, 0)}.reduce{|a,b| a+b}
  end

  def neighbourhood(x,y)
    [
      @tent_vars[{x, y+1}]?,
      @tent_vars[{x, y-1}]?,
      @tent_vars[{x+1, y+1}]?,
      @tent_vars[{x+1, y}]?,
      @tent_vars[{x+1, y-1}]?,
      @tent_vars[{x-1, y+1}]?,
      @tent_vars[{x-1, y}]?,
      @tent_vars[{x-1, y-1}]?,
    ].compact
  end

  def call
    # Initialize tent variables
    each_coord do |x, y|
      @tent_vars[{x,y}] = Z3.bool("tent #{x},#{y}")
    end

    # Initialize tree variables
    each_coord do |x, y|
      @tree_vars[{x,y}] = v = Z3.int("tree #{x},#{y}")
      if @trees[y][x]
        @solver.assert v >= 1
        @solver.assert v <= 4
      else
        @solver.assert v == 0
      end
    end

    # Row hints are correct
    @ysize.times do |y|
      @solver.assert row_tent_count(y) == @row_hints[y]
    end

    # Col hints are correct
    @xsize.times do |x|
      @solver.assert col_tent_count(x) == @col_hints[x]
    end

    # No two tents are next to each other
    each_coord do |x,y|
      neighbourhood(x,y).each do |nv|
        @solver.assert @tent_vars[{x,y}].implies(~nv)
      end
    end

    # Every tree has corresponding tent
    each_coord do |x,y|
      v = @tree_vars[{x,y}]
      @solver.assert (v == 1).implies(@tent_vars[{x,y-1}]? || false) # N
      @solver.assert (v == 2).implies(@tent_vars[{x+1,y}]? || false) # E
      @solver.assert (v == 3).implies(@tent_vars[{x,y+1}]? || false) # S
      @solver.assert (v == 4).implies(@tent_vars[{x-1,y}]? || false) # W
    end

    # Now print the solution
    if @solver.check
      model = @solver.model
      @ysize.times do |y|
        @xsize.times do |x|
          v = (model[@tent_vars[{x, y}]].to_s == "true")
          if @trees[y][x]
            print "T"
          elsif v
            print "*"
          else
            print "."
          end
        end
        print "\n"
      end
    else
      puts "No solution"
    end
  end
end

TentsSolver.new(ARGV[0]).call

코드는 대부분 간단합니다. 몇 가지 흥미로운 부분은 다음과 같습니다.

Z3은 _.implies(false)를 잘 처리하므로 경계 검사를 할 필요는 없지만 여전히 nil를 false로 변환해야 합니다.

입력 구문 분석에는 _.implies(@tent_vars[{x,y-1}]? || false)와 같은 멋진 Crystal 트릭이 포함되어 있습니다.

유형 검사기를 만족시키려면 lines.map(&.[0].to_i)와 같이 변수에 대한 빈 해시를 초기화해야 합니다. 이것은 중첩 배열을 사용하는 것보다 경계 검사에 대한 논리가 훨씬 적게 필요합니다

.

결과

$ ./tents 1.txt
.T*T*...T*T.*.*
.T....*..T....T
.*.*..T..*...T*
...T..T*....*..
..T*.*....*TTT*
T*...T.T....*..
.......*.T*.T..
.*T*.........T*
.T......*..T*.T
......*.T...T.*
.*.*TTT.T*.*..T
.T.T.*T*......*
.*.*......*T*T.
.T.T.T.T*...T.T
*T.*.*....*T*.*

지금까지의 이야기

All the code is on GitHub .

다음에 온다

다음 몇 개의 에피소드에 걸쳐 Crystal 및 Z3에서 몇 가지 더 많은 퍼즐 게임 해결사를 코딩할 것입니다.