Algorithm implementation to convert propositional formula into conjunctive normal form in JavaScript?

Question

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) {
  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,
    }
  })
}

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?

I tried implementing convertConjunction and convertDisjunction, but I don't think I have it right.

Answer 1

Working around the problem

The problem you raised about the nested conjunction expressions can be worked around by allowing a formula instance to have more than the base and head operands. I would suggest to allow conjunctions and disjunctions to have any number of operands and to store them in an array. So A^B^C^D would be just one conjunction.

I provide an implementation below. It defines one global class Formula which incorporates the sub classes as static members.

A Formula instance should be considered immutable. All methods that return a formula either return an existing formula without change, or will create a new formula.

Example use

// Create variables
const P = Formula.getVariable("P");
const Q = Formula.getVariable("Q");
const R = Formula.getVariable("R");
const S = Formula.getVariable("S");
const T = Formula.getVariable("T");

// Build a formula using the variables
//      (P^Q^~R)v(~S^T)
const formula = P.and(Q).and(R.not()).or(S.not().and(T));

// ...or parse a string (This will create variables where needed)
const formula2 = Formula.parse("(P^Q^~R)v(~S^T)");

// Get the string representation of a formula
console.log("Formula: " + formula);  // (P^Q^~R)v(~S^T)

// Check whether the formula has a CNF structure
console.log("Is it CNF: " + formula.isCnf());  // false

// Create a CNF equivalent for a formula
const cnfFormula = formula.cnf();
console.log("In CNF: " + cnfFormula); // (Pv~S)^(PvT)^(Qv~S)^(QvT)^(~Rv~S)^(~RvT)

// Verify that they are equivalent
console.log("Is equivalent? ", formula.equivalent(cnfFormula)); // true

// Evaluate the formula providing it the set of variables that are true
console.log("When P and T are true, and Q, R and S are false, this evaluates to: ", 
            formula.evaluate(new Set([P,T]))); // true

There should be no need to use new. The program does not have to be aware of the sub classes. The static methods on Formula (namely getVariable and parse) will give you a first formula instance, from which other formulas can be produced.

Be aware that making a CNF can result in large expressions. This code does not attempt to reduce the size by applying many of the rules available for propositional formulas. The returned CNF will always be a conjunction of disjunctions, without simplification. So even when the formula is just a single variable, calling .cnf() on it will turn it into a conjunction of one argument, which in turn is a disjunction of just one argument. Its string representation will still be the variable's name, as the stringification will not add parentheses for connectives which only have one argument.

Implementation

class Formula {
    #args;
    
    constructor(...args) {
        this.#args = args;
    }
    // Methods to return a formula that applied a connective to this formula
    not() {
        return new Formula.#Negation(this);
    }
    and(other) {
        return new Formula.#Conjunction(this, other);
    }
    or(other) {
        return new Formula.#Disjunction(this, other);
    }
    implies(other) {
        return new Formula.#Conditional(this, other);
    }
    
    // ==== Methods that can be overridden by the subclasses ====

    // Evaluate the formula using explicit FALSE/TRUE values.
    // A Variable will evaluate to TRUE if and only when it is in
    //      the Set that is given as argument.
    evaluate(trueVariables) {
        // Default is undefined: subclass MUST override and return boolean
    }
    toString() {
        // Default: subclass can override
        return this.#stringifyArgs().join(this.constructor.symbol);
    }
    // Return whether this formula is in CNF format
    // If level is provided, it verifies whether this formula 
    //    can be at that level within a CNF structure.
    isCnf(level=0) {
        return false; // Default: subclass can override 
    }
    // Return an equivalent formula that is in CNF format
    cnf() {
        return this; // Default: subclass MUST override
    }
    // Get list of all variables used in this formula
    usedVariables() {
        // Formula.Variable should override this
        return [...new Set(this.#args.flatMap(arg => arg.usedVariables()))];
    }
    
    // ==== Methods that are fully implemented (no need to override) ====
    
    // Brute-force way to compare whether two formulas are equivalent:
    //    It provides all the used variables all possible value combinations,
    //    and compares the outcomes.
    equivalent(other) {
        const usedVariables = [...new Set(this.usedVariables().concat(other.usedVariables()))];
        const trueVariables = new Set;
        
        const recur = (i) => {
            if (i >= usedVariables.length) {
                // All usedVariables have a value. Make the evaluation
                return this.evaluate(trueVariables) === other.evaluate(trueVariables);
            }
            trueVariables.delete(usedVariables[i]);
            if (!recur(i + 1)) return false;
            trueVariables.add(usedVariables[i]);
            return recur(i + 1);
        };
        
        return recur(0);
    }
    // Utility functions for mapping the args member
    #cnfArgs() {
        return this.#args.map(arg => arg.cnf());
    }
    #negatedArgs() {
        return this.#args.map(arg => arg.not());
    }
    #evalArgs(trueVariables) {
        return this.#args.map(arg => arg.evaluate(trueVariables));
    }
    #stringifyArgs() {
        return this.#args.length < 2 ? this.#args.map(String) // No parentheses needed
                : this.#args.map(arg => arg.#args.length > 1 ? "(" + arg + ")" : arg + "");
    }
    // Giving a more verbose output than toString(). For debugging.
    dump(indent="") {
        return [
            indent + this.constructor.name + " (", 
            ...this.#args.map(arg => arg.dump(indent + "  ")),
            indent + ")"
        ].join("\n");
    }
    
    // ==== Static members ====
    // Collection of all the variables used in any formula, keyed by name
    static #variables = new Map;
    // Get or create a variable, avoiding different instances for the same name
    static getVariable(name) {
        return this.#variables.get(name) 
                ?? this.#variables.set(name, new this.#Variable(name)).get(name);
    }
    // Parse a string into a Formula.
    // (No error handling: assumes the syntax is valid)
    static parse(str) { 
        const iter = str[Symbol.iterator]();
        
        function recur(end) {
            let formula;
            const connectives = [];
            for (const ch of iter) {
                if (ch === end) break;
                if ("^v~→".includes(ch)) {
                    connectives.push(ch);
                } else {
                    let arg = ch == "(" ? recur(")")
                                        : Formula.getVariable(ch);
                    while (connectives.length) {
                        const oper = connectives.pop();
                        arg = oper == "~" ? arg.not()
                            : oper == "^" ? formula.and(arg)
                            : oper == "v" ? formula.or(arg)
                                          : formula.implies(arg);
                    }
                    formula = arg;
                }
            }
            return formula;
        }
        return recur();
    }

    // Subclasses: private. 
    // There is no need to create instances explicitly
    //    from outside the class.

    static #Variable = class extends Formula {
        #name;
        constructor(name) {
            super();
            this.#name = name;
        }
        evaluate(trueVariables) {
            return trueVariables.has(this);
        }
        toString() {
            return this.#name;
        }
        dump(indent="") {
            return indent + this.constructor.name + " " + this;
        }
        isCnf(level=0) {
            return level >= 2;
        }
        cnf() {
            return new Formula.#Conjunction(new Formula.#Disjunction(this));
        }
        usedVariables() {
            return [this];
        }
    }

    static #Negation = class extends Formula {
        static symbol = "~";
        evaluate(trueVariables) {
            return !this.#evalArgs(trueVariables)[0];
        }
        toString() {
            return this.constructor.symbol + (this.#args[0].#args.length > 1 ? `(${this.#args[0]})` : this.#args[0]); 
        }
        isCnf(level=0) {
            return level == 2 && this.#args[0].isCnf(3);
        }
        cnf() {
            // If this is a negation of a variable, do as if it is a variable
            return this.isCnf(2) ? this.#args[0].cnf.call(this)
                                // Else, sift down the NOT connective
                                 : this.#args[0].negatedCnf(); 
        }
        negatedCnf() {
            return this.#args[0].cnf();
        }
    }

    static #Disjunction = class extends Formula {
        static symbol = "v";
        evaluate(trueVariables) {
            return this.#evalArgs(trueVariables).some(Boolean);
        }
        isCnf(level=0) {
            return level == 1 && this.#args.every(leaf => leaf.isCnf(2));
        }
        cnf() {
            function* cartesian(firstCnf, ...otherCnfs) {
                if (!firstCnf) {
                    yield [];
                    return;
                }
                for (const disj of firstCnf.#args) {
                    for (const combinations of cartesian(...otherCnfs)) {
                        yield [...disj.#args, ...combinations];
                    }
                }
            }
            
            return new Formula.#Conjunction(...Array.from(
                cartesian(...this.#cnfArgs()),
                leaves => new Formula.#Disjunction(...leaves)
            ));
        }
        negatedCnf() {
            return new Formula.#Conjunction(...this.#negatedArgs()).cnf();
        }
    }

    static #Conjunction = class extends Formula {
        static symbol = "^";
        evaluate(trueVariables) {
            return this.#evalArgs(trueVariables).every(Boolean);
        }
        isCnf(level=0) {
            return level === 0 && this.#args.every(disj => disj.isCnf(1));
        }
        cnf() {
            return this.isCnf(0) ? this // already in CNF format
                    : new Formula.#Conjunction(...this.#cnfArgs().flatMap(conj => conj.#args));
        }
        negatedCnf() {
            return new Formula.#Disjunction(...this.#negatedArgs()).cnf();
        }
    }

    static #Conditional = class extends Formula {
        static symbol = "→";
        evaluate(trueVariables) {
            return this.#evalArgs(trueVariables).reduce((a, b) => a <= b);
        }
        cnf() {
            return this.#args[0].not().or(this.#args[1]).cnf();
        }
        negatedCnf() {
            return this.#args[0].and(this.#args[1].not()).cnf();
        }
    }
}

// Examples

// Create variables
const P = Formula.getVariable("P");
const Q = Formula.getVariable("Q");
const R = Formula.getVariable("R");
const S = Formula.getVariable("S");
const T = Formula.getVariable("T");

// Build a formula using the variables
//      (P^Q^~R)v(~S^T)
const formula = P.and(Q).and(R.not()).or(S.not().and(T));

// ...or parse a string (This will create variables where needed)
const formula2 = Formula.parse("(P^Q^~R)v(~S^T)");

// Get the string representation of a formula
console.log("Formula: " + formula);

// Check whether the formula has a CNF structure
console.log("Is it CNF: " + formula.isCnf());

// Create a CNF equivalent for a formula
const cnfFormula = formula.cnf();
console.log("In CNF: " + cnfFormula);

// Verify that they are equivalent
console.log("Is equivalent? ", formula.equivalent(cnfFormula));

// Evaluate the formula providing it the set of variables that are true
console.log("When only P and T are true, this evaluates to: ", formula.evaluate(new Set([P,T])));

Alternative implementation with base and head

The rules you have listed are valid when expressions have nested con/disjunctions. Due to the recursive nature of some of the rules (where the operands are first converted to CNF, and then the top-level connective is converted), the tree's height will gradually be trimmed down as the recursion tracks back.

You indicated in comments you prefer:

• Plain JSON style objects
• Less language specifics
• Plain functions
• Keep base/head pair

So here is tested code that takes these wishes into account:

const VARIABLE = "variable";
const NEGATION = "negation";
const DISJUNCTION = "disjunction";
const CONJUNCTION = "conjunction";
const CONDITION = "condition";

// Factory functions
const variable = name => ({ type: VARIABLE, name });
const not = formula => ({ type: NEGATION, formula });
const connective = (type, base, head) => ({ type, base, head });
const or = connective.bind(null, DISJUNCTION);
const and = connective.bind(null, CONJUNCTION);
const implies = connective.bind(null, CONDITION);

// CNF related functions
function isCnf(formula) {
    return isCnfChild(formula) 
        || formula.type == CONJUNCTION
            && (isCnf(formula.base) || isCnfChild(formula.base))
            && (isCnf(formula.head) || isCnfChild(formula.head));
}
            
function isCnfChild(formula) {
    return isCnfLeaf(formula)
        || formula.type == DISJUNCTION
            && (isCnfChild(formula.base) || isCnfLeaf(formula.base))
            && (isCnfChild(formula.head) || isCnfLeaf(formula.head));
}

function isCnfLeaf(formula) {
    return formula.type == VARIABLE 
        || (formula.type == NEGATION && formula.formula.type == VARIABLE);
}

function cnf(formula) {
    if (isCnf(formula)) {
        return formula;
    }
    switch (formula.type) {
    case NEGATION:
        return negatedCnf(formula.formula);
    case CONJUNCTION:
        return and(cnf(formula.base), cnf(formula.head));
    case DISJUNCTION:
        let base = cnf(formula.base);
        let head = cnf(formula.head);
        return base.type != CONJUNCTION
            ? (head.type != CONJUNCTION
                ? or(base, head)
                : cnf(and(
                    or(base, head.base),
                    or(base, head.head)
                ))
            )
            : (head.type != CONJUNCTION
                ? cnf(and(
                    or(base.base, head),
                    or(base.head, head)
                ))
                : cnf(and(
                    or(base.base, head.base),
                    and(
                        or(base.base, head.head),
                        and(
                            or(base.head, head.base),
                            or(base.head, head.head)
                        )
                    )
                ))
            );
    case CONDITION:
        return cnf(or(not(formula.base), formula.head));
    }
}

function negatedCnf(formula) {
    switch (formula.type) {
    case NEGATION:
        return cnf(formula.formula);
    case DISJUNCTION:
        return cnf(and(not(formula.base), not(formula.head)));
    case CONJUNCTION:
        return cnf(or(not(formula.base), not(formula.head)));
    case CONDITION:
        return cnf(and(formula.base, not(formula.head)));
    }
}

// Evaluation related functions

function usedVariables(formula, collect={}) {
    while (formula.type == NEGATION) {
        formula = formula.formula;
    }
    if (formula.type == VARIABLE) {
        collect[formula.name] = false;
    } else {
        usedVariables(formula.base, collect);
        usedVariables(formula.head, collect);
    }
    return Object.keys(collect);
}

function evaluate(formula, trueVariables) {
    switch (formula.type) {
    case VARIABLE:
        return trueVariables.includes(formula.name);
    case NEGATION:
        return !evaluate(formula.formula, trueVariables);
    case CONJUNCTION:
        return evaluate(formula.base, trueVariables) && evaluate(formula.head, trueVariables);
    case DISJUNCTION:
        return evaluate(formula.base, trueVariables) || evaluate(formula.head, trueVariables);
    case CONDITION:
        return evaluate(formula.base, trueVariables) <= evaluate(formula.head, trueVariables);
    }
}

function isEquivalent(a, b) {
    const variableNames = usedVariables(and(a, b));
    let trueVariables = [];
    
    const recur = (i) => {
        if (i >= variableNames.length) {
            // All trueVariables have a value. Make the evaluation
            return evaluate(a, trueVariables) === evaluate(b, trueVariables);
        }
        trueVariables.push(variableNames[i]);
        if (!recur(i + 1)) return false;
        trueVariables.pop();
        return recur(i + 1);
    };
    
    return recur(0);
}

// String conversion functions

function bracket(formula) {
    if ([VARIABLE, NEGATION].includes(formula.type)) {
        return stringify(formula);
    }
    return "(" + stringify(formula) + ")";
}

function stringify(formula) {
    switch (formula.type) {
    case VARIABLE:
        return formula.name;
    case NEGATION:
        return "~" + bracket(formula.formula);
    case CONJUNCTION:
        return bracket(formula.base) + "^" + bracket(formula.head);
    case DISJUNCTION:
        return bracket(formula.base) + "v" + bracket(formula.head);
    case CONDITION:
        return bracket(formula.base) + "→" + bracket(formula.head);
    }
}

function parse(str) {
    const iter = str[Symbol.iterator]();
        
    function recur(end) {
        let formula;
        const connectives = [];
        for (const ch of iter) {
            if (ch === end) break;
            if ("^v~→".includes(ch)) {
                connectives.push(ch);
            } else {
                let arg = ch == "(" ? recur(")")
                                    : variable(ch);
                while (connectives.length) {
                    const oper = connectives.pop();
                    arg = oper == "~" ? not(arg)
                        : oper == "^" ? and(formula, arg)
                        : oper == "v" ? or(formula, arg)
                                      : implies(formula, arg);
                }
                formula = arg;
            }
        }
        return formula;
    }
    return recur();
}

function demo() {
    // Create variables
    const P = variable("P");
    const Q = variable("Q");
    const R = variable("R");
    const S = variable("S");
    const T = variable("T");

    // Build a formula using the variables
    //      (P^Q^~R)v(~S^T)
    const formula = or(and(and(P, Q), not(R)), and(not(S), T));

    // ...or parse a string (This will create variables where needed)
    const formula2 = parse("(P^Q^~R)v(~S^T)");

    // Get the string representation of a formula
    console.log("Formula: " + stringify(formula));

    // Check whether the formula has a CNF structure
    console.log("Is it CNF: " + isCnf(formula));

    // Create a CNF equivalent for a formula
    const cnfFormula = cnf(formula);
    console.log("In CNF: " + stringify(cnfFormula));

    // Verify that they are equivalent
    console.log("Is equivalent? ", isEquivalent(formula, cnfFormula));

    // Evaluate the formula providing it the set of variables that are true
    console.log("When only P and T are true, this evaluates to: ", evaluate(formula, [P,T]));
}

demo();

Answer 2

I think your tree data structure supports any kinds of nested formula just fine. See the example below where I define a test case of ((A ^ B) V (C ^ D)) ^ E ^ F.

    test = {
        type: 'conjunction',
        base: {
            type: 'disjunction',
            base: {
                type: 'conjunction', 
                base: { type: 'variable', name: 'A'}, 
                head: { type: 'variable', name: 'B'}
            },
            head: {
                type: 'conjunction', 
                base: { type: 'variable', name: 'C'}, 
                head: { type: 'variable', name: 'D'},
            }
        },
        head : {
            type: 'conjunction', 
            base: { type: 'variable', name: 'E'}, 
            head: { type: 'variable', name: 'F'},
        }
    }

What you need is a way to check if a formula is a disjunction of literals (I call it DoL in code for short). Also useful to have a way to check if a formula is CNF.

    function isDisjunctionOfLiteral(formula) {
        if (
          (formula.type === 'variable' ) || 
          (
            formula.type === 'disjunction' && 
            isDisjunctionOfLiteral(formula.base) &&
            isDisjunctionOfLiteral(formula.head)
          )
        ) {return true}
        else {return false}
    }

    function isCNF(formula) {
        if (
          isDisjunctionOfLiteral(formula) ||
          (
            formula.type === 'conjunction' && 
            isCNF(formula.base) &&
            isCNF(formula.head)
          )
        ) {return true}
        else {return false}
    }
    

Now we are ready to implement Conjunction and Disjunction cases (I leave the other 4 cases).

    /*
     * 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
      let cnfBase = convert(formula.base);
      // CONVERT(Q) must have the form Q1 ^ Q2 ^ ... ^ Qn,
      let cnfHead = convert(formula.head);
      // where all the Pi and Qi are disjunctions of literals.

      // So return P1 ^ P2 ^ ... ^ Pm ^ Q1 ^ Q2 ^ ... ^ Qn.
      return {
        type: 'conjunction',
        base: cnfBase ,
        head: cnfHead,
      }
    }
    
    function convertDisjunction(formula) {      
      // CONVERT(P) must have the form P1 ^ P2 ^ ... ^ Pm, and
      let cnfBase = convert(formula.base);
      // CONVERT(Q) must have the form Q1 ^ Q2 ^ ... ^ Qn,
      let cnfHead = convert(formula.head);
      // 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)      
      let finalResult = {type: 'conjunction'}; // finalResult is a tree of conjunctions with m x n elements
      let result = finalResult; // pointer to each element in finalResult
      let prevResult;
      function addEntry(item) {
          result.base = item;
          result.head = {type: 'conjunction'};
          prevResult = result;
          result = result.head;
      }
      forEachDoL(cnfBase, (baseDoL) => {
        forEachDoL(cnfHead, (headDoL) => {
          addEntry({
              type: 'disjunction',
              base: baseDoL,
              head: headDoL
          });
        });
      });
      // finally, fix the last node of the tree 
      // prevResult = prevResult.base; 
      let prevBase = prevResult.base
      prevResult.type = prevBase.type; 
      prevResult.base = prevBase.base; 
      prevResult.head = prevBase.head;           

      return finalResult;
    }
    
    
    function forEachDoL(cnf, callback) {
      if (!isCNF(cnf)) throw new Error('argument is not CNF');
      if (isDisjunctionOfLiteral(cnf)) {
        callback(cnf)
      } else {
        forEachDoL(cnf.base, callback);
        forEachDoL(cnf.head, callback);
      }
    }
    

Finally, included a print function to visualize our test case. It successfully converts ((A ^ B) V (C ^ D)) ^ E ^ F to (A V C) ^ (A V D) ^ (B V C) ^ (B V D) ^ E ^ F.

    function printValues(obj, level) {
        level = level || 0;
        for (var key in obj) {
            if (typeof obj[key] === "object") {
                console.log(" ".repeat(level*2) +  key +  " : ");    
                printValues(obj[key], level + 1);   
            } else {
                console.log(" ".repeat(level*2) +  key + " : " + obj[key]);    
            }
        }
    }
    
    printValues(convert(test));

Answer 3

Here's an approach that tries to follow the algorithm described in that question, and it's fairly close to what was described on Wikipedia.

It doesn't precisely answer your question, as we start with an entirely different model. I hope it might serve as a guide for working with your approach.

We create some factory functions that could be used like this:

Not (Or (Var ('A'), Var ('B')))

to us to build

{
    type: "Not",
    vals: [
        {
            type: "Or",
            vals: [
                {
                    type: "Var",
                    vals: [
                        "A"
                    ]
                },
                {
                    type: "Var",
                    vals: [
                        "B"
                    ]
                }
            ]
        }
    ]
}

and two different functions to turn that into a String:

• stringify yields "not (or (A, B))"
• display yields "~(A v B)"

Note that the formulae all have the same {type, vals} structure, even though Not and Var have only one child and Implies and Equiv each have exactly two. And and Or can have as many as needed, but the factory does try to imply that you will build this with exactly two.

This is not a head/tail list. We could convert it to one with only slight difficulty, but often arrays are easier to work with in JS. Here at one point we slice the array to get an initial portion and again to get a final portion. One of those would likely be trickier with pair-based lists. (This is not at all impossible, but I find this approach simpler.)

We then have a three formula transformation functions:

• negNormForm transforms nested Nots and Nots applied to conjunctions and disjunctions and transforms Implies and Equiv to appropriate Or/And/Not nested structure.

• disjOverConj distributes (P v (Q ^ R)) to make ((P v Q) ^ (P v R)).

• flattenConjDisj turns, for instance ((A v B) v C) into (A v B v C), and similarly for ^

The main function, cnf just composes these three transformations.

The code looks like this:

const Formula = {
  Var: (v) => ({type: 'Var', vals: [v]}),
  And: (p, q, ...ps) => ({type: 'And', vals: [p, q, ...ps]}),
  Or: (p, q, ...ps) => ({type: 'Or', vals: [p, q, ...ps]}),
  Not: (p) => ({type: 'Not', vals: [p]}),
  Implies: (p, q) => ({type: 'Implies', vals: [p, q]}),
  Equiv: (p, q) => ({type: 'Equiv', vals: [p, q]}),
}

const {Var, And, Or, Not, Implies, Equiv} = Formula

const run = (xs) => (formula) => {
  const fn = xs [formula .type] 
  return fn ? fn (formula .vals) : formula
}

const postorder = (fn) => (f) =>
  f .type == 'Var'
    ? fn (f)
    : fn (Formula [f .type] (... f .vals .map (postorder (fn))))


const stringify = run ({
  Var: ([val]) => String (val),
  And: (vals) => `and (${vals .map (stringify) .join (', ')})`,
  Or: (vals) => `or (${vals .map (stringify) .join (', ')})`,
  Not: ([val]) => `not (${stringify (val)})`,
  Implies: ([p, q]) => `implies (${stringify (p)}, ${stringify (q)})`,
  Equiv: ([p, q]) => `equiv (${stringify (p)}, ${stringify (q)})`,
})

const display = run ({
  Var: ([val]) => String (val),
  And: (vals) => `(${vals .map (display) .join (' ^ ')})`,    // or ∧
  Or:  (vals) => `(${vals .map (display) .join (' v ')})`,    // or ∨
  Not: ([val]) => `~${display (val)}`,                        // or ¬
  Implies: ([p, q]) => `(${display (p)} => ${display (q)})`,  // or → 
  Equiv: ([p, q]) => `(${display (p)} <=> ${display (q)})`,   // or ↔
})

const flattenConjDisj = postorder (run ({
  And: (vals) => And (... vals .flatMap ((f) => f.type == 'And' ? f .vals : [f])),
  Or:  (vals) =>  Or (... vals .flatMap ((f) => f.type == 'Or' ? f .vals : [f])),  
}))

const negNorm = postorder (run ({
  Not: ([val]) =>                                  // --\
    val .type == 'Not'                             //    +--- Double-negative
      ? negNorm (val .vals [0])                    // --/
    : val .type == 'And'                           // --\ 
      ? Or (... val .vals .map ((v) => Not (v)))   //    +--- DeMorgan's Laws
    : val .type == 'Or'                            //    |
      ? And (... val .vals .map ((v) => Not (v)))  // --/
    : Not (val),
  Implies: ([p, q]) => Or (Not (p), q),
  Equiv: ([p, q]) => And (Or (p, Not (q)), Or (Not (p), q))
}))

const conjOverDisj = postorder (run ({
  Or: (vals, andIdx = vals .findIndex ((x) => x .type == 'And'), and = vals [andIdx]) =>
    andIdx > -1                                   //--\
      ? And (... and .vals .flatMap (             //   +--- Distribution
          (v) => conjOverDisj ( Or (... vals .slice (0, andIdx), v, ...vals .slice (andIdx + 1)))
        ))                                        //--/
      : Or (...vals),
}))

const cnf = (f) => flattenConjDisj (conjOverDisj (negNorm (f)))


const testCases = [
  Or (Var ('P'), And (Var ('Q'), Var ('R'))),
  Not (Or (Var ('A'), Var ('B'))),
  And (Not (Not (Not (Var ('A')))), Equiv (Var ('B'), Var ('C')),),
  And (Var ('A'), And (Var ('B'), And (Implies (Var ('C'), Var ('D')), Not (Not (Not (Var ('E'))))))),
  Equiv (Var ('P'), Var ('Q')),
   Or (And (Var ('A'), Var ('B')), Var ('C'), And (Var ('D'), Var ('E'))),
]

console .log ('----------------------------------------------')
testCases .forEach ((x) => {
  console .log ('Original: ')
  console .log ('    ' + stringify (x))
  console .log ('    ' + display (x))
  console .log ('Conjunctive Normal Form:')
  console .log ('    ' + stringify (cnf (x)))
  console .log ('    ' + display (cnf (x)))
  console .log ('----------------------------------------------')
})

.as-console-wrapper {max-height: 100% !important; top: 0}

After the factory functions, we have two helpers. postorder walks the tree in a postorder fashion, running a transformation function on each node. run is a small helper, which is best seen by example:

//                 v--------- right here
const stringify = run ({
  Var: ([val]) => String (val),
  And: (vals) => `and (${vals .map (stringify) .join (', ')})`,
  Or: (vals) => `or (${vals .map (stringify) .join (', ')})`,
  Not: ([val]) => `not (${stringify (val)})`,
  Implies: ([p, q]) => `implies (${stringify (p)}, ${stringify (q)})`,
  Equiv: ([p, q]) => `equiv (${stringify (p)}, ${stringify (q)})`,
})

The result of this call, stringify is a function which takes a formula and passes its vals to the appropriate function based on its type. The appropriate formulas are supplied in the configuration object passed to run. This function simplifies the implementations of the other major function here, so it seems worth having, but I can't come up with a good name for it, and that makes me worry that it's not an appropriate abstraction. Still, it works for now. An earlier version looked like this:

const run = (xs) => ({type, vals}) => xs [type] (vals)

That works fine, but it requires the configuration object to handle every type and not just the ones it's interested in. (This is more important for the structure transformations function than for the display and stringify, which have to handle them all anyway.)

The other three main functions, flattenConjDisj, negNorm, and disjOverConj combine run with postorder to transform a tree based on individual type-specific functions.

I think the code for the first two is fairly clear. Please add a comment if it's not. The third one is trickier. We are distributing our And over our Or. Because our Or formulae can have more than two children, we do this recursively until none of the children is an And. When we find an And, we take all its children and combine them with all their peers. So to process this:

((A ^ B) v C v (D ^ E))

We note the first And and expand that, turning this into

((A v C) ^ (B v C)) v (D ^ E))

And then the recursive all expands the second And, yielding

(((A v C v D) ^ (A v C v E)) ^ ((B v C v D) ^ (B v C v E)))

When we call the flattening, that will turn this into

((A v C v D) ^ (A v C v E) ^ (B v C v D) ^ (B v C v E))

Again, if that's not clear, please ask for clarification in the comments.

A fun problem!

---

Note: I realized as I was typing this up that I didn't handle xor. At this point (approaching bedtime), I leave that as an exercise for the reader. It should be straightforward.