轉換布爾FlatZinc到CNF DIMACS

Question

解決set of Boolean equations，我與Constraint-Programming SolverMiniZinc嘗試使用以下輸入：

% 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模型到SAT solver像Cryptominisat,Lingeling或Clasp。我希望這些工具可能會勝過現有的MiniZinc後端。

我的問題：
是否有任何可用的工具，以一個純粹的布爾FlatZinc模型轉換爲CNF (DIMACS)？
我能做些什麼來取代xorall()謂詞，因爲一些MiniZinc後端似乎不支持它？

Answer 1

我不知道任何將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，並用sum（）和bool2int（）替換了xorall（）[我希望我將其轉換爲正確的。] Update：I've改爲Axel建議的版本。

% 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。 （更新：這些時間是針對較早的，錯誤的，模型的）模型中的問題實例由3s中的minicsp（包括展平），5s中的Opturion CPX解算器，fzn2smt在6s。和模型也許可以進一步與標號L等扭捏

鏈接所提到的求解：

• 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/。