오픈 소스 모험: 에피소드 66: 모자이크 퍼즐용 Crystal Z3 솔버

Mosaic Puzzle은 이전 에피소드에서 했던 Minesweeper Puzzle에 정말 가깝습니다.

논리적으로 유일한 차이점은 힌트 셀에 광산도 포함될 수 있다는 것입니다. 그런 이유로 "광산"대신 흑백 세포에 대해 이야기합니다.

우리가 겪게 될 어려움은 솔버가 아니라 출력과 관련될 것입니다.

shard.yml

먼저 Z3를 로드해야 합니다.

name: mosaic-solver
version: 0.0.1

dependencies:
  z3:
    github: taw/crystal-z3

솔버

솔버는 이전 에피소드에서 했던 Minesweeper의 솔버와 거의 동일합니다. 솔버 부분의 유일한 차이점은 @vars[{x, y}]?가 neighbourhood(x, y)에 포함된다는 것입니다. 더 이상 힌트 셀이 비어 있어야 한다고 주장하지 않습니다.

#!/usr/bin/env crystal

require "z3"

class MosaicSolver
  @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, y+1}]?,
      @vars[{x, y}]?,
      @vars[{x, y-1}]?,
      @vars[{x+1, y+1}]?,
      @vars[{x+1, y}]?,
      @vars[{x+1, 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
      end
    end
    ...
  end
end

solver = MosaicSolver.new(ARGV[0])
solver.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 v
            print "\e[30;104m"
          else
            print "\e[30;102m"
          end
          print c
        end
        print "\e[0m"
        print "\n"
      end
    else
      puts "No solution"
    end

결과

다음과 같습니다.

지금까지의 이야기

All the code is on GitHub .

다음에 온다

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