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

Question

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

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

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

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

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

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

1

declarative answer-set-programming satisfiability

Источник

user403875 23 фев '15 в 01:54

1 ответ

Решение

Другие вопросы по тегам declarative answer-set-programming satisfiability

user1911064 24 фев '15 в 20:03 2015-02-24 20:03 · Accepted Answer · 2015-02-24 20:03

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

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

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

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