Чтобы решитьсистема булевых уравненийЯ экспериментирую сConstraint-Programming Solver MiniZinc используя следующий вход:

%  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 решатель лайкCryptominisat, Lingeling или жепожатие, Я надеюсь, что эти инструменты могут превзойти существующие бэкэнды MiniZinc.

Мой вопрос:
Есть ли какой-либо инструмент, доступный для преобразования чисто логическогоFlatZinc модель вCNF (DIMACS)?
Что я мог сделать, чтобы заменитьxorall() предикат, поскольку некоторые бэкэнды MiniZinc, кажется, не поддерживают это?