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

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

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

Так, например, компилятор может взять следующую программу (показанную в синтаксисе Python, но мне подходит любой язык) в качестве входных данных и вывести формулу SAT. Подача формулы SAT в решатель SAT даст решение для параметра «сертификат». В этом случае решением будет [Ложь, Истина, Истина, Истина, Ложь], что указывает на то, что {-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 будет иметь другие вспомогательные переменные, поэтому компилятор должен будет указать, какие переменные соответствуют сертификату.

Существуют ли такие компиляторы? Есть ли у них открытый исходный код?