P52 - 合取范式

2026-09-07 00:00    #Haskell   #99题   #逻辑  

P52 - 合取范式

Conjunctive normal form

官方模块：Problems.P52　核心函数：toConjunctiveNormalForm

← P51 纠错码 | P53 归结原理 →

题目描述

将命题逻辑公式转换为合取范式（CNF）。CNF 是子句的合取，每个子句是文字的析取。

数据类型

1import Data.List (nub, sort)
2
3data Formula
4  = Value Bool | Variable String | Complement Formula
5  | Disjoin [Formula] | Conjoin [Formula]
6  deriving (Eq, Ord, Show)

函数签名

1toConjunctiveNormalForm :: Formula -> Formula

实现

方法一：真值表法（枚举所有 falsifying 行）

 1toConjunctiveNormalForm :: Formula -> Formula
 2toConjunctiveNormalForm formula = Conjoin
 3  [ Disjoin [literal name value | (name,value) <- env]
 4  | env <- environments (variables formula)
 5  , not (evaluate env formula)
 6  ]
 7  where
 8    literal name True  = Complement (Variable name)
 9    literal name False = Variable name
10
11variables :: Formula -> [String]
12variables (Value _)      = []
13variables (Variable x)   = [x]
14variables (Complement f) = variables f
15variables (Disjoin fs)   = sort . nub $ concatMap variables fs
16variables (Conjoin fs)   = sort . nub $ concatMap variables fs
17
18environments :: [String] -> [[(String, Bool)]]
19environments [] = [[]]
20environments (x:xs) =
21  [(x,value) : env | value <- [False,True], env <- environments xs]
22
23evaluate :: [(String, Bool)] -> Formula -> Bool
24evaluate _   (Value b)      = b
25evaluate env (Variable x)   = maybe False id (lookup x env)
26evaluate env (Complement f) = not (evaluate env f)
27evaluate env (Disjoin fs)   = any (evaluate env) fs
28evaluate env (Conjoin fs)   = all (evaluate env) fs

对于每个使公式为假的环境，生成一个对应子句排除它。

方法二：代数变换法

 1toConjunctiveNormalForm :: Formula -> Formula
 2toConjunctiveNormalForm = fromClauses . cnfClauses . toNNF
 3  where
 4    fromClauses clauses = Conjoin (map Disjoin clauses)
 5
 6    toNNF (Complement (Conjoin fs)) = Disjoin (map (toNNF . Complement) fs)
 7    toNNF (Complement (Disjoin fs)) = Conjoin (map (toNNF . Complement) fs)
 8    toNNF (Complement (Complement f)) = toNNF f
 9    toNNF (Complement (Value b)) = Value (not b)
10    toNNF (Conjoin fs) = Conjoin (map toNNF fs)
11    toNNF (Disjoin fs) = Disjoin (map toNNF fs)
12    toNNF f = f
13
14    cnfClauses (Value True)  = []
15    cnfClauses (Value False) = [[]]
16    cnfClauses (Conjoin fs)  = concatMap cnfClauses fs
17    cnfClauses (Disjoin fs)  = foldl distribute [[]] (map cnfClauses fs)
18    cnfClauses literal       = [[literal]]
19
20    distribute left right =
21      [nub (leftClause ++ rightClause)
22      | leftClause <- left, rightClause <- right]

toNNF 先用德摩根律把否定推到变量上。cnfClauses 用 [[Formula]] 表示“子句的合取”，遇到析取时计算两个子句集合的笛卡尔积，从而完整应用分配律。这个方法不枚举真值环境，通常比方法一生成更紧凑的 CNF。

方法对比

方法特点代价
真值表定义直接，结果容易验证变量数为 n 时枚举 2^n 个环境
代数变换不枚举赋值，保留公式结构分配律仍可能导致指数膨胀

测试

1>>> toConjunctiveNormalForm (Disjoin [Variable "x", Variable "y"])
2Conjoin [Disjoin [Variable "x",Variable "y"]]
3>>> toConjunctiveNormalForm
4...   (Disjoin [Variable "x", Conjoin [Variable "y", Variable "z"]])
5Conjoin [Disjoin [Variable "x",Variable "y"],Disjoin [Variable "x",Variable "z"]]

参考