오픈 소스 모험: 에피소드 69: 수족관 퍼즐용 Crystal Z3 솔버

Aquarium은 다음 규칙이 있는 퍼즐입니다.

다양한 물통

에 속하는 셀 그리드가 있습니다.

각 셀은 물을 포함하거나 포함하지 않을 수 있음

각 컨테이너는 일정 수준까지 채워집니다. 즉, 컨테이너의 셀에 물이 있는 경우 동일한 컨테이너의 동일한 레벨 이하에 있는 모든 셀에도 물이 있습니다

.

지정된 행 또는 열에서 채워지는 셀 수를 지정하는 행 및 열 힌트가 있습니다

.

퍼즐에 익숙해지려면 몇 번 플레이하는 것이 좋습니다. 그러면 게시물을 더 쉽게 따라갈 수 있습니다.

수입자

늘 그렇듯이 큰 퍼즐의 모든 문자를 수동으로 입력하는 데 인내심이 없고 오류가 발생하기 쉬울 것이므로 Puzzle Team의 내부 형식에서 변환하는 임포터를 작성했습니다.

#!/usr/bin/env crystal

hints, board = ARGV[0].split(";", 2)
hints = hints.split("_")
size = hints.size // 2
top = hints[0, size]
left = hints[size, size]
board = board.split(",").map{|c| (96+c.to_i).chr}.join.scan(/.{#{size}}/).map(&.[0])
puts ["  #{top.join}\n\n", left.zip(board).map{|a,b| "#{a} #{b}\n"}.join].join

$ ./import_puzzle '5_3_1_3_3_5_5_3_4_4_2_3_4_4_4_6_3_2_2_6;1,1,1,1,2,3,3,4,4,5,1,6,6,6,2,7,4,4,5,5,1,8,8,2,2,7,4,4,5,9,10,10,10,11,2,7,12,12,9,9,13,13,10,11,11,11,12,14,14,9,15,13,10,10,16,12,12,12,12,12,15,13,10,10,16,12,17,17,17,17,15,13,10,10,16,18,18,18,18,17,19,10,10,16,16,20,18,17,17,17,19,10,10,16,20,20,18,18,18,17' > 1.txt

일반 텍스트 입력

결과는 다음과 같습니다.

  5313355344

2 aaaabccdde
3 afffbgddee
4 ahhbbgddei
4 jjjkbgllii
4 mmjkkklnni
6 omjjplllll
3 omjjplqqqq
2 omjjprrrrq
2 sjjpptrqqq
6 sjjpttrrrq

조금 덜 바쁘게 하기 위해 힌트와 보드 사이에 여분의 열과 행을 추가했습니다.

솔버

솔버는 다음과 같습니다.

#!/usr/bin/env crystal

require "z3"

class AquariumSolver
  @col_hints : Array(Int32)
  @row_hints : Array(Int32)
  @board : Array(Array(Char))
  @containers : Set(Char)

  def initialize(path)
    lines = File.read_lines(path)
    @col_hints = lines[0][2..].chars.map(&.to_i)
    @xsize = @col_hints.size
    @row_hints = lines[2..].map(&.[0].to_i)
    @ysize = @row_hints.size
    @board = lines[2..].map{|l| l[2..].chars}
    @containers = @board.flatten.to_set
    @solver = Z3::Solver.new
    @cells = {} of Tuple(Int32, Int32) => Z3::BoolExpr
    @water_levels = {} of Char => Z3::IntExpr
  end

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

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

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

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

    # Initialize water level variables
    # We could restrict it more tightly to make solution unambiguous
    # Right now container at levels 4-6 can have any level 0-10
    # even though 0-4 means same (all full), and 6-10 means same (all empty)
    @containers.each do |c|
      @water_levels[c] = v = Z3.int("level #{c}")
      @solver.assert v >= 0
      @solver.assert v <= @ysize
    end

    # All cells in each container have correct water level
    each_coord do |x, y|
      c = @board[y][x]
      @solver.assert @cells[{x,y}] == (y >= @water_levels[c])
    end

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

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

    # Print the solution
    if @solver.satisfiable?
      model = @solver.model
      @ysize.times do |y|
        @xsize.times do |x|
          v = (model[@cells[{x, y}]].to_s == "true")
          if v
            print "#"
          else
            print "."
          end
        end
        print "\n"
      end
    else
      puts "No solution"
    end
  end
end

AquariumSolver.new(ARGV[0]).call

솔버는 일반적으로 이전 솔버에서 이미 다룬 기술을 사용합니다.

수위 검사는 아래쪽이 0(의미적으로 더 이해가 되므로) 대신 위쪽이 0(일반 텍스트 입력이 인덱싱되는 방식)부터 계산하기 때문에 약간 직관적이지 않습니다

.

단순함을 위해 컨테이너의 수위가 0에서 MAX까지(컨테이너의 상단 위 또는 하단의 수위도 포함) 허용하므로 솔루션에 약간의 모호성이 생기고 더 엄격한 경계를 계산합니다. 그러나 우리는 수위가 아닌 결과의 세포에만 관심이 있기 때문에 여전히 잘 작동합니다.

결과

$ ./aquarium 1.txt
.....##...
.###......
......####
...##...##
...###...#
#....#####
##...#....
##........
#.....#...
#...#####.

지금까지의 이야기

All the code is on GitHub .

다음에 온다

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