喇叭-可满足性
一般说来,命题公式可满足性,或者说SAT问题,是NP-完全问题,因此是难以证明的。
幸运的是,有一种特殊情况叫做喇叭可满足性,它可以用线性时间与负字数成正比地求解。
喇叭条款有一个形式是这样的A & B & C … => P
,或者等效地可写成¬A ∨ ¬B ∨ ¬C ∨ … ∨ P
。因此,析取形式的公式包含一组有限的负数(最多包含一个正数)。我们通常能识别出三种公式。
- 规则: Q => P
- 事实: true => P
- 目标: P => false
我昨天实现的函数功能conc就可以用这样的逻辑来写。
要“调用”这个程序,我们要要求这个目标是可满足性的。
Prolog解释将试图解决这个问题,并通过反证法找到答案。
算法实现
测试