Open Source Adventures: Episode 05: Sudoku Solver in Crystal Z3

All right, time to write a Sudoku Solver!

I wrote it probably 20 times by now in Ruby, as I did this so many times at unconferences and such, so I got one of them and tried to port it to Crystal Z3, filling in any missing functionality as I go.

Porting issues I encountered

I'll comment on code I wrote later, but first, here's some code I wanted to write, but couldn't.

There's nothing in Crystal like Ruby Pathname, and that's an APIs I like a lot. I found one on github (it looks like it's missing some features, but it's a start). For this is doesn't matter, as we just #read_lines, but I should take a look at this in the future. This is a case where Ruby's default APIs (File and Dir) are not great, but there's a really good one also included in the stdlib (Pathname).

Crystal has no __dir__, and I wanted to open "#{__dir__}/sudoku-1.txt" as default if no path argument was passed. __FILE__ exists, so in principle __dir__ could as well. It makes a bit less sense in compiled language, as things could be moved around by the time you run things, but it's fairly common to ship some data files or config files, especially with specs, and File.dirname(__FILE__) or such gets really tedious to do every single time, that's why Ruby added __dir__. Again, no big deal for this case, but might be an issue later.

A much bigger surprise was lack of Symbol interpolation, or any kind of dynamic Symbol creation for that matter. I tried to do Z3::IntSort[:"cell[#{i+1},#{j+1}]"] because :"..." works in Ruby and it's a fairly common pattern, but that does not work at all in Crystal. So I had to change the Crystal Z3 API, it now uses Strings not Symbols. The whole Symbol vs String situation in Ruby is a big mess, so I'm not surprised Crystal is doing things differently. Z3 uses interned Symbols everywhere, but they are all created dynamically at runtime, so they can't map to Crystal Symbols.

Sudoku Solver

Let's start from the end goal, here's the Sudoku Solver, ported from Ruby to Crystal with only modest changes:

#!/usr/bin/env crystal

require "./z3"

class SudokuSolver
  def initialize(path)
    @data = Array(Array(Int32 | Nil)).new
    @cells = Array(Array(Z3::IntExpr)).new
    @data = read_data(path)
    @solver = Z3::Solver.new
  end

  def call
    @cells = (0..8).map do |j|
      (0..8).map do |i|
        cell_var(@data[j][i], i, j)
      end
    end

    @cells.each do |row|
      @solver.assert Z3.distinct(row)
    end

    @cells.transpose.each do |column|
      @solver.assert Z3.distinct(column)
    end

    @cells.each_slice(3) do |rows|
      rows.transpose.each_slice(3) do |square|
        @solver.assert Z3.distinct(square.flatten)
      end
    end

    if @solver.satisfiable?
      print_answer
    else
      puts "failed to solve"
    end
  end

  def read_data(path)
    File.read_lines(path).map do |line|
      line.split.map{|c| c == "_" ? nil : c.to_i}
    end
  end

  def cell_var(cell, i, j)
    v = Z3::IntSort["cell[#{i+1},#{j+1}]"]
    @solver.assert v >= 1
    @solver.assert v <= 9
    @solver.assert v == cell if cell
    v
  end

  def print_answer
    model = @solver.model
    @cells.each do |row|
      puts row.map{|v| model[v]}.join(" ")
    end
  end
end

path = ARGV[0]? || "./sudoku-1.txt"
SudokuSolver.new(path).call

And here's example of Sudoku problem:

_ 6 _ 5 _ 9 _ 4 _
9 2 _ _ _ _ _ 7 6
_ _ 1 _ _ _ 9 _ _
7 _ _ 6 _ 3 _ _ 9
_ _ _ _ _ _ _ _ _
3 _ _ 4 _ 1 _ _ 7
_ _ 6 _ _ _ 7 _ _
2 4 _ _ _ _ _ 6 5
_ 9 _ 1 _ 8 _ 3 _

When we run it, it returns this:

$ ./sudoku.cr
8 6 3 5 7 9 2 4 1
9 2 5 3 1 4 8 7 6
4 7 1 8 2 6 9 5 3
7 1 4 6 8 3 5 2 9
6 8 9 7 5 2 3 1 4
3 5 2 4 9 1 6 8 7
1 3 6 2 4 5 7 9 8
2 4 8 9 3 7 1 6 5
5 9 7 1 6 8 4 3 2

I don't love declarations like @data = Array(Array(Int32 | Nil)).new and @cells = Array(Array(Z3::IntExpr)).new, other than that it's very clear what's going on.

I really like how much code Just Worked, like the whole each_slice/transpose/each_slice for squares.

Extracting data from the Model

The way Z3 works is - you send some assertions (expressions with symbols) to the Solver, then if it's possible, you get a Model back, which contains symbol to value mapping.

Then you can either iterate over that symbol to value mapping (which is honestly mostly useful for debugging), or ask model to evaluate various expressions for you.

This should generally return final values, but it doesn't have to. For example if assertions are: [a * b == 0], Z3 might just return {a: 0} as a model, as b is simplified away, so evaluating b will return b. When calling model_eval there's a flag if you want model to just return some value for all unknown variables instead (so it's effectively {a: 0, b: 0}) instead.

Once you go beyond integers and booleans, you can get a lot more complicated values returned.

Anyway, for now I didn't want to deal with any of this complexity, so model eval will just return Strings. You ask the model for some variable or expression, it will return "420" or "true" or such. This is good enough for a lot of cases.

Z3::LibZ3

I only added two entries:

fun model_eval = Z3_model_eval(ctx : Context, model : Model, ast : Ast, complete : Bool, result : Ast*) : Bool
fun ast_to_string = Z3_ast_to_string(ctx : Context, ast : Ast) : UInt8*

ast_to_string is simple enough. model_eval is a lot worse, as that's C hack for returning multiple values.

Z3::API

def ast_to_string(ast)
  String.new LibZ3.ast_to_string(Context, ast)
end

def model_eval(model, ast, complete)
  result_ptr = Pointer(LibZ3::Ast).malloc
  result = LibZ3.model_eval(Context, model, ast, complete, result_ptr)
  raise "Cannot evaluate" unless result == true
  # Full conversion is complicated, this is a good start
  ast_to_string result_ptr[0]
end

ast_to_string is completely unproblematic. I'm not really sure about model_eval. From what I understand that's how it's supposed to work in Crystal, and that result_ptr will get freed automatically.

Eventually we want this method to return Ast (that is struct Z3_Ast*), which then will be interrogated and wrapped in proper objects. That ast_to_string stuff is a placeholder.

Z3::Solver

I added just one method, satisfiable?, which returns true or false when results are known, and raises exception if Z3 returns unknown. In my experience that's the most useful interface, as for most problems unknowns are generally unexpected, and indicate programming error (or overly high expectation of what Z3 can handle).

Actually if you stick to simple types it's much more common to get "Z3 will tell you in a million years" result than unknown result, but there's no special handling for that.

def satisfiable?
  case check
  when LibZ3::LBool::True
    true
  when LibZ3::LBool::False
    false
  else
    raise "Unknown result"
  end
end

Z3::Model

def eval(expr, complete=false)
  API.model_eval(@model, expr._expr, complete)
end

def [](expr)
  eval(expr)
end

I'm not sure if default for complete should be true (return 0s for unknown variables) or false (return unknown variables unevaluated) and I should make some decision, as [] interface won't let you choose.

Story so far

All the code is in crystal-z3 repo.

We hit a few small problems, but Crystal Z3 is now sort of usable. Of course if you actually try to use it, you'll soon discover a lot of missing functionality.

Coming next

The library definitely needs tests - unit tests for each method, and integration tests (is Sudoku solver returning expected output etc.). Fortunately we can borrow both from the Ruby version.

One thing I'm not sure about is how to do negative type tests in Crystal. In Ruby I could do expect{ intVar + boolVal }.to raise_error(ArgumentError), but what do I even do in Crystal? expect{ intVar + boolVar }.to not_compile?

These are quite important, as they have to cover a lot of cases which DO type check in C API, but which segfault if we actually try them. It's our library's responsibility to make sure we're not mixing up expressions of different sorts, for C these are all Ast.