오픈 소스 모험: 에피소드 68: 스위치 퍼즐용 Crystal Z3 솔버

이번에는 조금 다릅니다. 나는 많은 숨은 그림 찾기 게임에서 미니 게임으로 이 퍼즐의 변형을 보았지만 실제로는 어디에서도 독립적으로 본 적이 없습니다.

퍼즐은 다음과 같습니다.

여러 개의 전구가 있고 각각 다른 전구

에 선으로 연결되어 있습니다.

일부 전구가 켜지고 일부 전구가 꺼짐

각 전구에는 스위치가 있지만 뒤집으면 원하는 전구뿐만 아니라 연결된 모든 전구

도 뒤집힙니다.

목표는 모든 전구를 켜는 것입니다

.

연결의 모양과 시각적 표현은 게임마다 다릅니다. 때로는 모든 것을 켜고, 때로는 끄고, 때로는 특정 패턴을 형성하기를 원합니다.

원칙적으로 스위치는 전구와 독립적일 수 있고 연결은 일방적일 수 있지만 일반적으로 수행되지 않으므로 여기서 다루지 않겠습니다.

스위치를 두 번 뒤집는 것은 뒤집지 않는 것과 같고 뒤집는 순서는 중요하지 않으므로 솔루션은 단순히 뒤집는 데 필요한 스위치 목록입니다.

예시

다음은 이 퍼즐 인스턴스의 시각적 예입니다.

  o -- o -- * -- *
  |    |    |    |
  * -- o -- o -- o
  |    |    |    |
  o -- * -- o -- o

12개의 전구가 있고 그 중 4개는 이미 켜져 있습니다. 왼쪽 상단을 클릭하면 다음과 같이 바뀝니다.

  * -- * -- * -- *
  |    |    |    |
  o -- o -- o -- o
  |    |    |    |
  o -- * -- o -- o

일반 텍스트 형식

우리는 멋진 ASCII 아트 파서를 만들고 싶지 않으므로 이것을 훨씬 더 간단한 형식으로 바꿀 것입니다.

이를 인코딩하기 위해 모든 노드에 이름을 지정해 보겠습니다.

  a -- b -- c -- d
  |    |    |    |
  e -- f -- g -- h
  |    |    |    |
  i -- j -- k -- l

이 퍼즐을 인코딩하는 방법은 다음과 같습니다.

a b c d e f g h i j k l
a b       f g h i   k l
a b
b c
c d
e f
f g
g h
i j
j k
k l
a e
b f
c g
d h
e i
f j
g k
h l

첫 번째 줄은 모든 이름의 목록입니다(이는 기술적으로 선택 사항입니다). 두 번째 줄은 뒤집어야 하는 모든 이름의 목록입니다. 다음 줄은 모두 연결입니다. 가장 컴팩트한 형식은 아니지만 가능합니다.

변수

스위치당 하나와 전구당 하나의 두 가지 변수 세트가 있습니다.

모든 전구 변수에 대해 반전 여부를 지정합니다. 연결된 모든 스위치의 XOR과 같습니다.

스위치를 뒤집어야 하는 경우 스위치 변수는 true입니다. 그러한 변수의 목록이 해결책입니다.

솔버

#!/usr/bin/env crystal

require "z3"
require "set"

class SwitchesSolver
  @nodes : Array(String)
  @flipme : Set(String)

  def initialize(path)
    lines = File.read_lines(path).map(&.split)
    @nodes = lines.shift
    @flipme = lines.shift.to_set
    @connections = {} of String => Set(String)
    @nodes.each do |n|
      @connections[n] = Set{n}
    end
    lines.each do |(a, b)|
      @connections[a] << b
      @connections[b] << a
    end
    @solver = Z3::Solver.new
    @switches = {} of String => Z3::BoolExpr
    @lights = {} of String => Z3::BoolExpr
  end

  def call
    # Initialize variables
    @nodes.each do |n|
      @lights[n] = Z3.bool("light #{n}")
      @switches[n] = Z3.bool("switch #{n}")
    end

    # Set which lights should or should not be flipped
    @nodes.each do |n|
      if @flipme.includes?(n)
        @solver.assert @lights[n]
      else
        @solver.assert ~@lights[n]
      end
    end

    # Which switches affect which light
    @nodes.each do |n|
      @solver.assert @lights[n] == @connections[n].map{|nn| @switches[nn]}.reduce{|a,b| a^b}
    end

    if @solver.check
      model = @solver.model
      puts @nodes.select{|n| model[@switches[n]].to_s == "true" }.sort.join(" ")
    else
      puts "No solution"
    end
  end
end

SwitchesSolver.new(ARGV[0]).call

솔버는 매우 간단합니다. 우리가 하는 덜 일반적인 일은 다음과 같습니다.

^ xor 연산자

Set{n} - 요소로 리터럴 설정n - Ruby에서는 Set[n]

결과

$ ./switches 1.txt
a b e f g i j k

수동으로 쉽게 확인할 수 있습니다.

지금까지의 이야기

All the code is on GitHub .

다음에 온다

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