Инструменты для заземления SAT?

В ASP (программирование набора ответов) программы пишутся на декларативном языке более высокого уровня, а затем обосновываются детерминистическим способом для создания экземпляра ASP с использованием такого средства заземления, как lparse или гринго.

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

vertex(a; b; c).
isRed(V) \/ isBlue (V) \/ isGreen(V) :- vertex(V).

и создать из него файл DIMACS?

В целом, как генерируются экземпляры соревнований SAT?


declarative satisfiability answer-set-programming
person dspyz    schedule 23.02.2015    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Экземпляры конкурса SAT обычно создаются с использованием специально разработанных программ-генераторов, а не обычных основатели ASP. Требования к тесту описаны здесь.

Другие варианты создания файла CNF/DIMACS включают:

  • Переведите логическое выражение через Limboole, bool2cnf или bc2cnf
  • Скомпилируйте объявление ограничения MiniZinc в CNF/DIMACS.
  • Преобразование ANF в CNF с помощью anf2cnf

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

person Axel Kemper    schedule 24.02.2015