Jak wygenerować losową formułę zdaniową (CNF) w haskell?

Question

Jak mogę uzyskać losową formułę zdaniową w haskell? Najlepiej potrzebuję formuły w CNF, ale chciałbym

Chcę używać formuły do ​​testowania wydajności, który obejmuje również solvers SAT. Proszę zwrócić uwagę, że moim celem nie jest sprawdzenie działania solwerów SAT! Nie interesują mnie też bardzo trudne formuły, więc trudność powinna być losowa lub zawierać jedynie proste formuły.

Wiem, że moje dane z prawdziwego świata prowadzą do formuł zdań, które nie są trudne dla solwerów SAT.

W tej chwili używam bibliotek hatt i SBV jako struktur danych do pracy z formułami zdaniowymi. Spojrzałem również na bibliotekę hGen, być może można jej użyć do generowania losowych formuł. Jednak nie ma dokumentacji i nie zaszedłem daleko, patrząc na kod źródłowy hGen.

Mój cel polega na wybraniu n i odzyskaniu formuły zawierającej zmienne boolean n.

Answer 1

Jeśli chcesz coś wygenerować losowo, proponuję niedoterministyczną monadę, której popularnym wyborem jest MonadRandom.

Proponuję dwa wejścia do tej procedury: vars, liczbę zmiennych i clauses liczbę klauzul. Oczywiście zawsze możesz wygenerować liczbę zdań również losowo, używając tego samego pomysłu. Oto szkic:

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) 

włączyłem opcjonalne podpisy typu w klauzuli where aby łatwiej śledzić strukturę.

Zasadniczo przestrzegaj "gramatyki" tego, co próbujesz wygenerować; z każdym nieterminalnym współpracownikiem z funkcją gen*.

Nie wiem, jak ocenić, czy wyrażenie CNF jest łatwe czy trudne.

Answer 2

Korzystanie typy w 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)