오픈 소스 모험: 에피소드 72: 도미노사 퍼즐용 Crystal Z3 솔버

16033 단어 crystalz3
Dominosa은 간단한 규칙이 있는 퍼즐입니다.
  • 숫자로 채워진 격자가 있습니다
  • .
  • 해당 번호를 도미노
  • 로 페어링해야 합니다.
  • 도미노마다 달라야 함

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

    이전 에피소드에서 설명한 대로 업데이트된 Crystal Z3 샤드를 사용하겠습니다.

    일반 텍스트 입력



    다음은 입력 예입니다.

    77525629349
    49071866039
    82294832830
    98723812246
    50186000647
    61556354899
    56113420383
    04114737281
    06552340497
    79171576958
    


    솔버




    #!/usr/bin/env crystal
    
    require "z3"
    
    class DominosaSolver
      @board : Array(Array(Int32))
      @xsize : Int32
    
      def initialize(path)
        @board = File.read_lines(path).map(&.chars.map(&.to_i))
        @ysize = @board.size
        @xsize = @board[0].size
        @solver = Z3::Solver.new
        @horizontal = {} of Tuple(Int32, Int32) => Z3::BoolExpr
        @vertical = {} of Tuple(Int32, Int32) => Z3::BoolExpr
        @dominos = {} of Tuple(Int32, Int32) => Array(Z3::BoolExpr)
      end
    
      def each_coord
        @xsize.times do |x|
          @ysize.times do |y|
            yield(x,y)
          end
        end
      end
    
      def connections(x,y)
        [
          @horizontal[{x,y}]?,
          @horizontal[{x-1,y}]?,
          @vertical[{x,y}]?,
          @vertical[{x,y-1}]?,
        ].compact
      end
    
      def add_domino(x1, y1, x2, y2, var)
        v1 = @board[y1][x1]
        v2 = @board[y2][x2]
        v1, v2 = [v1, v2].sort
        @dominos[{v1,v2}] ||= [] of Z3::BoolExpr
        @dominos[{v1,v2}].push var
      end
    
      def call
        # Setup horizontal variables
        each_coord do |x,y|
          next if x == @xsize - 1
          @horizontal[{x,y}] = var = Z3.bool("h #{x},#{y}")
          add_domino x, y, x+1, y, var
        end
    
        # Setup vertical variables
        each_coord do |x,y|
          next if y == @ysize - 1
          @vertical[{x,y}] = var = Z3.bool("v #{x},#{y}")
          add_domino x, y, x, y+1, var
        end
    
        # Each number belongs to exactly one domino
        each_coord do |x,y|
          @solver.assert 1 == Z3.add(connections(x,y).map{|v| v.ite(1,0)})
        end
    
        # Every type of domino has exactly one instance
        @dominos.each do |type, vars|
          @solver.assert 1 == Z3.add(vars.map{|v| v.ite(1,0)})
        end
    
        if @solver.satisfiable?
          model = @solver.model
          @ysize.times do |y|
            @xsize.times do |x|
              print @board[y][x]
              next if x == @xsize - 1
              print model[@horizontal[{x,y}]].to_b ? "*" : " "
            end
            print "\n"
    
            next if y == @ysize - 1
    
            @xsize.times do |x|
              print model[@vertical[{x,y}]].to_b ? "*" : " "
              next if x == @xsize - 1
              print " "
            end
            print "\n"
          end
        else
          puts "No solution"
        end
      end
    end
    
    DominosaSolver.new(ARGV[0]).call
    


    우리는 확실히 Z3.add와 적절하게 입력된Model#[]을 활용하고 있습니다.

    솔버의 중요한 부분은 add_domino 방법과 인쇄입니다. Z3 솔버를 사용하면 입력 및 출력이 솔버 로직보다 더 복잡하다는 것이 상당히 일반적입니다.

    아마도 모든 next if x == @xsize - 1 블록은 적절한 이름의 도우미로 대체될 수 있습니다. 너무 복잡하지 않기를 바랍니다.

    결과




    $ ./dominosa 1.txt
    7*7 5*2 5 6*2 9*3 4*9
            *
    4 9 0 7 1 8 6*6 0 3 9
    * * * *   *     * * *
    8 2 2 9 4 8 3*2 8 3 0
            *
    9 8*7 2 3 8*1 2*2 4 6
    *     *           * *
    5 0*1 8 6*0 0*0 6 4 7
                    *
    6*1 5*5 6*3 5*4 8 9*9
    
    5 6 1 1*3 4*2 0*3 8*3
    * * *
    0 4 1 1*4 7*3 7*2 8 1
                      * *
    0 6*5 5 2 3 4 0*4 9 7
    *     * * * *
    7 9*1 7 1 5 7 6*9 5*8
    


    지금까지의 이야기



    All the code is on GitHub .

    다음에 온다



    다음 에피소드에서는 퍼즐 해결사를 하나 더 하고 다른 프로젝트로 넘어갈 시간입니다.

    좋은 웹페이지 즐겨찾기