экземпляры SAT в реальном мире

Я разрабатываю и внедряю решатель SAT. Было бы особенно хорошо, если бы все предложения имели вид

a AND b = c
a OR b = c
a XOR b = c
a = NOT b

В литературе они используют форму CNF, которая, я думаю, будет менее эффективным представлением исходной проблемы реального мира на практике. Они делают это, потому что существующие решатели SAT могут лучше обрабатывать CNF. Однако это не сработало бы для моего SAT-решателя, что поставило бы меня в невыгодное положение. Кто-нибудь знает о каких-либо реальных случаях в приведенной выше форме?


constraint-programming operations-research satisfiability
person Albert Hendriks    schedule 20.07.2014    source источник
comment
Фахим Бахус проделал довольно большую работу по использованию представлений схем в решении SAT и QBF. Кажется, это очень связано с тем, что вы пытаетесь сделать.   -  person Pramod    schedule 24.12.2014

Ответы (2)


arrow_upward
3
arrow_downward

Вы поднимаете верный вопрос. У Питера Стаки был доклад «Нет проблем с УТС» на SAT Conference 2013. Слайды вы найдете здесь.

Для практических приложений было бы неплохо иметь высокоуровневый язык описания проблем, такой как MiniZinc Стаки. Кодирование проблемы в CNF слишком часто утомительно и подвержено ошибкам.

Чтобы ответить на ваш вопрос:
Да, большинство реальных задач описываются как логические или математические выражения, а не как CNF. Шаг кодирования необходим, чтобы разрешить их решение некоторым решателем.

На научном рынке существует множество «школ» решателей, которые делают кодирование задач менее проблематичным. Примерами являются программирование набора ответов (ASP), такое как Gringo/Clasp, и решатели программирования с ограничениями (CSP). ), например MiniZinc.

Другой вариант — использовать «Circuit-SAT», а не CNF-SAT. «Схема» описывается в терминах логических вентилей и связей между ними. Это своего рода вложенная система логических выражений. Мой любимый инструмент для преобразования цепей в CNF — bc2cnf.

Есть несколько хороших моментов, которые следует упомянуть о CNF:

  1. CNF (в формате DIMACS) может обрабатываться многими инструментами.
  2. CNF достаточно компактен
  3. CNF можно очень легко разобрать
person Axel Kemper    schedule 21.07.2014

arrow_upward
2
arrow_downward

Теория и применение решателей SAT очень тесно связаны с представлением CNF. Если ваш решатель использует логические формулы вместо CNF, вы можете думать о своем решателе не как о «решателе SAT», а как о «решателе SMT без поддержки теорий, кроме логики первого порядка без кванторов».

Многие решатели SMT поддерживают SMT-LIBv2 в качестве языка ввода. В SMT-LIB набор функций решателя настраивается путем установки «логики» с помощью оператора set-logic. Логика QF_UF поддерживает только базовые логические формулы без кванторов и должна быть эквивалентна тому, что вы хотите. Например. ваши примеры предложений в синтаксисе SMT-LIB:

(set-logic QF_UF)
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(assert (= (and a b) c))
(assert (= (or a b) c))
(assert (= (xor a b) c))
(assert (= a (not b)))
(check-sat)
(exit)

Который напечатает unsat при передаче решателю SMT.

Бенчмарк SMT-LIB QF_UF содержит большой набор проблем в этом формате (6647 "крафтовых" и 3 "промышленных"):

Соревнования SMT разделены на логические подразделения. Таким образом, можно выставить на соревнование решатель, который поддерживает только QF_UF. (На самом деле решатель OpenSMT2 поддерживает только QF_UF и участвовал в SMT-COMP 2014.)

person CliffordVienna    schedule 22.12.2014