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.

Comments

[Ary Borenszweig]

Nice post as usual! I'm secretly waiting every day for your posts, because they are really fun and interesting :-) (well, I guess it's not a secret anymore)

Regarding the lack of Pathname, Crystal has something similar, it's called Path: crystal-lang.org/api/1.3.2/Path.html . We thought Path was a better, shorter name.

Then Crystal doesn't have __dir__, but it has __DIR__ that works exactly like the one in Ruby. We though it was a bit strange that Ruby had __FILE__ and then __dir__ so we made them both look the same. And they are both resolved at compile-time.

Regarding symbols vs. strings, I totally get you. We added symbols to Crystal in the very beginning just because Ruby has them. Eventually we introduced enums, and symbols had less reason to exist. Now I really wish to remove symbols from the language, and I hope we do that for 2.0. So my advice is to never use symbols.

Regarding asserting that something doesn't compile, there's no current way to do it. Well, you could write a test that runs the compiler binary with an output and expect it to give an error. I don't think there's any language that gives you the ability to check that something doesn't compile (I might be wrong!), but we do have a discussion around that (it started being related to responds_to?): github.com/crystal-lang/crystal/is... . I personally think having something like compiles? or compile_error would be great to have, especially because in Crystal you can produce hand-crafted compile errors.

[Tomasz Wegrzanowski]

Oh, __DIR__ makes perfect sense.

Pathname can be used as OO interface for filesystem objects, like Pathname("something").mkdir_p or Pathname("something").readlines. Path doesn't seem to have any of that.

expect{ ... }.to_not compile might be a bit much, but is there at least some way to do expect(intVar).to_not respond_to(:+, boolVar)? That's the only case I care about here, but these are fairly important checks as they prevent segfaults.

[Ary Borenszweig]

So Crystal's philosophy, unlike Ruby, is to avoid having too many ways to do the same thing. Crystal has Dir.mkdir_p that takes a String or Path, and that's the only way to do it. Having that in Path would be redundant, with all the downsides that brings (subjective!): discussions between developers around which way is better, or which one should be used here or there; then a larger binary because it's just redundant generated code; it might be slightly inefficient if one calls the other and the optimizer decides not to inline it, etc. That said, in this particular case it might not be that bad, so feel free to open a discussion around that in our forums :-)

And right now there's no way to do responds_to?(:method, args), you can only check if something responds to a method. But this might come later, even in a 1.x version!

[Brian J. Cardiff]

Lovely series! I have my own crystal-z3 which I am looking forward to mark it as archived if you want to maintain a shard for this!

Two things that I have in my mind regarding z3 in Crystal.

1. Hopefully we can make the ideas of youtube.com/watch?v=rTOqg-f2rNM possible in Crystal. Having a solver assist the developer in program creating sounds sci-fi to me still.

2. API related, Crystal does not allow overriding some binary operators || &&, cause they have typing implications. So there is a limit on how seamlessly the integration can look. But a possible way to solve this is via macros. Somthing like Z3.expr(a && b) could be a macro that translates Crystal syntax to Z3 api without needing && to be an actual call of the typeof(a). This might be useful for the previous point, since a and b could be either actual values or Z3 expressions depending on how the program is invoked.

[Tomasz Wegrzanowski]

My Ruby Z3 gem uses | & and .ite for booleans as ||, &&, and ?: are not possible to override. I think I'll need to do the same in Crystal.

[Tomasz Wegrzanowski]

I've taken a look at your version, and wrote a post about how they compare.