4

In my last question I asked how I can parse an propositional expression and then find all models of the formula with the help of the SBV library. I used the hatt library to parse the boolean expression.

Unfortunately, the SBV seems like it is either unsuitable for reasonably fast SAT solving, or the "allSat" function to find all models is not implemented for speed. After all SBV is aimed at SMT solving.

I tested the performance of haskell SBV package using the provers Z3 and CVC4 compared to picosat. I used a propositional formula with 36 variables and 840 valid models. The result for picosat is that it took 0.5 seconds, while Z3 took 3 minutes and CVC4 took 6 minutes. Either there is some performance tricks with SBV and the "allSat" function to trim it for propositional formulas. Or some other prover might be faster than Z3.

But I assume now that I probably need to use a faster option for SAT solving and I want to use PicoSAT or MiniSAT as I had good results in the past and SAT competitions results seem good.

Questions:

  • Is there a binding to either Picosat or MiniSAT that is suitable to find all models (i.e., on the C/C++ level for fast results) of a propositional formula? For instance, the python bindings to picosat feature a function "itersolve" that just does that. But I could not find this function for the haskell picosat or miniSAT bindings (perhaps I overlooked them).

  • How should I proceed from a String that is parsed with the hatt package to a "int list" that is sutable for picosat/miniSat. Thus to go from an expression of type Expr in the hatt library to an represent a CNF formula in a style suitable for, e.g., picosat. Picosat uses the common SAT format of a list of ints. Please note that my formulas parsed from the String are originally already in CNF. Either I go directly from an hatt Expr to the int list. Or otherwise, I use the code from my last question to a format suitable for the allSat function of SBV and reimplement a variant of the allSAT function of SBV to use hasekll bindings of picosat/miniSAT.

Links:

Community
  • 1
  • 1
mrsteve
  • 4,082
  • 1
  • 26
  • 63
  • if there are clarification questions, I am in a different time zone than most, so it might take ~20 hours for my answers. – mrsteve Apr 26 '14 at 19:37
  • 1
    A common way to do this is to add the previously discovered solution to the cnf and re-run the SAT. For example, if a solution is `[1,-2,3]` then you would add the clause `[-1,2,-3]`. – Thomas M. DuBuisson Apr 26 '14 at 19:44
  • The `solveAll` function proposed by @ThomasM.DuBuisson has been added to the latest Picosat bindings on Hackage. http://hackage.haskell.org/package/picosat-0.1.0.2/docs/Picosat.html – Stephen Diehl Apr 27 '14 at 00:01

1 Answers1

1

As I said in my comment, a very common solution is to force the SAT solver to look for other solutions by explicitly adding a clause dis-allowing previously discovered solutions. For example:

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

In the above we have a CNF input to solveAll. When a solution is discovered we return that solution and all remaining solutions by adding the negation of our currently solution as a new clause. The solver will eventually return unsat, which suggests we have found all solutions, or unknown, which means there might be undiscovered solutions but the solver has given up.

A complete program follows

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 []
Thomas M. DuBuisson
  • 64,245
  • 7
  • 109
  • 166