Haskell: привязка к быстрому и простому решению SAT

Question

Сегодня я тоже хотел изучить варианты решения SAT в haskell. Сначала я решил написать собственный интерфейс для решения picosat.

Тогда я узнал, что есть SBV library. Это интерфейсы к Z3, Yices, CVC4 и Boolector.

Кроме того, я сделал поиск в google на github, и он проскакивает, есть даже Picosat binding.

Есть ли какие-либо другие привязки haskell для SAT-решателей, на которые стоит обратить внимание, учитывая ограничение быстрой/высокой производительности. Карификация: это подходит для высокопроизводительных SAT-решений (например, проблем, которые работают в течение нескольких дней, а также проблем, которые необходимо выполнить как можно быстрее, когда я проверяю проблемы с S^2 или 20 или более). Например, то, что я особенно не хватает в хаке, является привязкой к быстрому решению SAR-решения parrallel, например, Plingeling. (Кроме того, я узнал о текущем обновлении привязки picosat на github больше случайно, и я очень хорошо мог пропустить другие варианты)

По умолчанию для библиотеки SBV используется решатель Z3 SMT. Правильно ли я понял, что пикосат быстрее для простого решения SAT, чем Z3?

Answer 1

Раскрытие информации, я являюсь автором связок Haskell picosat, которые вы упомянули.

SBV - это действительно надежная библиотека, которая существует некоторое время, хорошо, если вы хотите использовать интерфейс для внешних SMT или SAT-решателей, таких как Yices или Z3. Picosat - это гораздо более простая библиотека, которую я написал просто потому, что мне нужна библиотека, которую можно было установить просто без внешних зависимостей.

Я правильно понял, что пикосат быстрее для простого решения SAT, чем Z3?

Я не знаю, что ваши ограничения производительности являются, но, насколько базовые библиотеки решатель идти, вы не будете замечать существенную разницу между Z3 или Picosat, пока вы не попали действительно огромные проблемы (миллиарды переменных) , Обе библиотеки очень сильно оптимизированы, и узкое место (по крайней мере, со стороны Haskell), вероятно, будет собирать данные между библиотекой и временем выполнения Haskell.

Answer 2

SBV является потокобезопасным.

Сравнение Z3 и Lingeling для производительности SAT - непростая задача. Я бы рискнул предположить, что они будут более или менее одинаковыми, если вы не потратите свое время, чтобы выяснить точные параметры, чтобы точно настроить их внутреннюю эвристику.

Хорошая вещь, что ЗСО обеспечивает общий интерфейс, так что вы можете изменить решатель, просто импортируя другой мост:

import Data.SBV.Bridge.Z3

против

import Data.SBV.Bridge.Boolector

и если вы скомпилируйте boolector, чтобы использовать lingeling, тогда вы можете легко проверить производительность, просто изменив одну строку Haskell.