是否有类似于CLPFD的ff-labeling的方法来指导Z3？

问题描述

这更多是我对解决问题的研究状态的认可，而不是与实际编程有关；看下面的Z3中的N-Queens典型例子：

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()

作为长期的Prologer，我习惯于以下优化搜索的风格：（这在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,D1).
/* Example:
   ?- n_queens(100,Qs),labeling([ff],Qs). */

这可以轻松处理100个皇后。显然，这种优化不能从字面上转换为SMT。所以，我的问题是：在这种情况下，惯用的方法来指导求解器是什么？

解决方法

像z3这样的通用SMT求解器永远无法满足Prolog SLD解析引擎的可扩展性。另一方面，SMT求解器使用的策略则更为通用：它们以混合匹配的方式在理论组合以及算术，数据结构，浮点等的推理能力中发挥了作用。。因此，基本的Prolog实现无法处理SMT求解器可以处理的一系列问题，至少不是开箱即用的。

我认为最好将这些系统看作是它们的本质：Prolog提出了SLD解析可以找到解决方案并可以扩展的问题。 SMT求解器实际上可以模拟SLD搜索，但是它无法像自定义SLD引擎那样扩展，就像您在专用的序言实现中所能找到的那样。更好地利用每种方式发挥各自的优势，而不是试图使一种模拟另一种。

clpfd labeling smt z3