Конвертировать Булевы плоские цинковые в CNF DIMACS

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

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

Источник

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 и заменил 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.

[Обновление: это время для более ранней, неправильной модели.] Проблема в модели решается (первое решение) с помощью minicsp за 3 с (включая выравнивание), с помощью решателя Opturion CPX за 5 с, с помощью fzn2smt за 6 с. И модель может быть улучшена с помощью надписей и т. Д.

Ссылки на упомянутые решатели:

Также смотрите мою страницу MiniZinc для более длинного списка решателей FlatZinc: http://www.hakank.org/minizinc/.

Источник
Другие вопросы по тегам