SBV lib는 SAT 해결을 위해 느려지는 것처럼 보입니다. picosat/miniSAT를 사용하는 방법은 무엇입니까?

Question

my last question에서 나는 명제 표현을 구문 분석 한 다음 SBV 라이브러리를 사용하여 수식의 모든 모델을 찾을 수있는 방법을 물었습니다. 부울 식을 구문 분석하기 위해 hatt 라이브러리를 사용했습니다.

유감스럽게도 SBV는 합리적으로 빠른 SAT 해결에 적합하지 않거나 모든 모델을 찾기위한 "allSat"기능이 속도를 위해 구현되지 않은 것처럼 보입니다. 모든 SBV가 SMT 해결을 목표로 한 후에.

필자는 Z3 및 CVC4를 사용하여 haskell SBV 패키지의 성능을 피코사스와 비교하여 테스트했습니다. 36 개의 변수와 840 개의 유효한 모델을 가진 명제식을 사용했습니다. 피코사드 결과는 Z3가 3 분, CVC4가 6 분이 소요되는 반면 0.5 초가 걸렸습니다. SBV 및 "allSat"기능을 사용하여 몇 가지 성능 트릭을 사용하여 명제식을 다듬을 수 있습니다. 또는 다른 증명 장치가 Z3보다 빠를 수도 있습니다.

하지만 이제는 SAT 해결에 더 빠른 옵션을 사용해야한다고 생각합니다. 과거에는 좋은 결과를 얻었으므로 PicoSAT 또는 MiniSAT를 사용하고 SAT 경기 결과는 좋게 보입니다.

질문 :

• 이되는 적합 Picosat 또는 MiniSAT 하나에 바인딩 모든 모델을 찾을 수있는 (즉, 빠른 결과를위한 C/C++ 단째) 명제 화학식? 예를 들어, 파이썬 바인딩에 파이썬 기능은 "itersolve"기능을 가지고 있습니다. 하지만 haskell picosat 또는 miniSAT 바인딩에 대해이 기능을 찾지 못했습니다 (아마도 내가 간과 한 것 같습니다).

• hatt 패키지로 구문 분석 된 문자열에서 picosat/miniSat에 대해 sutable 인 "int list"로 어떻게 진행해야합니까? 따라서, hatt 라이브러리 내의 타입 Expr의 표현식으로부터, 예를 들어, 피코사스 (picosat)에 적합한 스타일로 CNF 공식을 나타낼 수있다. Picosat은 int 목록의 일반적인 SAT 형식을 사용합니다. String에서 파싱 된 수식은 원래 CNF에 이미 있습니다. 어느 것이 든 hart Expr에서 int리스트로 직접 이동합니다. 그렇지 않으면 my last question의 코드를 SBV의 allSat 기능에 적합한 형식으로 사용하고 SBV의 allSAT 기능의 변형을 다시 구현하여 picosat/miniSAT의 hasekll 바인딩을 사용합니다.

링크 :

• my last question
• SBV library
• hatt library
• haskell picosat bindings
• minitSAT

Answer 1

제가 말씀 드렸듯이 매우 일반적인 해결책은 SAT 솔버가 이전에 발견 된 솔루션을 제거하는 조항을 명시 적으로 추가하여 다른 솔루션을 찾도록하는 것입니다. 예를 들어 위의에서

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

우리는 solveAll에 CNF 입력을 가지고있다. 솔루션이 발견되면 현재 솔루션의 부정을 새로운 절로 추가하여 해당 솔루션과 나머지 솔루션을 모두 반환합니다.솔버는 결국 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 []