ninetynine-1.3.0: Ninety-Nine Haskell Problems
CopyrightCopyright (C) 2023 Yoo Chung
LicenseGPL-3.0-or-later
Maintainerdev@chungyc.org
Safe HaskellSafe-Inferred
LanguageGHC2021

Problems.P52

Description

Part of Ninety-Nine Haskell Problems. Some solutions are in Solutions.P52.

Synopsis

Documentation

toConjunctiveNormalForm :: Formula -> Formula Source #

It is known that any boolean function can be represented in conjunctive normal form. These are conjunctions of disjunctions of literals, where literals are one of boolean values, variables, or the complement of values or variables. For example, the boolean formula \(\neg(x \wedge \neg y) \wedge (z \vee w)\) is equivalent to the conjunctive normal form \( (\neg x \vee y) \wedge (z \vee w) \).

Return the conjunctive normal form of a boolean formula. The value returned should always be a conjunction of disjunctions.

Examples

>>> toConjunctiveNormalForm $ Value True
Conjoin [Disjoin [Value True]]

>>> toConjunctiveNormalForm $ Complement $ Disjoin [Variable "X", Variable "Y"]
Conjoin [Disjoin [Complement (Variable "X")],Disjoin [Complement (Variable "Y")]]

>>> :{
toConjunctiveNormalForm $ Disjoin [ Variable "X"
                                  , Conjoin [ Complement $ Variable "Y"
                                            , Variable "Z"
                                            ]
                                  ]
:}
Conjoin [Disjoin [Variable "X",Complement (Variable "Y")],Disjoin ...

Hint

Expand

Transform a boolean formula using De Morgan's law, the distributive law, and double negation elimination to reduce nesting. Alternatively, the conjunctive normal form can be obtained easily from the truth table, although this will always require a running time exponential to the number of variables.

data Formula Source #

Represents a boolean formula.

Constructors

Value Bool

A constant value.

Variable String

A variable with given name.

Complement Formula

Logical complement. I.e., it is true only if its clause is false.

Disjoin [Formula]

Disjunction. I.e., it is true if any of its clauses are true.

Conjoin [Formula]

Conjunction. I.e., it is true only if all of its clauses are true.

Instances

Instances details
Generic Formula Source # 
Instance details

Defined in Problems.Logic

Associated Types

type Rep Formula :: Type -> Type #

Methods

from :: Formula -> Rep Formula x #

to :: Rep Formula x -> Formula #

Show Formula Source # 
Instance details

Defined in Problems.Logic

Methods

showsPrec :: Int -> Formula -> ShowS #

show :: Formula -> String #

showList :: [Formula] -> ShowS #

NFData Formula Source # 
Instance details

Defined in Problems.Logic

Methods

rnf :: Formula -> () #

Eq Formula Source # 
Instance details

Defined in Problems.Logic

Methods

(==) :: Formula -> Formula -> Bool #

(/=) :: Formula -> Formula -> Bool #

Ord Formula Source # 
Instance details

Defined in Problems.Logic

Methods

compare :: Formula -> Formula -> Ordering #

(<) :: Formula -> Formula -> Bool #

(<=) :: Formula -> Formula -> Bool #

(>) :: Formula -> Formula -> Bool #

(>=) :: Formula -> Formula -> Bool #

max :: Formula -> Formula -> Formula #

min :: Formula -> Formula -> Formula #

type Rep Formula Source # 
Instance details

Defined in Problems.Logic

type Rep Formula = D1 ('MetaData "Formula" "Problems.Logic" "ninetynine-1.3.0-4Xxr3hBGtJH9Ff8qb2Invo" 'False) ((C1 ('MetaCons "Value" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: C1 ('MetaCons "Variable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: (C1 ('MetaCons "Complement" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Formula)) :+: (C1 ('MetaCons "Disjoin" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Formula])) :+: C1 ('MetaCons "Conjoin" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Formula])))))

Supporting functions

The function below is not part of the problem.

evaluateFormula :: Map String Bool -> Formula -> Bool Source #

Evaluate a boolean formula with the given mapping of variable names to values.