我看到了如何將命題公式轉換為合取范式 (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，但我認為我做的不對。

uj5u.com熱心網友回復：

解決問題

您提出的關于嵌套連詞運算式的問題可以通過允許公式實體具有多于baseandhead運算元來解決。我建議允許連詞和析取有任意數量的運算元并將它們存盤在一個陣列中。所以A^B^C^D 只有一個連詞。

我在下面提供了一個實作。Formula它定義了一個將子類合并為靜態成員的全域類。

一個Formula實體應該被認為是不可變的。所有回傳公式的方法要么原樣回傳現有公式，要么創建一個新公式。

示例使用

// 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

應該沒有必要使用new. 程式不必知道子類。Formula(即getVariableand )上的靜態方法parse將為您提供第一個公式實體，從中可以生成其他公式。

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

uj5u.com熱心網友回復：

這是一種嘗試遵循該問題中描述的演算法的方法，它與維基百科上的描述非常接近。

它并不能準確回答您的問題，因為我們從一個完全不同的模型開始。我希望它可以作為使用您的方法的指南。

我們創建了一些可以像這樣使用的工廠函式：

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

給我們建造

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

和兩個不同的函式把它變成一個字串：

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

請注意，這些公式都具有相同的{type, vals}結構，即使NotandVar只有一個孩子，Implies并且Equiv每個都有兩個孩子。 And并且Or可以根據需要擁有任意數量，但工廠確實試圖暗示您將使用兩個來構建它。

這不是head/tail串列。我們可以輕松地將其轉換為 1，但陣列通常更容易在 JS 中使用。在這里，我們slice有一次使用陣列來獲取初始部分，然后再次獲取最終部分。其中之一對于基于對的串列可能會更棘手。（這并非不可能，但我發現這種方法更簡單。）

那么我們就有了三個公式轉換函式：

• negNormForm轉換嵌套Nots 并Nots應用于連詞和析取以及轉換和Implies適當Equiv的Or//嵌套結構。AndNot

• disjOverConj分發(P v (Q ^ R))使((P v Q) ^ (P v R))。

• flattenConjDisj變成，例如((A v B) v C)變成(A v B v C)，并且類似地^

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

同樣，如果不清楚，請在評論中要求澄清。

一個有趣的問題！

注意：我在打字時意識到我沒有處理xor。在這一點上（接近就寢時間），我把它留給讀者作為練習。它應該是直截了當的。

uj5u.com熱心網友回復：

我認為您的樹資料結構可以很好地支持任何型別的嵌套公式。請參閱下面的示例，其中我定義了((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'},
        }
    }

您需要的是一種方法來檢查 aformula是否是文字的析取（我在代碼中簡稱為 DoL）。有一種方法來檢查 aformula是否是 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}
    }
    

現在我們已經準備好實作 Conjunction 和 Disjunction 案例（我留下其他 4 個案例）。

    /*
     * 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);
      }
    }
    

最后，包含一個列印功能來可視化我們的測驗用例。它成功轉換((A ^ B) V (C ^ D)) ^ E ^ F為(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));

標籤：

上一篇：在Python中使用Start和Enddate在Dataframe中查找交集

下一篇：使用Haskell檢查有效日期