Konvertieren Sie Boolean FlatZinc in CNF DIMACS
A. LösenSatz von Booleschen GleichungenIch experimentiere mit demConstraint-Programming Solver
MiniZinc unter Verwendung der folgenden Eingabe:
% 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 findet eine Lösung für kleine Parameter(rows=cols=2, products=7)
, endet aber nicht mit den leicht erhöhten. Ich möchte die erzeugten fütternFlatZinc Modell in eineSAT-Löser mögenCryptominisat, Lingeling oderSchließe. Ich hoffe, dass diese Tools die vorhandenen MiniZinc-Backends übertreffen.
Meine Frage:
Gibt es ein Werkzeug, um einen rein booleschen Wert zu konvertieren?FlatZinc Modell inCNF (DIMACS)?
Was könnte ich tun, um das zu ersetzen?xorall()
Prädikat, da einige der MiniZinc-Backends es nicht zu unterstützen scheinen?