Come generare una formula proposizionale casuale (CNF) in haskell?

Question

Come posso ottenere una formula proposizionale casuale in haskell? Preferibilmente ho bisogno della formula in CNF, ma vorrei

Voglio usare le formule per il test delle prestazioni che coinvolge anche i risolutori SAT. Tieni presente che il mio obiettivo non è quello di testare le prestazioni dei solutori SAT! Inoltre, non sono interessato a formule molto difficili, quindi la difficoltà dovrebbe essere casuale o comunque includere solo formule semplici.

So che i dati del mio mondo reale portano a formule proposizionali che non sono difficili per i risolutori SAT.

Al momento utilizzo le librerie hatt e SBV come strutture dati per lavorare con formule proposizionali. Ho anche guardato la libreria hGen, forse può essere usata per generare le formule casuali. Tuttavia non c'è documentazione e non sono andato lontano guardando il codice sorgente di hGen.

Il mio obiettivo è scegliere n e recuperare una formula che include le variabili booleane n.

Answer 1

Se si desidera generare qualcosa a caso, suggerisco un monade non deterministico, di cui MonadRandom è una scelta popolare.

Vorrei suggerire due input per questa procedura: vars, il numero di variabili e clauses il numero di clausole. Ovviamente potresti sempre generare il numero di clausole a caso, usando la stessa idea. Ecco uno schizzo:

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) 

ho incluso le firme di tipo opzionali nella clausola where per rendere più facile seguire la struttura.

In sostanza, seguire la "grammatica" di ciò che si sta tentando di generare; con ogni associato non terminale con una funzione gen*.

Non so come giudicare se un'espressione CNF è facile o difficile.

Answer 2

Utilizzando i tipi 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)