4

前回の質問で、SBV ライブラリを利用して命題式を解析し、式のすべてのモデルを見つける方法を尋ねました。ブール式の解析には hatt ライブラリを使用しました。

残念ながら、SBV はかなり高速な SAT 解決には適していないか、すべてのモデルを検索する「allSat」機能が高速化のために実装されていないようです。やはりSBVはSMT解決を目指しています。

picosat と比較して、プルーバー Z3 および CVC4 を使用して、haskell SBV パッケージのパフォーマンスをテストしました。36 個の変数と 840 個の有効なモデルを含む命題の公式を使用しました。picosat の結果は、0.5 秒かかったのに対し、Z3 は 3 分、CVC4 は 6 分かかりました。SBV と "allSat" 関数を使用して、命題の式のためにそれをトリミングするためのいくつかのパフォーマンスのトリックがあります。または、他の証明者が Z3 よりも高速である可能性があります。

しかし、SAT を解くにはより高速なオプションを使用する必要があると思います。過去に良い結果があり、SAT 競技の結果も良さそうなので、PicoSAT または MiniSAT を使用したいと考えています。

質問:

  • 命題式のすべてのモデル (つまり、高速な結果を得るための C/C++ レベル)を見つけるのに適した、Picosat または MiniSAT へのバインディングはありますか? たとえば、picosat への python バインディングは、それを行う関数「itersolve」を備えています。しかし、haskell の picosat や miniSAT のバインディングについては、この関数を見つけることができませんでした (おそらく見落としていたのでしょう)。

  • hatt パッケージで解析された文字列から、picosat/miniSat に適した「int リスト」に進むにはどうすればよいですか。したがってExpr、hatt ライブラリの型の式から、たとえば picosat に適したスタイルで CNF 式を表現することになります。Picosat は、int のリストの一般的な SAT 形式を使用します。文字列から解析された私の数式は、もともと既に CNF にあることに注意してください。または、hatt Expr から int リストに直接移動します。または、前回の質問のコードを SBVの機能に適した形式に使用し、SBVallSatの機能のバリアントを再実装して、allSATpicosat/miniSAT の hasekll バインディングを使用します。

リンク:

4

1 に答える 1

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 []

上記では、 への CNF 入力がありsolveAllます。解決策が発見されると、現在の解決策の否定を新しい節として追加することにより、その解決策と残りのすべての解決策を返します。ソルバーは最終的に unsat を返します。これは、すべての解が見つかったことを示します。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 []
于 2014-04-26T19:56:47.570 に答える