Это команда depqbf, которую можно запустить в бесплатном хостинг-провайдере OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
depqbf - решатель для количественных булевых формул
СИНТАКСИС
депкбф [кредита ...] [NUM] [ФАЙЛОВ]
ОПИСАНИЕ
депкбф это основанный на поиске решатель для квантифицированных логических формул (QBF) в предварительном отчете
конъюнктивная нормальная форма. Он основан на алгоритме DPLL для QBF с конфликтно-управляемым
предложения и кубическое обучение на основе решений. Анализируя структуру формулы, DepQBF
пытается определить независимые переменные. Помимо других преимуществ, это часто
увеличивает свободу принятия решений. См. Также описание системы JSAT для DepQBF 0.1.
от QBFEVAL'10 за ссылки и краткое изложение идеи.
депкбф читает формулы QBF в формате QDIMACS. Если ФАЙЛОВ не задан, он считывает свой ввод из
stdin. Он соответствует стандартам ввода / вывода, как того требует QBFEVAL'10.
ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ
депкбф принимает следующие варианты:
-час, --Помогите
Распечатайте информацию об использовании.
--версия
Версия для печати.
--красивый принт
Только разобрать и распечатать формулу.
-v Постепенно увеличивайте степень детализации.
NUM Необязательно: тайм-аут через ЧИСЛО секунд.
ФАЙЛОВ Необязательно: прочитать ввод из ФАЙЛА.
ВЫХОД статус
Статус выхода равен 10, если формула QBF, заданная в качестве входных данных, удовлетворительна, и 20, если она
неудовлетворительно; любой другой код выхода означает, что формула не решена.
Используйте depqbf онлайн с помощью сервисов onworks.net
