将布尔型FlatZinc转换为CNF DIMACS [英] Convert Boolean FlatZinc to CNF DIMACS

问题描述

要解决一组布尔方程，我正在尝试Constraint-Programming Solver MiniZinc 使用以下输入:

To solve a set of Boolean equations, I am experimenting with the Constraint-Programming Solver MiniZinc using the following input:

%  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 确实找到了小参数(rows=cols=2, products=7)的解决方案，但并没有以略有增加. 我想将生成的 FlatZinc 模型提供给 Cryptominisat ， Lingeling 或

MiniZinc does find a solution for small parameters (rows=cols=2, products=7) , but does not come to an end with the slightly increased ones. I'd like to feed the generated FlatZinc model into a SAT solver like Cryptominisat, Lingeling or Clasp. My hope is these tools might outperform the existing MiniZinc back-ends.

我的问题:
是否有任何工具可以将纯布尔 FlatZinc 模型转换为

My Question:
Is there any tool available to convert a purely Boolean FlatZinc model into CNF (DIMACS)?
What could I do to replace the xorall() predicate as some of the MiniZinc back-ends don't seem to support it?

推荐答案

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

I don't know of any tools that converts a FlatZinc file to and CNF (DIMACS) file. (The MiniZinc distribution has a program to convert flatzinc to XCSP format. Perhaps there's a tool for XCSP to CNF?)

但是，有些基于SAT/启发式求解器可能会更好，例如minicsp，fzn2smt.问题是，正如您提到的那样，它们不支持全新的xorall()函数.

However, there are some SAT based/inspired solvers that might be better, e.g. minicsp, fzn2smt. There problem is that they - as you mention - don't support the quite new xorall() function.

此外，使用标记搜索(例如，这样的东西(请注意bool_search))可能是个好主意

Also, it might be a good idea to use a labeled search, i.e. something like this (note the 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的模型，在这些模型中，可以与其他求解器一样进行测试.

Also, I suggest you to test to convert to a 0..1 based model instead, where these solvers can be tested as well as others.

这是我转换后的模型，其中我刚刚将var bool更改为var 0..1，并用sum()和bool2int()替换了xorall()[我希望我能正确转换.]更新:我已经更改了到Axel建议的版本.

Here's my converted model where I've just changed var bool to var 0..1 and replaced the xorall() with sum() and bool2int() [I hope I converted that correct.] Update: I've changed to the version Axel suggested.

 %  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 .

[更新:这些时间是针对较早的，错误的模型的.]模型中的问题实例由minicsp在3s(包括展平)中，由Opturion CPX求解器在5s，由fzn2smt在3s中解决(第一个解决方案). 6s.并且可以通过标签等对模型进行进一步调整.

[Update: These times are for the earlier, wrong, model.] The problem instance in the model is solved (first solution) by minicsp in 3s (including flattening), by the Opturion CPX solver in 5s, by fzn2smt in 6s. And the model can perhaps be tweaked further with labelings etc.

与提到的求解器的链接:

Links to the solvers mentioned:

• Opturion CPX: http://www.opturion.com/cpx.html

MiniCSP: http://www.inra.fr/mia/T/katsirelos/minicsp.html

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

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

Also see my MiniZinc page for a longer list of FlatZinc solvers: http://www.hakank.org/minizinc/ .

这篇关于将布尔型FlatZinc转换为CNF DIMACS的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！