CODEWITHSUNDEEP
z3smtclpfdlabeling
Boris Shingarov
Boris Shingarov

Reputation: 11

Are there approaches to guide Z3 similar to CLP(FD)'s ff-labeling?

This is more of an admission of my illiteracy in the state of research in solving than related to actual programming; looking at the following canonical example of N-Queens in Z3:

print('Solving N Queens for a {} by {} chess board'.format(n, n))
# Instantiate solver
s = Solver()
# Creating row and column co-ordinates for each queen
columns = [Int('col_%d' % i) for i in range(n)]
rows = [Int('row_%d' % i) for i in range(n)]
# Should only be one queen per row or column
s.add(Distinct(rows))
s.add(Distinct(columns))

# Each cell should have a value within the boards co-ordinates
for i in range(n):
    s.add(columns[i] >= 0,columns[i] < n, rows[i] >= 0, rows[i] < n)
# No queens should be to take each other
for i in range(n - 1):
    for j in range(i + 1, n):
        s.add(abs(columns[i] - columns[j]) != abs(rows[i] - rows[j]))
s.check()

As a long-time Prologer I am used to the following style of optimizing the search: (this works in SWI-Prolog):

:- use_module(clpz).
n_queens(N, Qs) :-
        length(Qs, N),
        Qs ins 1..N,
        safe_queens(Qs).
safe_queens([]).
safe_queens([Q|Qs]) :- safe_queens(Qs, Q, 1), safe_queens(Qs).
safe_queens([], _, _).
safe_queens([Q|Qs], Q0, D0) :-
        Q0 #\= Q,
        abs(Q0 - Q) #\= D0,
        D1 #= D0 + 1,
        safe_queens(Qs, Q0, D1).
/* Example:
   ?- n_queens(100, Qs), labeling([ff], Qs). */

This handles 100 queens easily. Obviously, this optimization can not be translated to SMT literally. So, my question is: what would be the idiomatic way to guide the solver in cases like this?

Upvotes: 1

Views: 190

Answers (1)

alias
alias

Reputation: 30428

A general-purpose SMT solver like z3 can never match the scalability of Prolog's SLD resolution engine. On the other hand, the strategies used by an SMT solver are much more general: They shine in theory combinations and in the ability of reasoning about arithmetic, data-structures, floating point, etc., all in a mix-and-match fashion. So, a basic Prolog implementation cannot handle the range of problems an SMT solver can deal with, at least not out-of-the box.

I think it's best to consider these systems as what they are: Prolog shines in problems where SLD resolution can find the solution, and it can scale. An SMT solver can essentially simulate SLD search, but it won't scale like a custom SLD engine can like you would find in a dedicated prolog implementation. It's much better to use each playing to their strengths, instead of trying to make one simulate the other.

Upvotes: 1

Related Questions