Open Source Adventures: Episode 68: Crystal Z3 Solver for Switches Puzzle

This time something a bit different. I've seen variants of this puzzle as a minigame in a lot of hidden object games, but I haven't really seen it standalone anywhere.

Here's the puzzle:

• there's a bunch of light bulbs, each connected by lines to some other light bulbs
• some of the light bulbs start on, some start off
• each light bulb comes with a switches, but flipping it flips not just the one you want, but also every connected light bulb
• the goal is to turn all the light bulbs on

Shape of the connections, and visual representation differs from game to game. Sometimes you want to turn everything on, sometimes off, occasionally to form some specific pattern.

In principle switches could be independent from light bulbs, and connections could be one-sided, but it's not generally done so I won't cover it here.

It should be obvious that flipping a switch twice is the same as not flipping it, and order of flips doesn't matter, so the solution is simply a list of switches we need to flip.

Example

Here's a visual example of an instance of this puzzle:

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

There are 12 light bulbs, 4 of them already on. If we click on top left one, it will turn into this:

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

Plaintext format

We don't want to create a whole fancy ASCII art parser, so we'll turn this into a much simpler format.

To encode it, let's assign names to every node:

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

Here's how this puzzle would be encoded:

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

First line is list of all names (this is technically optional). Second line is list of all names that need to be flipped. All following lines are connections. It's not the most compact format, but it will do.

Variables

There are two sets of variables - one per switch, and one per light bulb.

For every light bulb variable we specify if it should be flipped or not. It is equal to XOR of all connected switches.

Switch variables are true if switch needs to be flipped. List of such variables is the solution.

Solver

#!/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

The solver is very straightforward. Some less usual things we do are:

• ^ xor operator
• Set{n} - Set literal with element n - in Ruby it would be Set[n]

Result

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

Which you can easily verify manually.

Story so far

All the code is on GitHub.

Coming next

Over the next few episodes I'll code a few more puzzle game solvers in Crystal and Z3.