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

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.

Solution

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.