Компиляторы, которые переводят алгоритмы проверки в задачи SAT - PullRequest
Новая
       54

Компиляторы, которые переводят алгоритмы проверки в задачи SAT

5 голосов
/ 12 декабря 2011

Доказательство того, что SAT является NP-полным, является конструктивным доказательством, поэтому должна быть возможность реализовать его как программу. Кто-нибудь делал это?

Я ищу программу (компилятор), которая принимает в качестве входных данных программу (которая возвращает true или false) и выводит формулу SAT.

Так, например, компилятор может взять следующую программу (показывать в синтаксисе с питоном, но мне подходит любой язык) в качестве входных данных и вывести формулу SAT. Подача формулы SAT в решатель SAT дала бы решение параметру «сертификат». В этом случае решением будет [False, True, True, True, False], что означает, что {-3, -2, 5} является решением. 

def verify(certificate):
  problem = [-7, -3, -2, 5, 8]
  sum = 0
  for (x, b) in zip(problem, certificate):
    if b:
      sum += x
  return sum == 0

Очевидно, что выходная формула SAT будет иметь другие вспомогательные переменные, поэтому компилятор должен будет указать, какие переменные соответствуют сертификату.

Такие компиляторы уже существуют? Кто-нибудь из них с открытым исходным кодом?

1 Ответ

3 голосов
/ 26 января 2012

Вам следует изучить SMT-решатели, так как они наиболее близки к тому, что вы хотите.Вы не пишете на полном языке Тьюринга с SMT (без циклов), но вы можете работать с целочисленными и вещественными переменными, логической логикой, функциями, базовой арифметикой и массивами.

...