हैकेल में एक यादृच्छिक प्रस्ताव सूत्र (सीएनएफ) कैसे उत्पन्न करें?

Question

मैं हैकेल में एक यादृच्छिक प्रस्ताव सूत्र कैसे प्राप्त कर सकता हूं? अधिमानतः मैं CNF में सूत्र की जरूरत है, लेकिन मैं

मैं निष्पादन परीक्षण है कि भी सैट समाधानकर्ताओं शामिल है के लिए फार्मूले का उपयोग करना चाहते हैं। कृपया ध्यान दें कि मेरा लक्ष्य एसएटी सॉल्वर के प्रदर्शन का परीक्षण नहीं करना है! मुझे बहुत मुश्किल सूत्रों में भी रूचि नहीं है, इसलिए कठिनाई यादृच्छिक होनी चाहिए या अन्यथा केवल आसान सूत्र शामिल हैं।

मुझे पता है कि मेरी असली दुनिया डेटा प्रोपोज़िशनल सूत्रों को सैट समाधानकर्ताओं के लिए मुश्किल नहीं कर रहे हैं की ओर जाता है।

फिलहाल मैं hatt और SBV पुस्तकालयों का उपयोग प्रोपोज़िशनल सूत्रों के साथ काम करने के लिए डेटा संरचनाओं के रूप में करता हूं। मैंने hGen लाइब्रेरी को भी देखा, शायद इसका उपयोग यादृच्छिक सूत्र उत्पन्न करने के लिए किया जा सकता है। हालांकि वहां कोई दस्तावेज नहीं है और hGen के स्रोत कोड को देखकर मैं दूर नहीं आया।

मेरा लक्ष्य n चुनना है और एक सूत्र वापस प्राप्त करना है जिसमें n बूलियन चर शामिल हैं।

Answer 1

आप कुछ बेतरतीब ढंग से उत्पन्न करने के लिए चाहते हैं, तो मैं एक nondeterminism इकाई, जिनमें से 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* फ़ंक्शन के साथ प्रत्येक nonterminal सहयोगी के साथ।

मैं न्याय के लिए कैसे है कि क्या एक CNF अभिव्यक्ति आसान या मुश्किल है पता नहीं है।

Answer 2

प्रकार का उपयोग करना 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)