오픈 소스 모험: 에피소드 65: 지뢰 찾기 퍼즐용 Crystal Z3 솔버

몇 가지 퍼즐 해결사를 작성해 봅시다. 이번에는 - Minesweeper Puzzle .

Minesweeper 퍼즐은 처음부터 많은 지뢰 힌트가 제공된다는 점에서 Minesweeper 게임과 다릅니다. 게임에서 빈 보드로 시작하고 게임이 진행됨에 따라 힌트를 얻습니다.

일반 텍스트 입력

이러한 퍼즐에서 매우 중요한 것은 일종의 편리한 일반 텍스트 입력 형식을 갖는 것입니다. 퍼즐 중 일부는 이론상 단순하고 서류상으로는 단순해 보일 수도 있지만 I/O를 처리하는 것만으로도 많은 작업이 필요합니다.

다행스럽게도 Minesweeper는 정말 간단합니다.

1_2__0__1_
_2__2__2_1
____22____
__42__21_1
2____21___
22__2____2
__1__11___
_2__3__23_
___5_2__3_
1____2_3_1

힌트가 있는 상자는 숫자로 표시됩니다. 유일한 복잡성은 힌트 없이 빈 셀을 처리하는 것입니다. 공백을 사용하고 싶지만 의미 있는 후행 공백은 모든 종류의 문제를 일으키므로 대신 _ 또는 .와 같은 자리 표시자 문자를 사용하는 것이 좋습니다.

이러한 형식은 구문 분석하기가 매우 쉽습니다.

@data : Array(Array(Nil | Int32))
@data = File.read_lines(path).map{|l| l.chars.map{|c| c.ascii_number? ? c.to_i : nil}}

한 가지 유혹적인 것은 c =~ /\d/ Ruby와 같지만 c는 Char가 아니라 String이므로 Crystal에서는 작동하지 않습니다. 이 경우.ascii_number?는 완전히 괜찮습니다.

변수

지뢰 찾기 퍼즐의 변수는 매우 분명합니다. 모든 셀에는 부울 값이 있습니다. 지뢰가 있으면 true이고 그렇지 않으면 false입니다.

그것들을 담는 더 분명한 구조는 중첩된 배열Array(Array(Z3::BoolExpr))이지만, 그렇게 했다면 주어진 셀의 모든 이웃을 얻으려면 많은 경계 검사가 필요할 것입니다.

@vars = {} of Tuple(Int32, Int32) => Z3::BoolExpr

shard.yml

Z3 라이브러리를 가져와 시작하겠습니다.

name: minesweeper-solver
version: 0.0.1

dependencies:
  z3:
    github: taw/crystal-z3

솔버 구조

일부 인수가 전달되었는지 확인하고 멋진 오류 메시지를 인쇄할 수 있지만 간단하게 건너뛰겠습니다.

#!/usr/bin/env crystal

require "z3"

class MinesweeperSolver
  @data : Array(Array(Nil | Int32))
  @ysize : Int32
  @xsize : Int32

  def initialize(path)
    @data = File.read_lines(path).map{|l| l.chars.map{|c| c.ascii_number? ? c.to_i : nil}}
    @ysize = @data.size
    @xsize = @data[0].size
    @solver = Z3::Solver.new
    @vars = {} of Tuple(Int32, Int32) => Z3::BoolExpr
  end

  ...
end

solver = MinesweeperSolver.new(ARGV[0])
solver.call

변수 초기화

해결을 시작하기 위해 모든 변수를 Hash에 넣을 수 있습니다.

대부분의 퍼즐은 그리드를 따릅니다. 저는 each_coord와 같은 도우미 메서드를 사용하여 이중 중첩 루프를 반복하지 않도록 하는 것을 좋아합니다.

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

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

제약 조건 추가

한 가지 유형의 제약 조건만 있습니다. 셀이 힌트 셀인 경우 광산을 포함할 수 없으며 주위의 광산 수는 힌트와 같습니다.

변수를 이중 인덱스Hash로 유지하기 때문에 neighbourhood 방법이 정말 쉬워집니다.

숫자를 추가하기 전에 부울을 1로 변환하고 0를 사용하여 .ite로 변환하도록 Z3에 지시해야 합니다(if-then-else). v ? 1 : 0 연산자를 오버로드할 수 없다는 점을 제외하면 기본적으로 ?: 와 동일한 Z3입니다.

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

  def neighbourhood_count(x, y)
    neighbourhood(x, y).map{|v| v.ite(1, 0)}.reduce{|a,b| a+b}
  end

  def call
    ...
    each_coord do |x, y|
      c = @data[y][x]
      if c
        @solver.assert neighbourhood_count(x, y) == c
        @solver.assert ~@vars[{x,y}]
      end
    end
    ...
  end

인쇄 솔루션

이제 Z3가 해결을 처리할 수 있으며 솔루션을 인쇄하기만 하면 됩니다.
Z3::Models#[] 가 아직 완전히 입력되지 않았기 때문에 Crystal Z3는 반환되는 항목을 잘 모릅니다(Z3::BoolExpr ). 간단하게 하기 위해 .to_s == "true"를 사용하여 변수가 참인지 아닌지 확인합니다. 이것은 확실히 개선될 수 있습니다.

여기서는 each_coord를 사용할 수 없습니다. 각 라인의 끝에서 무언가를 해야 하기 때문입니다(print \n s).

  def call
    ...
    if @solver.check
      model = @solver.model
      @ysize.times do |y|
        @xsize.times do |x|
          v = (model[@vars[{x, y}]].to_s == "true")
          c = @data[y][x]
          if c
            print c
          elsif v
            print "*"
          else
            print " "
          end
        end
        print "\n"
      end
    else
      puts "No solution"
    end
  end

작동 중인 솔버

솔버가 작동하는 예는 다음과 같습니다.

$ ./minesweeper.cr 1.txt
1*2* 0  1
 2  2  2*1
 * *22*
 *42 *21 1
2*  *21  *
22  2   *2
* 1 *11*
 2 *3  23*
  *5*2 *3
1*** 2*3*1

풀 솔버 코드

다음은 완전한 솔버입니다.

#!/usr/bin/env crystal

require "z3"

class MinesweeperSolver
  @data : Array(Array(Nil | Int32))
  @ysize : Int32
  @xsize : Int32

  def initialize(path)
    @data = File.read_lines(path).map{|l| l.chars.map{|c| c.ascii_number? ? c.to_i : nil}}
    @ysize = @data.size
    @xsize = @data[0].size
    @solver = Z3::Solver.new
    @vars = {} of Tuple(Int32, Int32) => Z3::BoolExpr
  end

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

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

  def neighbourhood_count(x, y)
    neighbourhood(x, y).map{|v| v.ite(1, 0)}.reduce{|a,b| a+b}
  end

  def call
    each_coord do |x, y|
      @vars[{x, y}] = Z3.bool("#{x},#{y}")
    end
    each_coord do |x, y|
      c = @data[y][x]
      if c
        @solver.assert neighbourhood_count(x, y) == c
        @solver.assert ~@vars[{x,y}]
      end
    end
    if @solver.check
      model = @solver.model
      @ysize.times do |y|
        @xsize.times do |x|
          v = (model[@vars[{x, y}]].to_s == "true")
          c = @data[y][x]
          if c
            print c
          elsif v
            print "*"
          else
            print " "
          end
        end
        print "\n"
      end
    else
      puts "No solution"
    end
  end
end

solver = MinesweeperSolver.new(ARGV[0])
solver.call

지금까지의 이야기

All the code is on GitHub .

다음에 온다

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