将 Boolean FlatZinc 转换为 CNF DIMACS

为了解决一个布尔方程组 http://arxiv.org/abs/1108.2830，我正在尝试Constraint-Programming Solver MiniZinc http://www.minizinc.org/使用以下输入：

%  Solve system of Brent's equations modulo 2

%  Matrix dimensions
int: aRows = 3;
int: aCols = 3;
int: bCols = 3;
int: noOfProducts = 23;

%  Dependent parameters
int: bRows = aCols;
int: cRows = aRows;
int: cCols = bCols;
set of int: products = 1..noOfProducts;

%  Corefficients are stored in arrays
array[1..aRows, 1..aCols, products] of var bool: A;
array[1..bRows, 1..bCols, products] of var bool: B;
array[1..cRows, 1..cCols, products] of var bool: C;

constraint
    forall(rowA in 1..aRows, colA in 1..aCols) (
        forall(rowB in 1..bRows, colB in 1..bCols) (
            forall (rowC in 1..cRows, colC in 1..cCols) (
                xorall (k in products) (
                    A[rowA, colA, k] /\ B[rowB, colB, k] /\ C[rowC, colC, k]
                ) == ((rowA == rowC) /\ (colB == colC) /\ (colA == rowB))
            )
        )
    );

solve satisfy;

%  Output solution as table of variable value assignments
output 
["\nSolution for <" ++ show(aRows) ++ ", " ++ show(aCols) ++ 
                 ", " ++ show(bCols) ++ "> " ++ show(noOfProducts) ++ " products:"] ++
["\nF" ++ show(100*rowA+10*colA+k) ++ " = " ++ 
show(bool2int(A[rowA, colA, k])) |
rowA in 1..aRows, colA in 1..aCols, k in products] ++

["\nG" ++ show(100*rowB+10*colB+k) ++ " = " ++ 
show(bool2int(B[rowB, colB, k])) |
rowB in 1..bRows, colB in 1..bCols, k in products] ++

["\nD" ++ show(100*rowC+10*colC+k) ++ " = " ++ 
show(bool2int(C[rowC, colC, k])) |
rowC in 1..cRows, colC in 1..cCols, k in products];

MiniZinc http://www.minizinc.org/确实找到了小参数的解决方案(rows=cols=2, products=7)，但并没有随着稍微增加而结束。 我想喂养生成的FlatZinc http://www.minizinc.org/模型化为SAT求解器 http://en.wikipedia.org/wiki/SAT_solver#Algorithms_for_solving_SAT like 小型隐秘卫星 http://www.msoos.org/cryptominisat2/, 林格林 http://fmv.jku.at/lingeling/ or Clasp http://www.cs.uni-potsdam.de/clasp/。我希望这些工具的性能可能优于现有的 MiniZinc 后端。

我的问题：
有没有什么工具可以转换纯布尔值FlatZinc http://www.minizinc.org/模型化为CNF (DIMACS) http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html?
我可以做什么来更换xorall()谓词，因为某些 MiniZinc 后端似乎不支持它？

我不知道有什么工具可以将 FlatZinc 文件转换为 CNF (DIMACS) 文件。 （MiniZinc 发行版有一个将 flatzinc 转换为 XCSP 格式的程序。也许有一个将 XCSP 转换为 CNF 的工具？）

然而，有一些基于 SAT/启发的求解器可能更好，例如minicsp、fzn2smt。问题是，正如您所提到的，它们不支持全新的 xorall() 函数。

另外，使用标记搜索可能是个好主意，即类似这样的东西（注意 bool_search）

  solve :: bool_search(
       [A[i,j,k] | i in 1..aRows, j in 1..aCols, k in products],
       first_fail,
       indomain_min,
       complete)
     satisfy;

另外，我建议您测试转换为基于 0..1 的模型，这样可以测试这些求解器以及其他求解器。

这是我转换后的模型，我刚刚将 var bool 更改为 var 0..1 并将 xorall() 替换为 sum() 和 bool2int() [我希望我转换正确。] 更新：我已更改为版本阿克塞尔提议道。

 %  Solve system of Brent's equations modulo 2

 %  Matrix dimensions
 int: aRows = 3;
 int: aCols = 3;
 int: bCols = 3;
 int: noOfProducts = 23;

 %  Dependent parameters
 int: bRows = aCols;
 int: cRows = aRows;
 int: cCols = bCols;
 set of int: products = 1..noOfProducts;

 %  Corefficients are stored in arrays
 array[1..aRows, 1..aCols, products] of var 0..1: A; % hakank: change to 0..1
 array[1..bRows, 1..bCols, products] of var 0..1: B;
 array[1..cRows, 1..cCols, products] of var 0..1: C;

constraint
     forall(rowA in 1..aRows, colA in 1..aCols) (
         forall(rowB in 1..bRows, colB in 1..bCols) (
             forall (rowC in 1..cRows, colC in 1..cCols) (
                 % hakank: changed
                 sum (k in products) (
                     bool2int(A[rowA, colA, k]=1/\ B[rowB, colB, k]=1 /\ C[rowC, colC, k]=1)
                ) == 
                     %% bool2int(rowA == rowC)+ bool2int(colB == colC) + bool2int(colA == rowB)
                     bool2int((rowA == rowC)/\(colB == colC)/\(colA == rowB))
             )
         )
     );


     solve :: int_search(
         [A[i,j,k] | i in 1..aRows, j in 1..aCols, k in products] ++ 
         [B[i,j,k] | i in 1..aRows, j in 1..aCols, k in products] ++ 
         [C[i,j,k] | i in 1..aRows, j in 1..aCols, k in products] 
         ,
         first_fail,
         indomain_min,
         complete)
     satisfy;

    %  Output solution as table of variable value assignments
    output 
    ["\nSolution for <" ++ show(aRows) ++ ", " ++ show(aCols) ++ 
             ", " ++ show(bCols) ++ "> " ++ show(noOfProducts) ++ " products:"] ++
    ["\nF" ++ show(100*rowA+10*colA+k) ++ " = " ++ 
        show(A[rowA, colA, k]) |
        rowA in 1..aRows, colA in 1..aCols, k in products] ++

    ["\nG" ++ show(100*rowB+10*colB+k) ++ " = " ++ 
       show(B[rowB, colB, k]) |
       rowB in 1..bRows, colB in 1..bCols, k in products] ++

    ["\nD" ++ show(100*rowC+10*colC+k) ++ " = " ++ 
       show(C[rowC, colC, k]) |
       rowC in 1..cRows, colC in 1..cCols, k in products];

这是模型：http://www.hakank.org/minizinc/akemper1_2.mzn http://www.hakank.org/minizinc/akemper1_2.mzn .

[更新：这些时间针对较早的错误模型。] 模型中的问题实例由 minicsp 在 3 秒内解决（第一个解决方案），由 Opturion CPX 求解器在 5 秒内解决，由 fzn2smt 在 6 秒内解决。该模型也许可以通过标签等进一步调整。

提到的求解器的链接：

• 选项 CPX：http://www.opturion.com/cpx.html http://www.opturion.com/cpx.html

• 小型CSP：http://www.inra.fr/mia/T/katsirelos/minicsp.html http://www.inra.fr/mia/T/katsirelos/minicsp.html

• fzn2smt：http://ima.udg.edu/Recerca/ESLIP/fzn2smt/index.html http://ima.udg.edu/Recerca/ESLIP/fzn2smt/index.html

另请参阅我的 MiniZinc 页面，了解更多 FlatZinc 求解器列表：http://www.hakank.org/minizinc/ http://www.hakank.org/minizinc/ .