Wednesday, 11 July 2012

N-Queens with core.logic, take 2

This post is a follow-up to my previous post on NQueens and core.logic, in which I tried to find the solutions using "pure" logic (without arithmetic goals) and basic minKanren / Reasoner Schemer building blocks.

After some excellent feedback and hints from Mr David Nolen (big thanks), I here present a greatly simplified (and faster) way of using core.logic to find all solutions. Credit also goes to good old Bratko.

First, let's fix the safeo function (and def-subo macro). In miniKanren, you can use arithmetic goals given 2 prerequisites; the fresh variable must be bound to a finite (number) space and we much use project to bind the values. This means we can get rid of subo altogether.

Project is mentioned in passing in the Reasoned Schemer book, it says "project is syntactically like fresh, but it binds different values to the lexical variables. project binds walk*ed values, whereas fresh binds variables using var". What that means in this case is that we can perform arithmetic operations of the projected variables. Here's our new safeo; This works if the x's as bound to number range with membero (remember that the y's are never fresh), this is done in a updated queens-run macro; As you can see, we got rid of subo (and all it's associations). That improves performance on a 6-queens run with ~5x

Next, we want to get rid of the big macro above and replace it with some readable looping constructs. To replicate the block of safeos generated by this macro (the gen-safeos fn), we are going to need 2 loops, one outer loop that goes over all N queens q, and one inner loop that for every q checks that it's safe against all other queens. Its time for some core.logic pattern matching magic!

Let's change safeo again. Instead of checking if 2 queens are not attacking each other, it checks if a given queen is not attacking any other queen in a given list (this is our inner loop); There's a couple of things going on here. defne is a convenience macro to build conde functions (which you end up doing all the time), secondly there are some clever destructing / pattern matching going on to pick the head / tail of a list and recur.

Now for the outer loop, let's introduce another recursive "conde function" called nqueenso, this function should loop over all queens in a list, check that they are all safe against each other (using safeo). It also needs to bind the x variables to a finite number space using membero; We're almost done now, we just to need rewrite the (run* ...) form. We can actually do without the (fresh ...) expression by creating core.logic logical variables (lvar) directly, this also eliminates the need for a macro to generate n symbols. Here's the whole thing; As you can see, with looping we are generating drastically less associations for core.logic to consider, that's good for performance.

Now it's ~70x faster than the original solution in the previous post. For a 8-queens run, this is ~50x slower than the hand-rolled functional backtracking solution in the very first posting. That's still pretty good for a generic prolog machinery with all the extra expression power that it packs.

Next part in this series will use cKanren functionality that is being worked on at the moment in core.logic. That might be even faster! 

4 comments:

  1. More fun with Z3 :)
    Here's the script in SMT for Z3, also tested on STP.
    http://rise4fun.com/Z3/kLSf

    Albeit only for 8 queen, but it is easy to write a small DSL to auto-generate the SMT expressions for arbitrary N.

    I ran this in a loop, adding an assert for each new solution.

    On my laptop timing to find all 92 solutions is :-)

    phil@phil:~/projects/8queens$ time ./run.sh 8queen.smt2
    real 0m12.308s
    user 0m9.761s
    sys 0m1.348s

    ReplyDelete
  2. Hm, 10s not to stellar; 500x slower than the hand-rolled Clojure version and 10x slower than the miniKanren version above :)

    ReplyDelete
  3. This comment has been removed by the author.

    ReplyDelete
  4. On which machine :) I have a slow laptop.
    1 iteration of Z3 is:
    phil@phil:~/projects/8queens$ time ~/bin/z3/bin/z3 8queen.smt2
    real 0m0.076s
    user 0m0.068s
    sys 0m0.004s
    The bash script, to iterate through solutions is proly nearly half of the total 12sec

    ReplyDelete

Note: only a member of this blog may post a comment.