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

Question

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

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

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

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

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

Answer 1

Раскрытие, я - автор упомянутых вами привязок на Haskell picosat.

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

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

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

Answer 2

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

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

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

import Data.SBV.Bridge.Z3

против

import Data.SBV.Bridge.Boolector

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