我看到了如何将命题公式转换为合取范式 (CNF)？但它没有进入实施细节。所以我很幸运地找到了显示类型的这个：
abstract class Formula { }
class Variable extends Formula { String varname; }
class AndFormula extends Formula { Formula p; Formula q; } // conjunction
class OrFormula extends Formula { Formula p; Formula q; } // disjunction
class NotFormula extends Formula { Formula p; } // negation
class ImpliesFormula extends Formula { Formula p; Formula q; } // if-then
class EquivFormula extends Formula { Formula p; Formula q; }
class XorFormula extends Formula { Formula p; Formula q; }
然后它有这个有用的（开始）功能CONVERT：
CONVERT(φ): // returns a CNF formula equivalent to φ
// Any syntactically valid propositional formula φ must fall into
// exactly one of the following 7 cases (that is, it is an instanceof
// one of the 7 subclasses of Formula).
If φ is a variable, then:
return φ.
// this is a CNF formula consisting of 1 clause that contains 1 literal
If φ has the form P ^ Q, then:
CONVERT(P) must have the form P1 ^ P2 ^ ... ^ Pm, and
CONVERT(Q) must have the form Q1 ^ Q2 ^ ... ^ Qn,
where all the Pi and Qi are disjunctions of literals.
So return P1 ^ P2 ^ ... ^ Pm ^ Q1 ^ Q2 ^ ... ^ Qn.
If φ has the form P v Q, then:
CONVERT(P) must have the form P1 ^ P2 ^ ... ^ Pm, and
CONVERT(Q) must have the form Q1 ^ Q2 ^ ... ^ Qn,
where all the Pi and Qi are dijunctions of literals.
So we need a CNF formula equivalent to
(P1 ^ P2 ^ ... ^ Pm) v (Q1 ^ Q2 ^ ... ^ Qn).
So return (P1 v Q1) ^ (P1 v Q2) ^ ... ^ (P1 v Qn)
^ (P2 v Q1) ^ (P2 v Q2) ^ ... ^ (P2 v Qn)
...
^ (Pm v Q1) ^ (Pm v Q2) ^ ... ^ (Pm v Qn)
If φ has the form ~(...), then:
If φ has the form ~A for some variable A, then return φ.
If φ has the form ~(~P), then return CONVERT(P). // double negation
If φ has the form ~(P ^ Q), then return CONVERT(~P v ~Q). // de Morgan's Law
If φ has the form ~(P v Q), then return CONVERT(~P ^ ~Q). // de Morgan's Law
If φ has the form P -> Q, then:
Return CONVERT(~P v Q). // equivalent
If φ has the form P <-> Q, then:
Return CONVERT((P ^ Q) v (~P ^ ~Q)).
If φ has the form P xor Q, then:
Return CONVERT((P ^ ~Q) v (~P ^ Q)).
我将它翻译成下面的 JavaScript，但被困在 AND 和 OR 位上。我想确保我也得到了正确的。
我的“数据模型”/数据结构的描述在这里。
/*
* Any syntactically valid propositional formula φ must fall into
* exactly one of the following 7 cases (that is, it is an instanceof
* one of the 7 subclasses of Formula).
*
* @see https://www.cs.jhu.edu/~jason/tutorials/convert-to-CNF.html
*/
function convert(formula) {
switch (formula.type) {
case 'variable': return formula
case 'conjunction': return convertConjunction(formula)
case 'disjunction': return convertDisjunction(formula)
case 'negation': return convertNegation(formula)
case 'conditional': return convertConditional(formula)
case 'biconditional': return convertBiconditional(formula)
case 'xor': return convertXOR(formula)
default:
throw new Error(`Unknown formula type ${formula.type}.`)
}
}
function convertConjunction(formula) {
return {
type: 'conjunction',
base: convert(formula.base),
head: convert(formula.head),
}
// CONVERT(P) must have the form P1 ^ P2 ^ ... ^ Pm, and
// CONVERT(Q) must have the form Q1 ^ Q2 ^ ... ^ Qn,
// where all the Pi and Qi are disjunctions of literals.
// So return P1 ^ P2 ^ ... ^ Pm ^ Q1 ^ Q2 ^ ... ^ Qn.
}
function convertDisjunction(formula) {
return {
type: 'disjunction',
base: convert(formula.base),
head: convert(formula.head),
}
// CONVERT(P) must have the form P1 ^ P2 ^ ... ^ Pm, and
// CONVERT(Q) must have the form Q1 ^ Q2 ^ ... ^ Qn,
// where all the Pi and Qi are dijunctions of literals.
// So we need a CNF formula equivalent to
// (P1 ^ P2 ^ ... ^ Pm) v (Q1 ^ Q2 ^ ... ^ Qn).
// So return (P1 v Q1) ^ (P1 v Q2) ^ ... ^ (P1 v Qn)
// ^ (P2 v Q1) ^ (P2 v Q2) ^ ... ^ (P2 v Qn)
// ...
// ^ (Pm v Q1) ^ (Pm v Q2) ^ ... ^ (Pm v Qn)
}
function convertNegation(formula) {
// If φ has the form ~A for some variable A, then return φ.
if (formula.formula.type === 'variable') {
return formula
}
// If φ has the form ~(~P), then return CONVERT(P). // double negation
if (formula.formula.type === 'negation') {
return convert(formula.formula.formula)
}
// If φ has the form ~(P ^ Q), then return CONVERT(~P v ~Q). // de Morgan's Law
if (formula.formula.type === 'conjunction') {
return convert({
type: 'disjunction',
base: {
type: 'negation',
formula: formula.formula.base,
},
head: {
type: 'negation',
formula: formula.formula.head,
}
})
}
// If φ has the form ~(P v Q), then return CONVERT(~P ^ ~Q). // de Morgan's Law
if (formula.formula.type === 'disjunction') {
return convert({
type: 'conjunction',
base: {
type: 'negation',
formula: formula.formula.base
},
head: {
type: 'negation',
formula: formula.formula.head
}
})
}
throw new Error(`Invalid negation.`)
}
function convertConditional(formula) {
// Return CONVERT(~P v Q). // equivalent
return convert({
type: 'disjunction',
base: {
type: 'negation',
formula: formula.base,
},
head: formula.head
})
}
function convertBiconditional(formula) {
// Return CONVERT((P ^ Q) v (~P ^ ~Q)).
return convert({
type: 'disjunction',
base: {
type: 'conjunction',
base: formula.base,
head: formula.head,
},
head: {
type: 'conjunction',
base: {
type: 'negation',
formula: formula.base,
},
head: {
type: 'negation',
formula: formula.head,
},
}
})
}
function convertXOR(formula) {
// CONVERT((P ^ ~Q) v (~P ^ Q)).
return convert({
type: 'disjunction',
base: {
type: 'conjunction',
base: formula.base,
head: {
type: 'negation',
formula: formula.head,
},
},
head: {
type: 'conjunction',
base: {
type: 'negation',
formula: formula.base,
},
head: formula.head,
}
})
}我有 AND 和 OR 作为一对。所以，如果你这样写数学：
A ∧ B ∧ C ∧ D ∧ E
在代码中会更像这样：
A ∧ (B ∧ (C ∧ (D ∧ E)))
但问题是，我们可能有任意的公式树：
(((A ∧ B) ∧ (C ∧ D)) ∧ (E ∧ F))
与 OR 相同。那么你将如何实现这些函数convertDisjunction和convertConjunction，以便它们可以处理那种树数据结构呢？
我尝试实现convertConjunctionand convertDisjunction，但我认为我做的不对。