gophersat
1.0.0
Это Gophersat, SAT и псевдобулевый решатель, написанный исключительно на Go. Gophersat был разработан CRIL (Центром исследований и информатики линз) при Университете Артуа и CNRS. Он выпускается под лицензией MIT. Gophersat довольно эффективен, т.е. в типичных тестах SAT он работает примерно в 2–5 раз медленнее, чем решатели верхнего уровня (а именно, глюкоза или минисат), на которых он основан. Он также может решать задачи MAXSAT, а также псевдологические задачи решения и оптимизации.
Последней стабильной версией Gophersat является версия 1.4. Он включает в себя дополнительную стратегию решения секущих плоскостей.
Некоторые проблемы, такие как знаменитая проблема с ячейками, требуют очень много времени для решения с использованием чистых логических рассуждений.
Задачу о ячейках можно сформулировать так: можно ли поместить n голубей в m ячеек, где m = n-1, не помещая при этом нескольких голубей в одну ямку и не помещая всех голубей в одну ямку? Ответ очевиден: если у вас 4 голубя в 3 норах, вы не сможете посадить их всех в другую нору. Но как это доказать ? Решатель SAT или PB докажет это, попробовав все возможные комбинации, и количество возможных комбинаций растет в геометрической прогрессии. Таким образом, попытка решить задачу с n=20 на практике неосуществима, несмотря на то, что задача имеет очевидный ответ.
Некоторые решатели PB реализуют альтернативную стратегию: стратегию секущих плоскостей. В этом документе она не описывается подробно, но эта стратегия может быть чрезвычайно эффективной в некоторых проблемах, таких как проблема с классическими ячейками, которую нельзя эффективно решить с помощью чисто логических рассуждений, но в большинстве задач она будет медленнее.
Теперь можно использовать секущие плоскости с Gophersat. Просто используйте параметр командной строки -cp . Итак, вместо вызова:
gophersat problem.opb
Просто позвоните:
gophersat -cp problem.opb
Последней стабильной версией Gophersat является версия 1.3. Это небольшое обновление, добавляющее возможность доступа к базовому решателю при решении проблем MAXSAT.
Gophersat версии 1.2 включает в себя способ понимания экземпляров UNSAT как путем предоставления сертификатов RUP, когда проблема связана с UNSAT, так и путем предоставления возможности извлекать неудовлетворительные подмножества формулы. Также было исправлено множество ошибок и улучшена поддержка поэтапного решения SAT.
Чтобы узнать больше об этих функциях, вы можете просмотреть руководство по сертификатам UNSAT и MUS.
Чтобы сгенерировать сертификат с помощью исполняемого файла gophersat, просто вызовите:
gophersat -certified problem.cnf
Сертификат затем будет выведен на стандартный вывод с использованием нотации RUP. Сертификат генерируется «на лету», поэтому имейте в виду, что частичный бесполезный сертификат будет создан, даже если проблема действительно разрешима. Это обычная практика в сообществе, и хотя генерируемые предложения являются бесполезным шумом, на практике это не является проблемой.
Чтобы извлечь MUS из экземпляра UNSAT, просто вызовите:
gophersat -mus problem.cnf
MUS будет напечатан на стандартном выходе. Если проблема не в UNSAT, появится сообщение об ошибке.
На данный момент эти возможности доступны только для решения чистых задач SAT (т.е. не псевдобулевых задач).
Начиная с версии 1.1, Gophersat включает в себя новый, более эффективный основной решатель для чистых задач SAT и пакет для решения задач MAXSAT. Он также включает новый API для оптимизации и подсчета моделей, благодаря которому новые модели записываются в каналы сразу после их обнаружения.
Начиная с версии 1.0 API Gophersat считается стабильным, а это означает, что API гарантированно останется обратно совместимым до смены основной версии. Другими словами, если ваша программа работает с gophersat версии 1.0, она все равно будет работать с версией 1.1 или выше, но не обязательно с версией выше 2.0.
Обратите внимание, что под «все еще работать» мы подразумеваем только «будет компилироваться и выдавать тот же результат», а не «будет иметь одинаковую производительность с точки зрения памяти или времени». Это важное различие: во время небольших обновлений версии могут быть введены новые эвристики или типы данных, а это означает, что некоторые проблемы могут быть решены быстрее или медленнее, чем раньше.
go get github.com/crillab/gophersat && go install github.com/crillab/gophersat
Gophersat можно использовать как автономный решатель (чтение файлов DIMACS CNF) или как библиотеку в любой программе Go.
Чтобы решить файл DIMACS, вы можете вызвать gophersat со следующим синтаксисом:
gophersat --verbose file.cnf
где --verbose — необязательный параметр, который позволяет решателю отображать информацию во время процесса решения.
Gophersat также способен читать и решать более общие логические формулы, а не только задачи, представленные в недружественном для пользователя формате DIMACS. Он также изначально имеет дело с ограничениями мощности, то есть предложениями, которые должны иметь как минимум n истинных литералов, при этом n > 1.
Gophersat можно использовать как автономный решатель (чтение файлов OPB) или как библиотеку в любой программе Go.
Чтобы решить псевдологическую задачу (будь то задачу решения или оптимизации), вы можете вызвать gophersat со следующим синтаксисом:
gophersat --verbose file.opb
где --verbose — необязательный параметр, который позволяет решателю отображать информацию во время процесса решения.
На данный момент он может решать только так называемые проблемы DEC-SMALLINT-LIN и OPT-SMALLINT-LIN, т.е. проблемы решения (есть решение или нет) для линейных ограничений (суммы взвешенных литералов) на небольшие целые числа. (n <2^30) или задачи оптимизации (каково наилучшее решение, минимизирующее заданную функцию стоимости) для линейных ограничений на небольшие целые числа.
Благодаря пакету maxsat Gophersat теперь может решать проблемы MAXSAT.
Чтобы решить взвешенную задачу MAXSAT, вы можете вызвать gophersat со следующим синтаксисом:
gophersat --verbose file.wcnf
где --verbose — необязательный параметр, который позволяет решателю отображать информацию во время процесса решения. Предполагается, что файл будет представлен в формате (формат WCNF)[http://www.maxsat.udl.cat/08/index.php?disp=requirements].
SAT, что означает «булева проблема выполнимости» , является канонической NP-полной проблемой, то есть проблемой, для которой не существует известного решения, которая в худшем случае не требует экспоненциального времени. В нескольких словах, решатель SAT пытается найти для данной пропозициональной формулы назначение для всех ее переменных, которое делает ее истинной, если такое присваивание существует.
Хотя реализовать решатель SAT с использованием простого алгоритма тривиально, на практике такая реализация будет очень неэффективной. Gophersat реализует самые современные функции и, таким образом, весьма эффективен, что позволяет использовать его на практике в программах Go, которым требуется эффективный механизм вывода.
Хотя это не всегда лучшее решение по практическим соображениям, любая NP-полная задача может быть преобразована в задачу SAT и решена с помощью Gophersat. К таким задачам относятся задача коммивояжера, программирование в ограничениях, задача о рюкзаке, планирование, проверка модели, проверка правильности программного обеспечения и т. д.
Более подробную информацию о проблеме SAT можно найти в статье Википедии о SAT.
Вы также можете найти информацию о том, как представлять свои собственные логические формулы, чтобы их можно было использовать gophersat, в руководстве «SAT для новичков».
MAXSAT — это оптимизационный эквивалент проблемы принятия решений SAT. В то время как чистый решатель SAT либо вернет модель, удовлетворяющую всем условиям, либо UNSAT, если такой модели не существует, решатель MAXSAT вернет модель, которая удовлетворяет как можно большему количеству предложений.
Существуют расширения MAXSAT.
Частичный MAXSAT означает, что, хотя мы хотим удовлетворить как можно больше условий, некоторые условия (называемые жесткими условиями ) должны быть выполнены, несмотря ни на что. Таким образом, частичную задачу MAXSAT можно объявить неразрешимой.
Например, создание расписания для школы — это частичная задача MAXSAT: существуют как мягкие (например, мы хотим, чтобы уроков было как можно меньше, которые начинаются после 16:00), так и сложные (два учителя не могут находиться в двух разных местах в в то же время) ограничения.
Взвешенный MAXSAT означает, что статьи связаны с затратами: хотя они не являются обязательными, некоторые статьи считаются более важными, чем другие. Например, если стоимость пункта C1 равна 3, а стоимость пунктов C2 и C3 равна 1, решение, удовлетворяющее C1, но не удовлетворяющее ни C2, ни C3, будет считаться лучшим, чем решение, удовлетворяющее как C2, так и C3, но не удовлетворяющее C1, все остальные все в равных условиях.
Частично взвешенный MAXSAT означает, что в задаче есть как мягкие, так и жесткие положения, причем мягкие положения имеют вес. В этом отношении «чистый» MAXSAT является частным случаем более общего MAXSAT с частичным взвешиванием: «чистая» проблема MAXSAT — это задача MAXSAT с частичным взвешиванием, где все предложения являются мягкими предложениями, связанными с весом 1.
Псевдобуловые задачи в некотором смысле являются обобщением задач SAT: любое предложение высказывания может быть записано как одно псевдологическое ограничение, но для представления псевдологического ограничения может потребоваться экспоненциальное количество предложений высказываний.
(Линейное) псевдологическое выражение — это выражение типа:
w1 l1 + w2 x2 + ... + wn xn ≥ y
где y и все wi — целочисленные константы, а все li — логические литералы.
Например, чтобы следующее выражение было истинным
2 ¬x1 + x2 + x3 ≥ 3
логическая переменная x1 должна быть ложной, и хотя бы одна из x2 и x3 должна быть истинной. Это эквивалентно пропозициональной формуле
¬x1 ∧ (x2 ∨ x3)
Псевдобулевые выражения являются обобщением предложений-предложений: любое предложение
x1 ∨ x2 ∨ ... ∨ xn
можно переписать как
x1 + x2 + ... + xn ≥ 1
Описание псевдобулевой задачи может быть экспоненциально меньшим, чем ее пропозициональный аналог, но решение псевдобулевой задачи по-прежнему остается NP-полным.
Gophersat решает как проблемы принятия решений (есть ли вообще решение проблемы), так и проблему оптимизации. Задача оптимизации — это псевдобулева задача, связанная с функцией стоимости, то есть суммой членов, которые необходимо минимизировать. Вместо того, чтобы просто пытаться найти модель, удовлетворяющую заданным ограничениям, gophersat попытается найти модель, которая гарантированно удовлетворяет ограничениям и минимизирует функцию стоимости.
Во время поиска оптимальных решений gophersat будет предоставлять субоптимальные решения (т. е. решения, которые устраняют все ограничения, но еще не гарантированно являются оптимальными), как только он их находит, поэтому пользователь может либо получить субоптимальное решение за заданное время. ограничьте или дольше ждите гарантированно оптимального решения.
Да и нет. Он намного быстрее, чем наивные реализации, достаточно быстр, чтобы его можно было использовать для решения реальных задач, но медленнее, чем высокооптимизированные, современные решатели верхнего уровня.
Gophersat не стремится стать самым быстрым из доступных решателей SAT/PB. Цель — предоставить сусликам доступ к технологиям SAT и PB, не прибегая к интерфейсам к решателям, написанным на других языках (обычно C/C++).
Однако в некоторых случаях взаимодействие с решателем, написанным на другом языке, является лучшим выбором для вашего приложения. Если вам нужно решить множество мелких проблем, Gophersat станет самой быстрой альтернативой. Для более серьезных задач, если вы хотите иметь как можно меньше зависимостей за счет времени на решение, Gophersat тоже подойдет. Если вам нужно решать сложные задачи и вы не против использовать cgo или внешнюю программу, Gophersat, вероятно, не лучший вариант.
В Го есть еще несколько решателей SAT, в основном go-sat и gini. Согласно проведенным нами тестам, производительность Gini практически равна производительности Gophersat, хотя в среднем немного медленнее.
Gophersat также предоставляет интересные функции, которые не всегда доступны с другими решателями (например, удобный формат ввода), поэтому его можно использовать в качестве инструмента для описания и решения NP-сложных задач, которые можно легко свести к SAT/PB. проблема.
Нет. Пакет bf (для «логической формулы») предоставляет средства для перевода любой логической формулы в CNF.
Это называется подсчетом моделей, и да, для этого есть функция: solver.Solver.CountModels .
Вы также можете подсчитывать модели из командной строки, используя
gophersat --count filename
где имя файла может быть файлом .opb или .cnf.
