crystal-z3

A small announcement. Mostly as a way to play with Crystal, I created Crystal bindings for Z3 library, and I think it might be quite usable as a MVP.

Check included examples and specs for how to use it.

Architecture of z3 gem

This post is meant for people who want to dig deep into Z3 gem, or who want to learn from example how to interface with another complex C library. Regular users of Z3 are better off checking out some tutorials I wrote.

Architecture of z3 gem The z3 theorem prover is a C library with quite complex API, and z3 gem needs to take a lot of steps to provide good ruby experience with it.

Z3 C API Overview

The API looks conventional at first - a bunch of black box data types like Z3_context Z3_ast (Abstract Syntax Tree), and a bunch of functions to operate on them. For example to create a node representing equality of two nodes, you call:

Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r);

A huge problem is that so many of those calls claim to accept Z3_ast, but it needs to be particular kind of Z3_ast, otherwise you get a segfault. It's not even static limitation - l and r can be anything, but they must represent the same type. So any kind of thin wrapper is out of the question.

Very Low Level API

The gem uses ffi to setup Z3::VeryLowLevel with direct C calls. For example the aforementioned function is attached like this:

attach_function :Z3_mk_eq, [:ctx_pointer, :ast_pointer, :ast_pointer], :ast_pointer

There's 618 API calls, so it would be tedious to do it manually, so instead a tiny subproject lives in api and generates most of it with some regular expressions. A list of C API calls is extracted from Z3 documentation into api/definitions.h. They look like this:

def_API('Z3_mk_eq', AST, (_in(CONTEXT), _in(AST), _in(AST)))

Then api/gen_api script translates it into proper ruby code. It might seem like it could be handled by ffi library, but there are too many Z3-specific hacks needed. A small number of function calls can't be handled automatically, so they're written manually.

For example Z3_mk_add function creates a node representing addition of any number of nodes, and has signature of:

attach_function :Z3_mk_add, [:ctx_pointer, :int, :pointer], :ast_pointer

Low Level API

There's one intermediate level between raw C calls and ruby code. Z3::LowLevel is also mostly generated by api/gen_api. Here's an example of automatically generated code:

def mk_eq(ast1, ast2) #=> :ast_pointer
  VeryLowLevel.Z3_mk_eq(_ctx_pointer, ast1._ast, ast2._ast)
end

And this one is written manually, with proper helpers:

def mk_and(asts) #=> :ast_pointer
  VeryLowLevel.Z3_mk_and(_ctx_pointer, asts.size, asts_vector(asts))
end

A few things are happening here:

• Z3 API requires Z3_context pointer for almost all of its calls - we automatically provide it with singleton _ctx_pointer.
• We get ruby objects, and extract C pointers from them.
• We return C pointers FFI::Pointer and leave responsibility for wrapping them into ruby objects to the caller, as we actually don't have enough information here to do so.

Another thing Z3::LowLevel API does is setting up error callback, to convert Z3 errors into Ruby exceptions.

Ruby objects

And finally we get to ruby objects like Z3::AST, which is a wrapper for FFI::Pointer representing Z3_ast. Other Z3 C data types get similar treatment.

module Z3
  class AST
    attr_reader :_ast
    def initialize(_ast)
      raise Z3::Exception, "AST expected, got #{_ast.class}" unless _ast.is_a?(FFI::Pointer)
      @_ast = _ast
    end

    # ...

    private_class_method :new
  end
end

First weird thing is this Python-style pseudo-private ._ast. This really shouldn't ever be accessed by user of the gem, but it needs to be accessed by Z3::LowLevel a lot. Ruby doesn't have any concept of C++ style "friend" classes. I've chosen Python pseudo-private convention as opposed to a lot of .instance_eval or similar.

Another weird thing is that Z3::AST class prevents object creation - only its subclasses representing nodes of specific type can be instantiated.

Sorts

Z3 ASTs represent multiple things, mostly sorts and expressions. Z3 automatically interns ASTs, so two identically-shaped ASTs will be the same underlying objects (like two same Ruby Symbols), saving us memory management hassle here.

Sorts are sort of like types. The gem creates a parallel hierarchy so every underlying sort gets an object of its specific class. For example here's whole Z3::BoolSort, which should only have a single object.

module Z3
  class Sort < AST
    def initialize(_ast)
      super(_ast)
      raise Z3::Exception, "Sorts must have AST kind sort" unless ast_kind == :sort
    end
    # ...

module Z3
  class BoolSort < Sort
    def initialize
      super LowLevel.mk_bool_sort
    end

    def expr_class
      BoolExpr
    end

    def from_const(val)
      if val == true
        BoolExpr.new(LowLevel.mk_true, self)
      elsif val == false
        BoolExpr.new(LowLevel.mk_false, self)
      else
        raise Z3::Exception, "Cannot convert #{val.class} to #{self.class}"
      end
    end

    public_class_method :new
  end
end

ast_kind check is for additional segfault prevention.

BoolSort.new creates Ruby object with instance variable _sort pointing to Z3_ast describing Boolean sort.

It seems a bit overkillish to setup so much structure for BoolSort with just two instance values, but some Sort classes have multiple Sort instances. For example Bit Vectors of width n are:

module Z3
  class BitvecSort < Sort
    def initialize(n)
      super LowLevel.mk_bv_sort(n)
    end

    def expr_class
      BitvecExpr
    end    

Expressions

Expressions are also ASTs, but they all carry reference to Ruby instance of their sort.

module Z3
  class Expr < AST
    attr_reader :sort
    def initialize(_ast, sort)
      super(_ast)
      @sort = sort
      unless [:numeral, :app].include?(ast_kind)
        raise Z3::Exception, "Values must have AST kind numeral or app"
      end
    end

This again might seem like an overkill for expressions representing Bool true, but it's extremely important for BitvecExpr to know if it's 8-bit or 24-bit. Because if they get mixed up, segfault.

Building Expressions

Expressions can be built from constants:

IntSort.new.from_const(42)

Declared as variables:

IntSort.new.var("x")

Or created from one or more of existing expression nodes:

module Z3
  class BitvecExpr < Expr
    def rotate_left(num)
      sort.new(LowLevel.mk_rotate_left(num, self))
    end

As you can see, the low level API doesn't know how to turn those C pointers into Ruby objects.

This interface is a bit tedious for the most common case, so there are wrappers with simple interface, which also allow mixing Z3 expressions with Ruby expressions, with a few limitations:

Z3::Int("a") + 2 == Z3::Int("b")

For some advanced use you actually need the whole interface.

Creating Sorts and Expressions from raw pointers

For ASTs we construct we track their sorts. Unfortunately sometimes Z3 gives us raw pointers and we need to guess their types - most obviously when we actually get a solution to our set of constraints.

Z3's introspection API lets us figure this out, and find out proper Ruby objects to connect to.

It has unfortunate limitation that we can only see underlying Z3 sorts. I'd prefer to have SignedBitvectorExpr and UnsignedBitvectorExpr as separate types with nice APIs, unfortunately there's no way to infer if answer Z3 gave came from Ruby SignedBitvectorExpr or UnsignedBitvectorExpr, so that idea can't work.

Printer

Expressions need to be turned into Strings for human consumption. Z3 comes with own printer, but it's some messy Lisp-like syntax, with a lot of weirdness for edge cases.

The gem instead implements its own printer in traditional math notation. Right now it sometimes overdoes explicit parentheses.

Examples

The gem comes with a set of small and intermediate examples in examples/ directory. They're a good starting point to learn common use cases.

There are obvious things like sudoku solvers, but also regular expression crossword solver.

Testing

Testing uses RSpec and has two parts.

Unit tests require a lot of custom matchers, as most objects in the gem override ==.

Some examples:

let(:a) { Z3.Real("a") }
let(:b) { Z3.Real("b") }
let(:c) { Z3.Real("c") }
it "+" do
  expect([a == 2, b == 4, c == a + b]).to have_solution(c => 6)
end

Integration tests run everything in examples and verify that output is exactly as expected. I like reusing other things as test cases like this.

Solving Self-Referential Aptitude Test with ruby and Z3

Previously, I wrote how to solve sudoku and nonograms with ruby and Z3.

Let's try something much more devious and complex - the Self-Referential Aptitude Test, a 20-question multiple-choice test where answers depend on other answers.

By the way the test is totally solvable by pen and paper, I'd say it should take about half an hour, and no excessive backtracking.

There's going to be a lot of code, but hopefully with my explanations it will all turn to be straightforward.

Basic structure

First, let's setup basic structure. Z3.Int("Q1") to Z3.Int("Q20") will be answers to the questions, with A being 1,  B being 2, C being 3, D being 4, and E being 5. I'm going to create a Hash storing question symbols, as we'll be using them a lot.

To make the code read more like DSL than a blob of math, I'm going to define a lot of helpers.

answer(10, "A") is expression stating that answer to question 10 is A.

define(10, "A") { expression } means that answer to question 10 can be A only if expression is true. Note that this is implication, not equality, as multiple answers could be valid - see question 19 for most extreme example.

require "z3"
class SelfRefPuzzleSolver
  attr_reader :q
  def initialize
    @solver = Z3::Solver.new
    @q = {}
    (1..20).each do |i|
      @q[i] = Z3.Int("Q#{i}")
      @solver.assert @q[i] >= 1
      @solver.assert @q[i] <= 5
    end
  end

  def answer(question_number, a)
    @q[question_number] == " ABCDE".index(a)
  end

  def define(question_number, a)
    @solver.assert answer(question_number, a).implies(yield)
  end

  def print_answers!
    raise "Something went wrong" unless @solver.satisfiable?
    model = @solver.model
    (1..20).each do |i|
      answer = " ABCDE"[model[q[i]].to_i]
      puts "Q#{'%2d' % i}: #{answer}"
    end
  end

  def solve!
    # Question code goes here
    print_answers!
  end
end

Code below goes inside solve! method, except for helpers which all go inside the class.

Counting answers

Many questions require counting how many times something is true - mainly how many questions have specific answer.

For this we convert Z3 Booleans (which are true or false) into 1s and 0s using statement.ite(if_true, if_false), and then add 1s together with Z3.Add. Z3.Add and friends aren't anything special, and you might just as well use .inject(&:+) etc. if you prefer.

  def count(*statements)
    Z3.Add(*statements.map{|b| b.ite(1,0)})
  end

  def count_answers(a, range=1..20)
    count(*range.map{|i| answer(i, a)})
  end

Question 1

The first question whose answer is B is question
    (A) 1
    (B) 2
    (C) 3
    (D) 4
    (E) 5

It's important to notice that answer like D means not only that "Q4 is B", but also that "Q1, Q2, and Q3 are not B".

    define(1, "A"){  answer(1, "B") }
    define(1, "B"){ !answer(1, "B") &
                     answer(2, "B") }
    define(1, "C"){ !answer(1, "B") &
                    !answer(2, "B") &
                     answer(3, "B") }
    define(1, "D"){ !answer(1, "B") &
                    !answer(2, "B") &
                    !answer(3, "B") &
                     answer(4, "B") }
    define(1, "E"){ !answer(1, "B") &
                    !answer(2, "B") &
                    !answer(3, "B") &
                    !answer(4, "B") &
                     answer(5, "B") }

Question 2

The only two consecutive questions with identical answers are questions
    (A) 6 and 7
    (B) 7 and 8
    (C) 8 and 9
    (D) 9 and 10
    (E) 10 and 11

There are shorter ways to write this answer, but let's just do it in the most straightforward way.
(1..20).each_cons(2) from ruby standard library generates a list of consecutive pairs. Then answer can be A if the only pair that's equal is 6 and 7, and so on.

    question_pairs = (1..20).each_cons(2)
    define(2, "A") {
      Z3.And(*question_pairs.map{|i,j| (q[i] == q[j]) == (i == 6) })
    }
    define(2, "B") {
      Z3.And(*question_pairs.map{|i,j| (q[i] == q[j]) == (i == 7) })
    }
    define(2, "C") {
      Z3.And(*question_pairs.map{|i,j| (q[i] == q[j]) == (i == 8) })
    }
    define(2, "D") {
      Z3.And(*question_pairs.map{|i,j| (q[i] == q[j]) == (i == 9) })
    }
    define(2, "E") {
      Z3.And(*question_pairs.map{|i,j| (q[i] == q[j]) == (i == 10) })
    }

Question 3

The number of questions with the answer E is
    (A) 0
    (B) 1
    (C) 2
    (D) 3
    (E) 4

Since we have a helper for counting how many of specific answer we've got, it's very straighforward:

    define(3, "A") { count_answers("E") == 0 }
    define(3, "B") { count_answers("E") == 1 }
    define(3, "C") { count_answers("E") == 2 }
    define(3, "D") { count_answers("E") == 3 }
    define(3, "E") { count_answers("E") == 4 }

Question 4

The number of questions with the answer A is
    (A) 4
    (B) 5
    (C) 6
    (D) 7
    (E) 8

This is basically the same as previous question.

    define(4, "A") { count_answers("A") == 4 }
    define(4, "B") { count_answers("A") == 5 }
    define(4, "C") { count_answers("A") == 6 }
    define(4, "D") { count_answers("A") == 7 }
    define(4, "E") { count_answers("A") == 8 }

Question 5

The answer to this question is the same as the answer to question
    (A) 1
    (B) 2
    (C) 3
    (D) 4
    (E) 5

Nothing complex here. Z3 has no problem with defining Q5 in terms of Q5.

    define(5, "A") { q[5] == q[1] }
    define(5, "B") { q[5] == q[2] }
    define(5, "C") { q[5] == q[3] }
    define(5, "D") { q[5] == q[4] }
    define(5, "E") { q[5] == q[5] }

Question 6

The answer to question 17 is 
    (A) C
    (B) D
    (C) E
    (D) none of the above
    (E) all of the above

A small trick here is that "none of the above" means "Q17 is A or B", and "all of the above" is nonsensical.

    define(6, "A") { answer(17, "C") }
    define(6, "B") { answer(17, "D") }
    define(6, "C") { answer(17, "E") }
    define(6, "D") { answer(17, "A") | answer(17, "B") }
    define(6, "E") { false }

Question 7

Alphabetically, the answer to this question and the answer to the following question are
    (A) 4 apart
    (B) 3 apart
    (C) 2 apart
    (D) 1 apart
    (E) the same

Answers are already encoded as numbers, so just subtracting them will get us alphabetic distance, but it has direction (like 3 or -3) while we want just magnitude (3 in both cases). We could either get absolute value with small helper or just spell out both cases. I'll use abs helper function.

  def abs(x)
    (x >= 0).ite(x, -x)
  end

Then the code becomes:

    distance_7_8 = abs(q[7] - q[8])
    define(7, "A") { distance_7_8 == 4 }
    define(7, "B") { distance_7_8 == 3 }
    define(7, "C") { distance_7_8 == 2 }
    define(7, "D") { distance_7_8 == 1 }
    define(7, "E") { distance_7_8 == 0 }

But this alternative isn't too bad:

    distance_7_8 = q[7] - q[8]
    define(7, "A") { (distance_7_8 == 4) | (distance_7_8 == -4) }
    define(7, "B") { (distance_7_8 == 3) | (distance_7_8 == -3) }
    define(7, "C") { (distance_7_8 == 2) | (distance_7_8 == -2) }
    define(7, "D") { (distance_7_8 == 1) | (distance_7_8 == -1) }
    define(7, "E") { distance_7_8 == 0 }

Question 8

The number of questions whose answers are vowels is
    (A) 4
    (B) 5
    (C) 6
    (D) 7
    (E) 8

We could just add A and E answers, or pass custom condition to count helper:

    count_vowel_answers = count_answers("A") + count_answers("E")
    define(8, "A") { count_vowel_answers == 4 }
    define(8, "B") { count_vowel_answers == 5 }
    define(8, "C") { count_vowel_answers == 6 }
    define(8, "D") { count_vowel_answers == 7 }
    define(8, "E") { count_vowel_answers == 8 }

Question 9

The next question with the same answer as this one is question
    (A) 10
    (B) 11
    (C) 12
    (D) 13
    (E) 14

Just as with question 1, we need 1+2+3+4+5 implications to cover it fully. This has similar structure to question 1, so maybe we could use a helper to DRY it up a bit. Here's we'll use the explicit version.

    define(9, "A") { Z3.And(q[9] == q[10]) }
    define(9, "B") { Z3.And(q[9] != q[10],
                            q[9] == q[11]) }
    define(9, "C") { Z3.And(q[9] != q[10],
                            q[9] != q[11],
                            q[9] == q[12]) }
    define(9, "D") { Z3.And(q[9] != q[10],
                            q[9] != q[11],
                            q[9] != q[12],
                            q[9] == q[13]) }
    define(9, "E") { Z3.And(q[9] != q[10],
                            q[9] != q[11],
                            q[9] != q[12],
                            q[9] != q[13],
                            q[9] == q[14]) }

Question 10

The answer to question 16 is
    (A) D
    (B) A
    (C) E
    (D) B
    (E) C

Completely straightforward.

    define(10, "A") { answer(16, "D") }
    define(10, "B") { answer(16, "A") }
    define(10, "C") { answer(16, "E") }
    define(10, "D") { answer(16, "B") }
    define(10, "E") { answer(16, "C") }

Question 11

The number of questions preceding this one with the answer B is
    (A) 0
    (B) 1
    (C) 2
    (D) 3
    (E) 4

This is same as counting E and A, except we limit the count to first 10 questions.

    preceding_B_answers = count_answers("B", 1..10)
    define(11, "A") { preceding_B_answers == 0 }
    define(11, "B") { preceding_B_answers == 1 }
    define(11, "C") { preceding_B_answers == 2 }
    define(11, "D") { preceding_B_answers == 3 }
    define(11, "E") { preceding_B_answers == 4 }

Question 12

The number of questions whose answer is a consonant is
    (A) an even number
    (B) an odd number
    (C) a perfect square
    (D) a prime
    (E) divisible by 5

This definitely demands a helper, and since we know counts will be between 0 and 20, it's just easier to list possible values instead of trying to come with formulas for "perfect square" or "prime".

    consonant_answers = count_answers("B") +
                        count_answers("C") +
                        count_answers("D")
    define(12, "A") {
      equals_one_of(consonant_answers, 0, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20)
    }
    define(12, "B") {
      equals_one_of(consonant_answers, 1, 3, 5, 7, 9, 11, 13, 15, 17, 19)
    }
    define(12, "C") {
      equals_one_of(consonant_answers, 0, 1, 4, 9, 16)
    }
    define(12, "D") {
      equals_one_of(consonant_answers, 2, 3, 5, 7, 11, 13, 17, 19)
    }
    define(12, "E") {
      equals_one_of(consonant_answers, 0, 5, 10, 15, 20)
    }

Question 13

The only odd-numbered problem with answer A is
    (A) 9
    (B) 11
    (C) 13
    (D) 15
    (E) 17

This of course means that problems 1, 3, 5, 7, and 19 can't have answer A.
We can use Range#step to generate list of odd numbers, and use similar code to question 2.

    odd_questions = 1.step(19, 2)
    define(13, "A") {
      Z3.And(*odd_questions.map{|i| answer(i, "A") == (i == 9) })
    }
    define(13, "B") {
      Z3.And(*odd_questions.map{|i| answer(i, "A") == (i == 11) })
    }
    define(13, "C") {
      Z3.And(*odd_questions.map{|i| answer(i, "A") == (i == 13) })
    }
    define(13, "D") {
      Z3.And(*odd_questions.map{|i| answer(i, "A") == (i == 15) })
    }
    define(13, "E") {
      Z3.And(*odd_questions.map{|i| answer(i, "A") == (i == 17) })
    }

The alternative is to reverse definitions and assert that answer(9, "A") is true if and only if answer(13, "A") etc., while all unlisted odd-numbered answers are not A. In this case we need to use ==, not implies.

    @solver.assert !answer(1, "A")
    @solver.assert !answer(3, "A")
    @solver.assert !answer(5, "A")
    @solver.assert !answer(7, "A")
    @solver.assert answer(9, "A") == answer(13, "A")
    @solver.assert answer(11, "A") == answer(13, "B")
    @solver.assert answer(13, "A") == answer(13, "C")
    @solver.assert answer(15, "A") == answer(13, "D")
    @solver.assert answer(17, "A") == answer(13, "E")
    @solver.assert !answer(19, "A")

Question 14

The number of questions with answer D is
    (A) 6
    (B) 7
    (C) 8
    (D) 9
    (E) 10
Same as questions 3 and 4.

    define(14, "A") { count_answers("D") == 6 }
    define(14, "B") { count_answers("D") == 7 }
    define(14, "C") { count_answers("D") == 8 }
    define(14, "D") { count_answers("D") == 9 }
    define(14, "E") { count_answers("D") == 10 }

Question 15

The answer to question 12 is
    (A) A
    (B) B
    (C) C
    (D) D
    (E) E
Straightforward:

    define(15, "A") { answer(12, "A") }
    define(15, "B") { answer(12, "B") }
    define(15, "C") { answer(12, "C") }
    define(15, "D") { answer(12, "D") }
    define(15, "E") { answer(12, "E") }

Question 16

The answer to question 10 is
    (A) D
    (B) C
    (C) B
    (D) A
    (E) E
Also straightforward:

    define(16, "A") { answer(10, "D") }
    define(16, "B") { answer(10, "C") }
    define(16, "C") { answer(10, "B") }
    define(16, "D") { answer(10, "A") }
    define(16, "E") { answer(10, "E") }

Question 17

The answer to question 6 is
    (A) C
    (B) D
    (C) E
    (D) none of the above
    (E) all of the above
Same logic as question 6, and notice how they refer to each other:

    define(17, "A") { answer(6, "C") }
    define(17, "B") { answer(6, "D") }
    define(17, "C") { answer(6, "E") }
    define(17, "D") { answer(6, "A") | answer(6, "B") }
    define(17, "E") { false }

Question 18

The number of questions with answer A equals the number of questions 
with answer
    (A) B
    (B) C
    (C) D
    (D) E
    (E) none of the above
We can use the same helper function, and only last case is different: 

    define(18, "A") { count_answers("A") == count_answers("B") }
    define(18, "B") { count_answers("A") == count_answers("C") }
    define(18, "C") { count_answers("A") == count_answers("D") }
    define(18, "D") { count_answers("A") == count_answers("E") }
    define(18, "E") {
      Z3.And(
        count_answers("A") != count_answers("B"),
        count_answers("A") != count_answers("C"),
        count_answers("A") != count_answers("D"),
        count_answers("A") != count_answers("E"),
      )
    }

Question 19

The answer to this question is:
    (A) A
    (B) B
    (C) C
    (D) D
    (E) E
This is a bit of a fake question as it's obvious that every answer works.

Of course if you want, you can add this do nothing code anyway:

    define(19, "A") { answer(19, "A") }
    define(19, "B") { answer(19, "B") }
    define(19, "C") { answer(19, "C") }
    define(19, "D") { answer(19, "D") }
    define(19, "E") { answer(19, "E") }

Question 20

Standardized test is to intelligence as barometer is to
    (A) temperature (only)
    (B) wind-velocity (only)
    (C) latitude (only)
    (D) longitude (only)
    (E) temperature, wind-velocity, latitude, and longitude
That's the only question that requires outside knowledge and the answer is obviously E.

We could list it the same way as other questions:

    define(20, "A") { false }
    define(20, "B") { false }
    define(20, "C") { false }
    define(20, "D") { false }
    define(20, "E") { true }

Or much more concisely:

    @solver.assert answer(20, "E")

Z3 is the ultimate TDD

If you wanted to write solver for Self-Referential Aptitude Test, you'd need to write something quite close to code above - syntax would be a bit different, and it would be slightly cleaner as you could use ruby values instead of Z3 expressions, but it wouldn't be much more code.

And then you'd need to write the solver itself - but here we don't have to - with fully specified problem Z3 generates the answer. The only thing we wrote were tests and a few lines to print the solution. That's as TDD as it gets.

Q 1: D
Q 2: A
Q 3: D
Q 4: B
Q 5: E
Q 6: D
Q 7: D
Q 8: E
Q 9: D
Q10: A
Q11: B
Q12: A
Q13: D
Q14: B
Q15: A
Q16: D
Q17: B
Q18: A
Q19: B
Q20: E

Z3 can do a lot more

I said it before, but I'll repeat it again - Z3 is great for a lot more than just solving puzzles. Puzzles simply make the best tutorial material.

If you're interested, you can find more examples in gem's repository. Or just try it yourself.

Solving nonograms with ruby and Z3

Z3 is quite amazing, and whenever I show it to people on various unconferences response is very enthusiastic, but it desperately needs some tutorials.

I wrote one for sudoku, but sudoku is maybe just a too straightforward example - variables are simply what goes into cells, and constraints are simply game rules. Usually you'll need at least a bit more modelling than that.

So let's try something just a bit more complicated - nonograms:

Nonograms are a puzzle where there's a grid of cells, either filed or empty.

Every row and column has numbers describing cells as seen from its own perspective. So if a row has numbers "2 7" next to it, it means there's a group of 2 filled cells, and then (with at least one empty cell gap) another group of 7 filled cells.

I'm going to refer to both rows and columns as "stripes", as logic for both is exactly the same, so it's simpler to just write it once.

Get the data

So the first thing we do is OCR that image... Just kidding, we'll transcribe it manually, as setting up proper OCR would take longer than that.

Of course in a real solver these numbers would come from somewhere - probably an HTML scrapper, but it could really be OCR, or something else altogether.

class NonogramSolver
  def initialize
    @row_constraints = [
      [3],
      [5],
      [3,1],
      [2,1],
      [3,3,4],
      [2,2,7],
      [6,1,1],
      [4,2,2],
      [1,1],
      [3,1],
      [6],
      [2,7],
      [6,3,1],
      [1,2,2,1,1],
      [4,1,1,3],
      [4,2,2],
      [3,3,1],
      [3,3],
      [3],
      [2,1],
    ]
    @column_constraints = [
      [2],
      [1,2],
      [2,3],
      [2,3],
      [3,1,1],
      [2,1,1],
      [1,1,1,2,2],
      [1,1,3,1,3],
      [2,6,4],
      [3,3,9,1],
      [5,3,2],
      [3,1,2,2],
      [2,1,7],
      [3,3,2],
      [2,4],
      [2,1,2],
      [2,2,1],
      [2,2],
      [1],
      [1],
    ]
    @row_count = @row_constraints.size
    @column_count = @column_constraints.size
    @solver = Z3::Solver.new
  end
end

Setting up cell variables

Z3 variables are basically just Symbols with types, and Z3's boolean sort already has the right range, so we don't need to do anything special. A helper function

For convenience let's write helpers to return row and column of such variables.

None of these functions are strictly necessary and it's totally reasonable to do such calculations where they're needed.

  def cell(x,y)
    Z3.Bool("cell#{x},#{y}")
  end

  def row(y)
    (0...@column_count).map{|x| cell(x,y) }
  end

  def column(x)
    (0...@row_count).map{|y| cell(x,y) }
  end

Express grid constraints as stripe constraints

Every stripe (row or column) is independent, so let's write our grid constraints in terms of constraints over individual stripes.

We're passing unique identifier like "row-4" or column-7 to the following function, as they'll need to setup some variables, which need to be unique, and such meaningful names make debugging easier than just allocating variable names at random.

  def setup_grid_constraints!
    (0...@column_count).each do |x|
      setup_stripe_constraints! "column-#{x}", @column_constraints[x], column(x)
    end

    (0...@row_count).each do |y|
      setup_stripe_constraints! "row-#{y}", @row_constraints[y], row(y)
    end
  end

Constraints for single stripe

Everything we've written so far was trivial, but here comes some real modelling. We have match group size constraints - an array like [4,2,2] with an array of boolean cell variables.

How would we model that? Here's one idea:

• For every group have its starting and ending cell as integer variable
• All starts and ends must fit within stripe size - between 0 and N-1 for stripe with N cells
• Difference between start and end equals group size minus one
• Difference between end of one group and start of the next is at least 2
• Cell is filled (true) if and only if it's between start and end of one of the groups

Here's the code for it:

  def setup_stripe_constraints!(stripe_name, stripe_constraints, stripe)
    group_count = stripe_constraints.size
    group_start = (0...group_count).map{|i| Z3.Int("#{stripe_name}-#{i}-start")}
    group_end = (0...group_count).map{|i| Z3.Int("#{stripe_name}-#{i}-end")}

    # Start and end of each group
    (0...group_count).each do |i|
      @solver.assert (group_start[i] >= 0) & (group_start[i] < stripe.size)
      @solver.assert (group_end[i] >= 0) & (group_end[i] < stripe.size)
      @solver.assert group_end[i] - group_start[i] == stripe_constraints[i] - 1
    end
    # Gap between each group and following group
    (0...group_count).each_cons(2) do |i,j|
      @solver.assert group_start[j] >= group_end[i] + 2
    end
    # Cells
    (0...stripe.size).each do |k|
      cell_in_specific_group = (0...group_count).map{|i|
        (k >= group_start[i]) & (k <= group_end[i])
      }
      @solver.assert stripe[k] == Z3.Or(*cell_in_specific_group)
    end
  end

The obvious alternative would be to make end variable point at cell after last, or to just have one variable for cell position, and do a bit more math.

Print the result

And that's it. Let's print the results, and while at it, why not use some Unicode to spice them up

  def solve!
    setup_grid_constraints!
    if @solver.satisfiable?
      model = @solver.model
      (0...@row_count).each do |y|
        (0...@column_count).each do |x|
          value = model[cell(x,y)].to_s
          print value == "true" ? "\u25FC" : "\u25FB"
        end
        print "\n"
      end
    else
      puts "Nonogram has no solution"
    end
  end

Results

Just as expected.

Next Steps

I'd strongly recommend everyone to play with Z3. Logic puzzles are definitely not its main application, they're just great for showing basic techniques without getting bogged down with details of real world problems.

The gem itself contains a collection of examples and you're definitely welcome to contribute more.

If posts like this one are popular, I can keep writing tutorials more increasingly more complex and realistic problems.

Solving sudoku with ruby and Z3

Solving Sudoku is a bit like FizzBuzz for constraint solvers, but since Z3 is very poorly known, and Z3 for ruby has few users other than me, I want to write a series of posts explaining various Z3 techniques, starting from very simple problems.

Parsing Sudoku

Before we get to Z3, let's read test data. A nice format for sudoku would be a text file like this:

_ 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 _

Where _s represent empty cells, and numbers represent pre-filled cells.

Fairly straightforward code like this can parse it to 9x9 Array of Arrays:

File.read(path).strip.split("\n").map do |line|
  line.split.map{|c| c == "_" ? nil : c.to_i}
end

Getting us data structure like this:

[[nil, 6, nil, 5, nil, 9, nil, 4, nil],
 [9, 2, nil, nil, nil, nil, nil, 7, 6],
 [nil, nil, 1, nil, nil, nil, 9, nil, nil],
 [7, nil, nil, 6, nil, 3, nil, nil, 9],
 [nil, nil, nil, nil, nil, nil, nil, nil, nil],
 [3, nil, nil, 4, nil, 1, nil, nil, 7],
 [nil, nil, 6, nil, nil, nil, 7, nil, nil],
 [2, 4, nil, nil, nil, nil, nil, 6, 5],
 [nil, 9, nil, 1, nil, 8, nil, 3, nil]]

Z3 workflow

First, we need to get the solver:

solver = Z3::Solver.new

After that we feed it with a bunch of formulas with solver.assert formula.
How would we describe sudoku problem in plain English?

• There are 9x9 integer variables
• Each of them is between 1 and 9
• They correspond to prefilled data, unless that data is nil
• Each row contains distinct values
• Each column contains distinct values
• Each 3x3 square contains distinct values

Once we tell Z3 about that, we check if our formulas are solvable with solver.check == :sat, and if it so, get model with solver.model - I feel those two steps should probably be refactored into one, but let's leave it for now.

Model can be then accessed with model[z3_variable] syntax to get our answers. So let's get to it!

Creating variables

There's nothing special about Z3 variables, they're sort of like ruby Symbols with associated types. So we could build our formulas with names like Z3.Int("cell[4,8]") - such name is just for our personal use, and doesn't mean cells form an array or anything.

However, since we'll be referring to the same 9x9 variables all the time it's probably useful to save them to an Array of Arrays.

cells = (0..8).map do |j|
  (0..8).map do |i|
    Z3.Int("cell[#{i},#{j}]")
  end
end

Setting possible values

All variables are between 1 and 9, which is very easy to tell the solver about:

cells.flatten.each do |v|
  solver.assert v >= 1
  solver.assert v <= 9
end

Setting prefilled variables

Telling solver that Z3 Int variable is equal to some ruby Integer is completely straightforward:

cells.each_with_index do |row, i|
  row.each_with_index do |var, j|
    solver.assert var == data[i][j] if data[i][j]
  end
end

All rows contain distinct values

If we relied on basic operations, we might have to give Z3 a lot of inequalities per row, fortunately there's Z3.Distinct(a,b,c,...) formula, which handles this very common case.

It makes it really easy:

cells.each do |row|
  solver.assert Z3.Distinct(*row)
end

All columns contain distinct values

We can use Array#transpose to flip our multidimensional array, and do the same thing we did for rows:

cells.transpose.each do |column|
  solver.assert Z3.Distinct(*column)
end

All square contain distinct values

This is a bit more complex rearrangement, but it's all pure ruby, with Z3 getting very similar looking formula in the end:

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

By the way, you should really take a look at Enumerable API, it contains a lot of useful methods which will save you a ton of time.

Get the model and print it

And we're basically done:

raise "Failed to solve" unless solver.check == :sat
model = solver.model
cells.each do |row|
  puts row.map{|v| model[v]}.join(" ")
end

Getting the answer we want:

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

Avoid temptation to optimize

Everything we did here was so ridiculously straightforward - we skipped even the most obvious shortcuts.

For example why the hell did we assert that cells are between 1 and 9 even for cells whose value we know perfectly well? And why did we even create variables for them if we know their value already? If we coded any kind of manual sudoku solver, we'd probably start with those.

It turns out Z3 really doesn't care about such optimizations, and will solve your problem just as efficiently either way - but by "optimizing" your code will become more complicated, and there's a good chance you'll make an error trying to "optimize".

That's not to say Z3 is made of magic, and that there are no cases where you can help it - but that's much more likely to be by restating a problem in a different way than by some microoptimizations.

Some pitfalls

One small pitfall to remember is that Z3 values - including those returned by solved models - override all operators including == so you can't check if for example model[Z3.Int("x")] == 5 - that will just create a Z3 Bool expression.

This is necessary behaviour for some more complex use cases, but for the simplest case you'll generally want to #to_s whatever you get out of the model and go on from there.

API is subject to change

Some details will probably change in future versions to simplify things - especially everything from solver.check onwards, which will probably receive a simpler API for the most common case, but existing one will still be supported as it's necessary for some more complex situations.

Integers variables constrained to specific range are another commonly used pattern which could use some shortcuts.

Z3 is crazy powerful

This was a very simple example. You could probably write a sudoku solver yourself - even if it'd take a lot more time, and would probably perform a lot worse than Z3.

This manual approach doesn't scale - doing much bigger and much more complex problems with a constraint solver is as literally fast as just writing the constraints, while doing it manually constraint list is barely a starting point, and naive approaches get exponentially slow almost right away.

Due to unfortunate accidents of programming history constraint solvers got relegated to an obscure niche, but they really ought to be a tool in every good programmer's toolkit, and once you learn them you'll find applications for them all the time.

Z3 Constraint Solver library for Ruby

Wouldn't it be awesome if you could just describe a problem to the computer, like let's say a sudoku, and it would find the answer for you?

That was the premise of "logic programming" in 1970s and 1980s, which was also one of many cases where Japan tried to do something else than everybody else, and failed, but it's not a post about history.

Logic programming suffered a lot worse than other paradigms. Lisp, Smalltalk, Perl, and friends left rich legacy of features for future programming languages to mine, but Prolog variants were all one big dead end.

Which is a bit of a shame, as some problems are really best coded by giving computer a list of constraints, and telling it to have a go at it, and it's very difficult to write a decent custom algorithm for them.

Technically you could use constraint solver libraries even without logic programming, but they were mostly only available in obscure Lisp / Prolog dialects, hard to compile on modern systems, barely documented, and/or extremely limited.

This somewhat changed with Z3 by Microsoft Research, which even got rudimentary Python interface.

But while Python is tolerable, I got tired of all the self. nonsense, and I wanted a nice Ruby DSL, so I wrote Ruby bindings. You can install them as z3 gem but first you need z3 library itself (brew install z3 or whatever works on your system).

If you want a quick look, check examples folder. If you want longer explanation, let's keep going.

Basic model

The basic Z3 workflow is:

• create solver with Z3::Solver.new
• create a bunch of formulas, generally starting with variables like Z3.Int("a"), Z3.Bool("b") etc. - formulas are independent of any solver, they're basically symbol trees.
• assert some facts about those variables, like solver.assert Z3.Int("a") == Z3.Int("b") + Z3.Int("c")
• ask solver to check if your set of formulas is satisfiable with solver.check. If it returns :sat, you're good to go.
• get Z3::Model with solver.model
• ask model for value of various variables with queries like model[Z3.Int("a")] etc.

Sorts

Let's go deeper, one step at a time. Values in Z3 all belong to "Sorts" which are sort of like types.

To create a Sort object, just instantiate its class, like Z3::BoolSort.new, then you can create relevant object like Z3::BoolSort.new.var("my_var") or Z3::IntSort.new.from_const(5). This seems like unnecessary indirection, and it sort of is for most common sorts, but there are fancier ones where it's necessary.

Some of the sorts are:

• Z3::BoolSort.new - boolean variables
• Z3::IntSort.new - integers, unlimited precision
• Z3::RealSort.new - real numbers, unlimited precision 
• Z3::BitvecSort.new(size) - bit vector sorts, of size bits
• Z3::FloatSort.new(esize, ssize) - floating point sort of esize exponent bits and ssize significand bits
• Z3::RoundingModeSort.new - floating point rounding mode sort
• Z3::SetSort.new(elemement_sort) - set sort of elements of elemement_sort sort
• Z3::ArraySort.new(key_sort, value_sort) - associative array sort with keys of key_sort, and values of value_sort
• there are some more sorts in Z3 which are not yet implemented

For vast majority of uses you want Bool and Int sorts, for physics style calculations you want Real sort (generally don't use Floats for them). They have decently completely and nice APIs.

Bitvec and Float sorts should work reasonably well, but their APIs are somewhat awkward - for example a lot of Bitvec operations have separate signed and unsigned operations, so you need to do awkward things like Z3.Bitvec("a", 32).signed_gt(100) instead of more obvious but ambiguous Z3.Bitvec("a", 32) > 100.

Float APIs are even worse as a lot of operations need rounding mode passed - and most operations take rounding mode argument, and printing out results tries to use precise but unintuitive notation like 1.25B+5.

Sets, Arrays, and fancier stuff, are basically unfinished.

The obvious missing sort is any kind of finite domain integer, like Int[1..9] - in Z3 you need to create Int variable, and then tell the solver that it's within certain range, like solver.assert (Z3.Int("a") >= 1) & (Z3.Int("a") <= 9)

ASTs

You want to give Z3 a bunch of formulas, and these generally start with variables like sort.var("name"). As Z3::BoolSort.new.var("name") is fairly long, shortcuts like Z3.Bool("name") are provided.

From that point, you can construct your formulas with fairly straightforward ruby - a + b == c means exactly what you'd expect if a is Z3.Int("a") and so on.

There are of course some complications:

• ruby won't let us override !, &&, and || - so we use ~, & and | for booleans - and they have different parsing priorities so you might need to add some parentheses
• you can't directly check if a value is equal to something else, as foo == 0 will create a z3 Bool expression not give you true/false. It's a great case where some extra operators would be useful, but for now just .to_s whatever you want to extract or check.
• some operations don't have easy operator equivalents, so other syntax is provided. For some common examples - to assert that a bunch of values are all different, you can use Z3.Distinct(a, b, c, ...), for z3 ternary use (bool_expression).ite(if_true, if_false).
• we'll automatically convert ruby values like true or 42 to z3 expressions, but if you try to mix sorts without converting them appropriately you'll generally get an exception
• ASTs are interned, so every Z3.Int("a") + 2 == Z3.Int("b") is going to be the same underlying object.

Library layers

Z3 is a huge library, and it really doesn't map to anything resembling a sensible ruby API, so there are many layers here:

• We use ffi to create Z3::VeryLowLevel interface of raw C calls. You should never use it directly.
• After that there's Z3::LowLevel interface which basically deals with context management, array arguments, and mapping Ruby object arguments (but not return values) to FFI pointers. You should also never use it directly.
• Then there are legitimate Ruby objects. A lot of them are wrappers around C pointers, so using SomeClass.new(c_pointer) to create them directly is not really supported. These pointers can be accessed by attributes starting with underscore (like _ast, _sort etc.), but it's all for internal use only.
• The main reason for this anal system is that if you mess anything up, you'll get a crash. For some things Z3 library raises error which we then turn into Z3::Exception, but other things just crash your program with segmentation fault. I added a lot of checks for operations which might end with segmentation fault so you get Z3::Exception instead, but I'm sure I missed some things.
• Reference counting memory management z3 uses is not exactly compatible with ruby, so if you use it in a very long running process like Rails server, it might cause problems. It's usually going to be no worse than Symbol interning.
• Default interface doesn't give any guarantees for running time. The underlying z3 library has ways to restrict solver check running time, but they're not exposed in any convenient way yet.

No semantic versioning

Z3 is huge library (I only described the basic), and the gem is not only incomplete, but many APIs are fairly poor.

Until I release 1.0, any version can freely break any API, so if you want to rely on a stable version, just depend on exact one - or help me complete it faster.

The regular flow with Bool, Int, Real and Solver shouldn't break too often, but Bitvec, Float etc. feel awkward and could use a nicer API.

Pull requests wellcome.