如何在haskell中生成隨機命題公式（CNF）？

如何在haskell中獲得一個隨機命題公式？最好我需要在CNF的公式，但我會如何在haskell中生成隨機命題公式（CNF）？

我想要使用公式進行性能測試，也涉及SAT求解器。請注意，我的目標不是測試SAT求解器的性能！我也對非常困難的公式不感興趣，所以難度應該是隨機的，否則只包含簡單的公式。

我知道我的真實世界的數據導致命題公式，這對SAT解算器來說並不困難。

目前我使用hatt和SBV庫作爲數據結構來處理命題公式。我也看了一下hGen庫，也許它可以用來生成隨機公式。但是沒有任何文檔，通過查看hGen的源代碼，我沒有得到太多的結果。

我的目標是選擇n並取回包含n布爾變量的公式。

來源

2014-04-30 mrsteve

如果你想隨機產生一些東西，我建議一個非確定性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-30 01:21:38 luqui

monadrandom這應該真正被稱爲「隨機性單子」而不是「nondetermism單子」 –

@PhilipJF，我想到的是，那個'[]'＆CO通常被稱爲不確定性，但我沒有看到爲什麼稱蘭德爲非確定性單子會是不正確的。從語義上講，它屬於同一個家族。你知道一個很好的理由嗎？ – luqui

好吧，monadrandom會產生一個結果的概率分佈，這與非確定性實際上不是一回事，它在語義上只是給你一個集合。 –

在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-30 01:47:15 user2407038

如何在haskell中生成隨機命題公式（CNF）？

回答

相關問題