javascriptalgorithmmathlogicconjunctive-normal-form

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

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.

Solution

  • 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:

    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();