오픈 소스 모험: 에피소드 70: 노노그램 퍼즐용 Crystal Z3 솔버

Nonograms은 인기 있는 퍼즐 중 하나입니다.

셀 그리드가 있습니다. 그 중 일부를 채워야 합니다

.

각 행과 각 열에는 몇 가지 힌트가 있으며 각각은 숫자 목록입니다

.

"2 5 3"과 같은 힌트는 행(또는 열)에 3개의 채워진 셀 그룹(2개의 채워진 셀 그룹, 5개의 채워진 셀 그룹, 3개의 채워진 셀 그룹)이 있음을 의미합니다. 하나 이상의 빈 셀로 구분된 각 그룹

정규식 ^_*#{2}_+#{5}_+#{3}_+$에 해당하는

, _를 비어 있고 #를 채워진 공간

으로 취하면

늘 그렇듯이 퍼즐을 몇 번 플레이하여 좋은 느낌을 받는 것이 좋습니다. 쉽게 따라하실 수 있습니다.

일반 텍스트 입력

보드는 빈 상태로 시작하므로 보드가 필요하지 않습니다. 열 힌트와 행 힌트가 필요합니다.
- 선으로 구분합니다. 빈 줄이 더 분명하겠지만, 퍼즐은 행이나 열에 대한 빈 힌트를 합법적으로 포함할 수 있습니다(이 경우 채워진 셀이 없음).

다음은 25x25 퍼즐의 예입니다.

4 2 1 2 2
4 1 1 3
4 2 2 3
8 10
6 3 9
3 1 1 9
2 1 1 8
2 1 1 2 2 5
1 1 4 1 3
2 9 6
13 7
4 1 6 4 2
1 1 3 3 3
1 3 1 1 2
2 8 2
5 1 4 2
5 3 1 2
5 2 4
6 2 3
5 1 2
3 4 2
4 2 3 2
6 3 4 3
8 4 1
1 1 4 4
-
6 1 2
1 5 1 3
6 8 3
5 5 10
5 4 9
4 2 9
1 1 5 1
1 3 1 2 2
4 2 1 2
1 1 6 2
1 3 8
10
5 5 3
9 6
4 5 1 5
6 3 2 5
4 1
8
1 6 2 1
4 5 1
5 5 1 1
7 9 1
11 2 2 3
4 6 6
5 6

솔버

#!/usr/bin/env crystal

require "z3"

class Nonograms
  @col_hints : Array(Array(Int32))
  @row_hints : Array(Array(Int32))

  def initialize(path)
    col, row = File.read(path).split("-\n", 2)
    @col_hints = col.chomp.split("\n").map{|l| l.split.map(&.to_i)}
    @row_hints = row.chomp.split("\n").map{|l| l.split.map(&.to_i)}
    @xsize = @col_hints.size
    @ysize = @row_hints.size
    @solver = Z3::Solver.new
    @cells = {} of Tuple(Int32, Int32) => Z3::BoolExpr
  end

  def column_cells(x)
    (0...@ysize).map{|y| @cells[{x,y}]}
  end

  def row_cells(y)
    (0...@xsize).map{|x| @cells[{x,y}]}
  end

  def setup_groups(name, hints, cells)
    count = hints.size
    starts = (0...count).map{|i| Z3.int("#{name} start #{i}") }
    ends = (0...count).map{|i| Z3.int("#{name} end #{i}") }

    # Every group is on the board
    count.times do |i|
      @solver.assert starts[i] >= 0
      @solver.assert ends[i] <= cells.size
    end

    # Every group has correct size
    hints.each_with_index do |hint, i|
      @solver.assert starts[i] + hint == ends[i]
    end

    # There is a gap between groups
    (count-1).times do |i|
      @solver.assert starts[i+1] >= ends[i] + 1
    end

    # Each filled cell belongs to one of the groups
    cells.each_with_index do |c, j|
      cell_j_in_group_i = count.times.map{|i| (j >= starts[i]) & (j < ends[i]) }
      # this is fairly awkward and we should probably add Z3.or()
      cell_j_in_any_group = count == 0 ? false : cell_j_in_group_i.reduce{|a,b| a|b}
      @solver.assert c == cell_j_in_any_group
    end
  end

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

    # Setup groups
    @col_hints.each_with_index do |hints, x|
      setup_groups("c#{x}", hints, column_cells(x))
    end

    @row_hints.each_with_index do |hints, y|
      setup_groups("r#{y}", hints, row_cells(y))
    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

Nonograms.new(ARGV[0]).call

코드는 대부분 간단하지만 몇 가지 문제가 있습니다.

cell_j_in_any_group = count == 0 ? false : cell_j_in_group_i.reduce{|a,b| a|b} 계산은 정말 보기 흉합니다. 차라리 @solver.assert c == Z3.or(cell_j_in_group_i)와 같은 것을 보고 싶습니다. Z3.and , Z3.mul 및 Z3.add

이전 솔버와 마찬가지로 Z3::Model#[] 반환 유형을 보장하지 않는 것이 문제이며 (model[@cells[{x, y}]].to_s == "true") 대신 model[@cells[{x, y}]].to_b를 사용하는 것이 좋습니다. .to_i Z3 정수 및 비트 벡터에 대해 (BigInt 아님), Z3 실수에 대해 반환할 좋은 개체가 없습니다.

결과

$ ./nonograms 1.txt
...######......#......##.
#..#####.......#......###
######.....########..###.
#####..#####..##########.
#####....####..#########.
.####.....##....#########
...#......#....#####...#.
...#.....###..#...##..##.
....####.##...#......##..
#...#....######......##..
#...###..########........
.........##########......
.......#####..#####...###
.......#########...######
..####..#####.#.....#####
######..###.##......#####
...####.............#....
########.................
#.######..##....#........
...####.#####...........#
...#####.#####..#.......#
.#######.#########......#
###########...##.##...###
####..######.....######..
.......#####.....######..

지금까지의 이야기

All the code is on GitHub .

다음에 온다

몇 가지 퍼즐 게임 해결사를 더 하고 싶지만 먼저 Crystal Z3 샤드를 개선하여 지금까지의 문제를 해결하고 싶습니다.