오픈 소스 모험: 에피소드 74: 라이트 업 퍼즐용 Crystal Z3 솔버

적어도 지금은 Crystal Z3 솔버의 마지막 에피소드입니다.

이전 에피소드에서 수학으로 Lights Up 퍼즐을 푸는 방법을 보여드렸으니 이제 Crystal Z3 솔버를 작성할 차례입니다.

Light Up (Akari)은 다음 규칙이 있는 간단한 퍼즐입니다.

셀 그리드가 있습니다

.

일부 세포는 벽세포

귀하의 임무는 일부 셀

에 전구를 배치하는 것입니다.

전구에서 빛이 수평 및 수직으로 퍼지지만 벽을 통과하지는 않습니다

모든 셀에 조명이 켜져 있어야 함

어떤 전구도 다른 전구를 비출 수 없습니다

일부 벽 셀에는 힌트(0-4)가 있어 얼마나 많은 전구가 벽 셀에 수평 또는 수직으로 직접 인접해 있는지 나타냅니다

.

퍼즐에 익숙해지려면 몇 번 플레이하는 것이 좋습니다.

수입자

늘 그렇듯이 큰 퍼즐을 수동으로 입력할 인내심이 없습니다. 다행스럽게도 Puzzle Team의 내부 형식은 매우 간단합니다.

B 벽용

힌트가 있는 벽의 경우 0 ~ 4

a ~ z 1~26개의 빈 공간 시퀀스

스크립트는 다음과 같습니다.

#!/usr/bin/env crystal

puzzle = ARGV[0].gsub(/[a-z]/){|c| "." * (c[0].ord - 96)}.gsub("B", "#")
size = (puzzle.size ** 0.5).to_i

puzzle.chars.each_slice(25) do |slice|
  puts slice.join
end

퍼즐 문자열을 인수로 전달하여 사용할 수 있습니다.

$ ./import_puzzle aBaB0fBfBBbBBaBaBaB1b10aBb0B1d2BaBBBBcB11cBe0BBBBBbBBcBgB0hBb2d0i1e1BBaBe1bBaBdBdBa1aBbBaBb2a3b2eB2f2e0g2a0aBcBjBaBdBb11bBaBb1pBb2a1dBa0cBb1Bk2fBfBc3Bb0cBaBb2aBb0a1cBbBBc1fBf2kB2b0cBa1dBa1bBp0bBa0b11b2d0a1j1cBaBaBgBe1f11e3b1aBb1aBb1aBaBd1dBa3bBe0a1BBe1i0dBbBhBBg1cBBbB1BB11e0c0BBcBBBBaB0dB1BbBaB2bB0aBaBaBBbBBfBfBBaBa

결과는 다음과 같습니다.

.#.#0......#......##..##.
#.#.#1..10.#..0#1....2#.#
###...#11...#.....0#####.
.##...#.......#0........#
..2....0.........1.....1#
#.#.....1..#.#....#....#.
1.#..#.#..2.3..2.....#2..
....2.....0.......2.0.#..
.#..........#.#....#..11.
.#.#..1................#.
.2.1....#.0...#..1#......
.....2......#......#...3#
..0...#.#..2.#..0.1...#..
##...1......#......2.....
......#2..0...#.1....#.1.
.#................0..#.0.
.11..2....0.1..........1.
..#.#.#.......#.....1....
..11.....3..1.#..1.#..1.#
.#....1....#.3..#.....0.1
##.....1.........0....#..
#........##.......1...##.
.#1##11.....0...0##...###
#.#0....#1#..#.#2..#0.#.#
.##..##......#......##.#.

솔버

코드는 다음과 같습니다.

#!/usr/bin/env crystal

require "z3"

class LightUp
  @xsize : Int32

  def initialize(path)
    @board = File.read_lines(path)
    @ysize = @board.size
    @xsize = @board[0].size
    @solver = Z3::Solver.new
    @cells = {} of Tuple(Int32, Int32) => Z3::BoolExpr
    @horizontal = {} of Tuple(Int32, Int32) => Z3::BoolExpr
    @vertical = {} of Tuple(Int32, Int32) => Z3::BoolExpr
    @members = {} of Z3::BoolExpr => Array(Z3::BoolExpr)
    @members.compare_by_identity
  end

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

  def neighbours_count(x, y)
    Z3.add(
      [
        @cells[{x+1,y}]?,
        @cells[{x-1,y}]?,
        @cells[{x,y+1}]?,
        @cells[{x,y-1}]?,
      ].compact.map{|v| v.ite(1,0)}
    )
  end

  def empty?(x, y)
    @board[y][x] == '.'
  end

  # Everything outside the board is a wall
  def empty_left?(x, y)
    x != 0 && empty?(x-1, y)
  end

  def empty_top?(x, y)
    y != 0 && empty?(x, y-1)
  end

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

    # Setup walls and hints
    each_coord do |x,y|
      c = @board[y][x]
      v = @cells[{x,y}]
      if c != '.'
        @solver.assert ~v
      end
      if c.ascii_number?
        @solver.assert neighbours_count(x, y) == c.to_i
      end
    end

    # Setup horizontal group variables
    each_coord do |x, y|
      next unless empty?(x, y)
      if empty_left?(x, y)
        # continue existing group
        @horizontal[{x,y}] = @horizontal[{x-1,y}]
      else
        # start a new group
        @horizontal[{x,y}] = Z3.bool("h #{x},#{y}")
        @members[@horizontal[{x,y}]] = [] of Z3::BoolExpr
      end
      @members[@horizontal[{x,y}]] << @cells[{x,y}]
    end

    # Setup vertical group variables
    each_coord do |x, y|
      next unless empty?(x, y)
      if empty_top?(x, y)
        # continue existing group
        @vertical[{x,y}] = @vertical[{x,y-1}]
      else
        # start a new group
        @vertical[{x,y}] = Z3.bool("v #{x},#{y}")
        @members[@vertical[{x,y}]] = [] of Z3::BoolExpr
      end
      @members[@vertical[{x,y}]] << @cells[{x,y}]
    end

    # Every cell sees a light - either in its horizontal or vertical group (or both)
    each_coord do |x, y|
      next unless empty?(x, y)
      @solver.assert(@horizontal[{x,y}] | @vertical[{x,y}])
    end

    # Group has a light if any of its members has a light
    @members.each do |var, members|
      @solver.assert var == Z3.or(members)
    end

    # No two lights see each other = no group has more than one light
    @members.each do |var, members|
      @solver.assert Z3.add(members.map{|v| v.ite(1,0)}) <= 1
    end

    if @solver.satisfiable?
      model = @solver.model
      @ysize.times do |y|
        @xsize.times do |x|
          c = @board[y][x]
          if c == '.'
            v = model[@cells[{x,y}]].to_b
            print v ? "*" : "."
          else
            print c
          end
        end
        print "\n"
      end
    else
      puts "No solution"
    end
  end
end

LightUp.new(ARGV[0]).call

재정의 비용 ==

그것의 대부분은 이전 에피소드에서 보여준 수학을 따릅니다. 코드 측면에서 가장 흥미로운 점은 Hash 로 인덱싱된 Z3::BoolExpr 입니다. Z3::BoolExpr가 ==를 재정의하여 Z3::BoolExpr s 대신에 Bool s를 반환하므로 실제로는 Hash 호환 유형이 아닙니다. 따라서 대신 @members.compare_by_identity 를 호출하여 object_id 비교로 전환합니다. 이는 이 사용 사례에 충분하지만 일반적으로는 아닙니다. 예를 들어 Hash 에 의해 인덱싱된 Tuple(Z3::BoolExpr, Z3::BoolExpr) , 완전히 합리적인 디자인을 원한다면 그 트릭은 작동하지 않을 것입니다.

그러한 객체Hash를 가능하게 만드는 것이 가능한지 잘 모르겠습니다. 제가 하고 있는 == 재정의에 상당한 비용이 듭니다. Z3.equal(a, b) 또는 solver.assert_equal(a, b) 를 수행했다면 이러한 문제가 발생하지 않았지만 표현식이 훨씬 더 나빠 보일 것입니다. API 설계 판단 호출입니다.

결과

$ ./light_up 2.txt
...*.
#*1.0
*.###

$ ./light_up 1.txt
*#*#0.*....#....*.##.*##*
#*#.#1.*10.#*.0#1...*2#*#
###..*#11..*#*....0#####*
*##...#.*.....#0.......*#
.*2*...0........*1.*...1#
#.#...*.1.*#*#.*..#...*#.
1.#.*#.#*.2*3.*2..*..#2*.
*...2.....0.*.....2.0.#..
.#..*.......#.#...*#.*11*
.#.#.*1..........*.....#.
.2*1....#.0.*.#..1#....*.
.*...2*.....#*.....#..*3#
..0..*#.#.*2*#..0.1*..#*.
##...1.*....#.*....2*....
..*...#2*.0.*.#.1*...#*1.
.#.........*......0..#.0.
*11*.2*...0.1*.........1*
..#.#*#..*....#....*1....
.*11...*.3*.1.#.*1.#..1*#
.#.*..1..*.#*3*.#.*...0.1
##....*1.....*...0..*.#.*
#.*......##....*..1*..##.
*#1##11*....0...0##..*###
#*#0.*..#1#*.#.#2*.#0.#*#
*##.*##..*...#..*...##*#*

지금까지의 이야기

All the code is on GitHub .

다음에 온다

그것은 마지막 Crystal Z3 솔버입니다. 다음 에피소드에서는 다른 기술을 시도해 보겠습니다.