Как мне преобразовать ряд математических ограничений в задачи SAT или SMT и получить ответ?

Question

У меня есть произвольный набор ограничений. Например:

A, B, C and D are 8-bit integers.

A + B + C + D = 50
(A + B) = 25
(C + D) = 30
A < 10

Я могу преобразовать это в проблему SAT, которую можно решить с помощью picosat (я не могу заставить minisat скомпилировать на моем Mac), или в проблему SMT, которая может быть решена с помощью CVC4. Для этого мне нужно:

1. Преобразуйте эти уравнения в булеву схему.
2. Примените преобразование Цейтина к схеме и преобразуйте его в формат DIMACS.

Мои вопросы:

1. Какие инструменты я использую для преобразования в схему?
2. Какие форматы файлов для схем и какие обычно используются?
3. Какие инструменты я использую для преобразования схемы в формат DIMACS?

Answer 1

Концептуально

Постройте схему, затем примените преобразование Цейтина.

Вы должны будете выразить операторы сложения и сравнения как логическую логику. Существуют стандартные способы построения схемы для добавления двух дополнений и сравнения двух дополнений.

Затем используйте преобразование Цейтина, чтобы преобразовать его в экземпляр SAT.

На практике

Используйте интерфейс SAT, который сделает это преобразование за вас. Z3 позаботится об этом за вас. Так будет STP. (Преобразование иногда называют "взрывом".)

Answer 2

В MiniZinc вы могли бы просто написать модель программирования ограничений:

set of int: I8 = 0..255;

var I8: A;
var I8: B;
var I8: C;
var I8: D;

constraint A + B + C + D == 50;

constraint (A + B) = 25;

constraint (C + D) = 30;

constraint A < 10;

solve satisfy;

Примеры ограничений не могут быть выполнены из-за 25 + 30 > 50,

---

Интерфейс Python Z3 позволил бы следующее:

from z3 import *
A, B, C, D = Ints('A B C D')
s = Solver()
s.add(A >= 0, A < 256)
s.add(B >= 0, B < 256)
s.add(C >= 0, C < 256)
s.add(A+B+C+D == 50)
s.add((A+B) == 25)
s.add((C+D) == 30)
s.add(A < 10)
print(s.check())
print(s.model())

Answer 3

Итак, у меня есть ответ. Есть программа Sugar: основанный на SAT Constraint Solver, который принимает ряд ограничений в виде S-выражений, преобразует все это в файл DIMACS, запускает SAT Solver, а затем преобразует результаты SAT Solver обратно в результаты. ваших ограничений.

Сахар был разработан Наоюки Тамурой для решения математических задач, таких как головоломки Судоку. Я обнаружил, что это чрезвычайно упрощает кодирование сложных ограничений и их запуск.

Например, чтобы найти квадратный корень из 625, можно сделать это:

(int X 0 625)
(= (* X X) 625)

В первой строке написано, что X находится в диапазоне от 0 до 625. Во второй строке написано, что X*X равно 625.

Это может быть не так просто и элегантно, как Z3, но это сработало очень хорошо.