SBV lib кажется медленным для решения SAT, как использовать picosat / miniSAT?

В мой последний вопрос Я спросил, как я могу разобрать пропозициональное выражение, а затем найти все модели формулы с помощью библиотеки SBV. Я использовал библиотеку hatt для анализа логического выражения.

К сожалению, SBV кажется, что он либо не подходит для достаточно быстрого решения SAT, либо функция «allSat» для поиска всех моделей не реализована для скорости. Ведь SBV нацелена на решение SMT.

Я тестировал производительность пакета haskell SBV с помощью пруверов Z3 и CVC4 по сравнению с picosat. Я использовал пропозициональную формулу с 36 переменными и 840 действительными моделями. Результат для picosat - 0,5 секунды, Z3 - 3 минуты, а CVC4 - 6 минут. Либо есть некоторые уловки производительности с SBV и функцией "allSat", чтобы обрезать его для пропозициональных формул. Или какой-нибудь другой прувер может быть быстрее Z3.

Но теперь я предполагаю, что мне, вероятно, нужно использовать более быстрый вариант для решения SAT, и я хочу использовать PicoSAT или MiniSAT, поскольку у меня были хорошие результаты в прошлом, а результаты соревнований SAT кажутся хорошими.

Вопросы:

  • Есть ли привязка к Picosat или MiniSAT, которая подходит для поиска всех моделей (т. Е. На уровне C / C ++ для быстрых результатов) пропозициональной формулы? Например, привязки python к picosat имеют функцию itersolve, которая только и делает это. Но я не смог найти эту функцию для привязок haskell picosat или miniSAT (возможно, я их не заметил).

  • Как мне перейти от строки, которая анализируется с помощью пакета hatt, к "списку int", который можно сшить для picosat / miniSat. Таким образом, чтобы перейти от выражения типа Expr в библиотеке hatt к представлению формулы CNF в стиле, подходящем, например, для picosat. Picosat использует общий формат SAT списка целых чисел. Обратите внимание, что мои формулы, полученные из String, изначально уже находятся в CNF. Либо я перехожу прямо из hatt Expr в список int. В противном случае я использую код из мой последний вопрос в формат, подходящий для allSat функции SBV, и переопределить вариант allSAT функции SBV для использования привязок hasekll для picosat / miniSAT.

Ссылки:


haskell smt satisfiability
person mrsteve    schedule 26.04.2014    source источник
comment
Если есть уточняющие вопросы, я нахожусь в другом часовом поясе, чем большинство, поэтому ответы могут занять ~ 20 часов.   -  person mrsteve    schedule 26.04.2014
comment
Обычный способ сделать это - добавить ранее обнаруженное решение в cnf и повторно запустить SAT. Например, если решением является [1,-2,3], вы должны добавить предложение [-1,2,-3].   -  person Thomas M. DuBuisson    schedule 26.04.2014
comment
Функция solveAll, предложенная @ ThomasM.DuBuisson, была добавлена ​​в последние привязки Picosat на Hackage. hackage.haskell.org/package/picosat-0.1.0.2/ docs / Picosat.html   -  person Stephen Diehl    schedule 27.04.2014

Ответы (1)


arrow_upward
1
arrow_downward

Как я сказал в своем комментарии, очень распространенное решение - заставить SAT-решатель искать другие решения, явно добавляя пункт, запрещающий ранее обнаруженные решения. Например:

solveAll :: [[Int]] -> IO [[Int]]
solveAll e =
 do s <- solve e
    case s of
        Solution x -> (x :) `fmap` solveAll (map negate x : e)
        _          -> return []

В приведенном выше примере у нас есть вход CNF для solveAll. Когда решение обнаружено, мы возвращаем это решение и все оставшиеся решения, добавляя отрицание нашего текущего решения в качестве нового предложения. Решающая программа в конечном итоге вернет unsat, что означает, что мы нашли все решения, или неизвестное, что означает, что могут быть неоткрытые решения, но решающая программа отказалась.

Полная программа следует

import Data.Logic.Propositional hiding (interpret)
import Picosat
import Control.Monad ((<=<))

main :: IO ()
main = do
       let expr = [ [1, -2] , [3, -2] ]
       putStrLn $ "Solving expr: " ++ show expr
       (print <=< solve) expr
       (print <=< solveAll) expr

solveAll :: [[Int]] -> IO [[Int]]
solveAll e =
 do s <- solve e
    case s of
        Solution x -> (x :) `fmap` solveAll (map negate x : e)
        _          -> return []
person Thomas M. DuBuisson    schedule 26.04.2014
comment
Это действительно полезная функция, я добавлю ее в библиотеку Picosat. - person Stephen Diehl; 27.04.2014