How to generate a random propositional formula (CNF) in haskell?

Question

How can I get a random propositional formula in haskell? Preferably I need the formula in CNF, but I would

I want to use the formulas for performance testing that also involves SAT solvers. Please note that my goal is not to test the performance of SAT solvers! I am also not interested in very difficult formulas, so the difficulty should be random or otherwise only include easy formulas.

I know that my real world data leads to propositional formulas that are not difficult for SAT solvers.

At the moment I use the hatt and SBV libraries as data structures to work with propositional formulas. I also looked at the hGen library, perhaps it can be used to generate the random formulas. However there is no documentation and I didn’t get far by looking at the source code of hGen.

My goal is to chose n and get back a formula that includes n boolean variables.

Answer 1

If you want to generate something randomly, I suggest a nondeterminism monad, of which MonadRandom is a popular choice.

I would suggest two inputs to this procedure: vars, the number of variables, and clauses the number of clauses. Of course you could always generate the number of clauses at random as well, using this same idea. Here's a sketch:

import Control.Monad.Random (Rand, StdGen, uniform)
import Control.Applicative ((<$>))
import Control.Monad (replicateM)

type Cloud = Rand StdGen  -- for "probability cloud"

newtype Var = Var Int
data Atom = Positive Var   -- X
          | Negative Var   -- not X

type CNF = [[Atom]]  -- conjunction of disjunctions

genCNF :: Int -> Int -> Cloud CNF
genCNF vars clauses = replicateM clauses genClause
    where
    genClause :: Could [Atom]
    genClause = replicateM 3 genAtom  -- for CNF-3

    genAtom :: Cloud Atom
    genAtom = do
        f <- uniform [Positive, Negative]
        v <- Var <$> uniform [0..vars-1]
        return (f v)

I included the optional type signatures in the where clause to make it easier to follow the structure.

Essentially, follow the "grammar" of what you are trying to generate; with each nonterminal associate with a gen* function.

I don't know how to judge whether a CNF expression is easy or hard.

Answer 2

Using the types in hatt:

import Data.Logic.Propositional
import System.Random
import Control.Monad.State 
import Data.Maybe
import Data.SBV

type Rand = State StdGen 

rand :: Random a => (a, a) -> Rand a 
rand = state . randomR 

runRand :: Rand a -> IO a 
runRand r = randomIO >>= return . fst . runState r . mkStdGen 

randFormula :: Rand Expr 
randFormula = rand (3, 10) >>= randFormulaN 50  

randFormulaN :: Int -> Int -> Rand Expr 
randFormulaN negC n = replicateM n clause >>= return . foldl1 Conjunction 
  where vars = take n (map (Variable . Var) ['a'..])

        clause = rand (1, n) >>= mapM f . flip take vars >>= return . foldl1 Disjunction 

        f v = rand (0,100) >>= \neg -> return (if neg <= negC then Negation v else v)