6

如何在haskell中获得随机命题公式？最好我需要 CNF 中的公式，但我会

我想使用公式进行性能测试，也涉及 SAT 求解器。请注意，我的目标不是测试 SAT 求解器的性能！我也对非常困难的公式不感兴趣，所以难度应该是随机的，否则只包括简单的公式。

我知道我的真实世界数据导致的命题公式对于 SAT 求解者来说并不困难。

目前，我使用hatt和SBV库作为数据结构来处理命题公式。我还查看了hGen库，也许它可以用来生成随机公式。但是没有文档，而且我通过查看hGen的源代码也没有走多远。

我的目标是选择n并取回一个包含n布尔变量的公式。

4

2 回答 2

6

如果你想随机生成一些东西，我建议使用非确定性 monad，其中MonadRandom是一种流行的选择。

我建议这个过程有两个输入：vars变量clauses的数量和子句的数量。当然，您也可以使用相同的想法随机生成子句的数量。这是一个草图：

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)

我在子句中包含了可选的类型签名，where以便更容易遵循结构。

本质上，遵循您尝试生成的“语法”；每个非终结符都与一个gen*函数相关联。

我不知道如何判断一个 CNF 表达式是简单还是困难。

于 2014-04-30T01:21:38.177 回答
3

使用中的类型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)
于 2014-04-30T01:47:15.513 回答