I saw How to convert a propositional formula to conjunctive normal form (CNF)? but it doesn’t go into implementation details. So I was lucky to find this which shows the types:
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; }
Then it has this helpful (start of a) function 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)).
I translated it to JavaScript below, but am stuck on the AND and OR bits. I want to make sure I get this correct too.
The description of my “data model” / data structure is here.
/*
* 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) {
// 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) {
// 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 ~(...), 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
}
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,
}
})
}
I have the AND and OR as a pair. So if you write in math like this:
A ∧ B ∧ C ∧ D ∧ E
That would be more like this in code:
A ∧ (B ∧ (C ∧ (D ∧ E)))
But the problem is, we might have arbitrary trees of formulas:
(((A ∧ B) ∧ (C ∧ D)) ∧ (E ∧ F))
Same with the OR. So how would you implement these functions convertDisjunction and convertConjunction, so they can handle that sort of tree data structure?
So what I would do is this:
function convertConjunction(formula) {
let convertedBase
if (formula.base.type === 'conjunction') {
convertedBase = convertConjunction(formula.base)
}
let convertedHead
if (formula.head.type === 'conjunction') {
convertedHead = convertConjunction(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.
}
I get lost right at the beginning.
