True Knight

#!/usr/bin/env ruby

require "z3"

class TrueKnight
  def initialize
    @solver = Z3::Solver.new
  end

  def cell_x(i)
    Z3::Int("x#{i}")
  end

  def cell_y(i)
    Z3::Int("y#{i}")
  end

  def cell_n(i)
    Z3::Int("n#{i}")
  end

  def solve!
    (0...30).each do |i|
      @solver.assert cell_x(i) >= 0
      @solver.assert cell_x(i) <= 5
      @solver.assert cell_y(i) >= 0
      @solver.assert cell_y(i) <= 4
      @solver.assert cell_n(i) == cell_x(i) + 6 * cell_y(i) + 1
    end
    @solver.assert cell_n(0) == 1
    @solver.assert cell_n(3) == 18
    @solver.assert cell_n(6) == 25
    @solver.assert cell_n(10) == 12
    @solver.assert cell_n(18) == 20
    @solver.assert cell_n(27) == 6
    (0...30).each_cons(2) do |a,b|
      dx = cell_x(a) - cell_x(b)
      dy = cell_y(a) - cell_y(b)
      abs_dx = (dx > 0).ite(dx, -dx)
      abs_dy = (dy > 0).ite(dy, -dy)
      @solver.assert ((abs_dx == 1) & (abs_dy == 2)) | ((abs_dx == 2) & (abs_dy == 1))
    end
    @solver.assert Z3.Distinct(*(0...30).map{|i| cell_n(i)})

    if @solver.satisfiable?
      model = @solver.model
      puts "Oh yeah!"
      (0...30).each do |i|
        puts "#{i}: #{model[cell_n(i)]} (#{model[cell_x(i)]},#{model[cell_y(i)]})"
      end
      # 0th at (0,0) is prefilled, only clicked ones get added to solution
      puts (1...30).map{|i| model[cell_n(i)].to_s }.join
      # 95182921251431612232719841572028241122261321061730
    else
      puts "Can't be solved"
    end
  end
end

TrueKnight.new.solve!