Как сгенерировать формулу случайных высказываний (CNF) в haskell?

Как я могу получить случайную пропозициональную формулу в haskell? Предпочтительно мне нужна формула в CNF, но я бы

Я хочу использовать формулы для тестирования производительности, которые также включают решатели SAT. Обратите внимание, что моей целью не является тестирование производительности SAT-решателей! Меня также не интересуют очень сложные формулы, поэтому сложность должна быть случайной или включать только простые формулы.

Я знаю, что мои данные из реального мира приводят к пропозициональным формулам, которые несложны для решателей SAT.

На данный момент я использую шляпу и Библиотеки SBV как структуры данных для работы с пропозициональными формулами. Я также просмотрел библиотеку hGen, возможно, ее можно использовать для генерации случайных формул. Однако документации нет, и я не продвинулся далеко, просмотрев исходный код hGen.

Моя цель — выбрать n и получить формулу, включающую n логических переменных.


haskell smt satisfiability
person mrsteve    schedule 30.04.2014    source источник

Ответы (2)


arrow_upward
5
arrow_downward

Если вы хотите сгенерировать что-то случайным образом, я предлагаю монаду недетерминизма, из которых 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 простым или сложным.

person luqui    schedule 30.04.2014
comment
monadrandom это действительно должно называться монадой случайности, а не монадой недетерминизма - person Philip JF; 30.04.2014
comment
@PhilipJF, я думал об этом, что [] и другие обычно называют недетерминизмом, но я не вижу причин, по которым называть Rand монадой недетерминизма было бы неправильно. Это в той же семье, семантически говоря. Знаете уважительную причину? - person luqui; 30.04.2014
comment
Что ж, монослучайность дает распределение вероятностей результатов, что на самом деле не то же самое, что недетерминизм, который, с точки зрения семантики, просто дает вам множество. - person Philip JF; 30.04.2014

arrow_upward
3
arrow_downward

Использование типов в 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)
person user2407038    schedule 30.04.2014