JavaScript中将命题公式转换为合取范式的算法实现？
Algorithm implementation to convert propositional formula into conjunctive normal form in JavaScript?
我看到 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 显示类型：
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 位上。我也想确保我的理解正确。
我的“数据模型”/数据结构的描述是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,
}
})
}
我有一对 AND 和 OR。所以如果你这样写数学：
A ∧ B ∧ C ∧ D ∧ E
在代码中更像这样：
A ∧ (B ∧ (C ∧ (D ∧ E)))
但问题是，我们可能有任意的公式树：
(((A ∧ B) ∧ (C ∧ D)) ∧ (E ∧ F))
与手术室相同。那么你将如何实现这些函数 convertDisjunction 和 convertConjunction，以便它们可以处理那种树数据结构？
我尝试实施 convertConjunction 和 convertDisjunction，但我认为我做对了。
解决问题
您提出的有关嵌套连词表达式的问题可以通过以下方式解决
允许公式实例有多个 base 和 head 操作数。我建议允许
连词和析取具有任意数量的操作数并将它们存储在数组中。所以 A^B^C^D
将只是一个连词。
我在下面提供了一个实现。它定义了一个全局 class Formula 其中包含
sub classes 作为静态成员。
一个Formula实例应该被认为是不可变的。 return 公式的所有方法
return 现有公式不变，或者将创建一个新公式。
使用示例
// 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。该程序不必知道子 classes。
Formula 上的静态方法（即 getVariable 和 parse）将为您提供第一个公式实例，
可以从中产生其他公式。
请注意，制作 CNF 可能会导致大型表达式。此代码不会尝试
通过应用许多可用于命题公式的规则来减少大小。 returned CNF 将永远是
析取的结合，没有简化。所以即使公式只是一个变量，
在其上调用 .cnf() 会将其变成一个参数的合取，而这又是一个参数的析取。
它的字符串表示仍然是变量的名称，因为字符串化不会为连接词添加括号
只有一个参数。
实施
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])));
base 和 head
的替代实施
当表达式嵌套 con/disjunctions 时，您列出的规则有效。由于某些规则的递归性质（先将操作数转换为CNF，然后再转换top-level连接词），树的高度将随着递归回溯而逐渐被修剪。
您在评论中表示您更喜欢：
- 普通 JSON 样式对象
- 较少的语言细节
- 普通函数
- 保持base/head对
所以这里是经过测试的代码，考虑了这些愿望：
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();
我认为你的树数据结构支持任何类型的嵌套公式就好了。请参阅下面的示例，其中我定义了 ((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'},
}
}
你需要的是一种方法来检查 formula 是否是文字的析取（我在代码中简称为 DoL）。有一种方法来检查 formula 是否是 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}
}
现在我们已经准备好实现合取和析取的情况（我留下其他 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));
这是一种尝试遵循该问题中描述的算法的方法，它与维基百科上描述的算法非常接近。
它没有准确回答您的问题，因为我们从一个完全不同的模型开始。我希望它可以作为使用您的方法的指南。
我们创建了一些可以像这样使用的工厂函数：
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} 结构，即使 Not 和 Var 只有一个 child 和 Implies 和 Equiv每个正好有两个。 And 和 Or 可以根据需要有多少，但工厂确实试图暗示你将只用两个来构建它。
这不是 head/tail 列表。我们可以轻松地将它转换为一个数组，但通常数组在 JS 中更容易使用。在这一点上，我们 slice 数组获得初始部分并再次获得最终部分。其中之一对于 pair-based 列表可能会更棘手。 （这并非完全不可能，但我觉得这种方法更简单。）
那么我们就有了三个公式转换函数：
negNormForm 转换嵌套的 Nots 和 Nots 应用于连词和析取，并将 Implies 和 Equiv 转换为适当的 Or/And/Not 嵌套结构。
disjOverConj分发(P v (Q ^ R))制作((P v Q) ^ (P v R)).
flattenConjDisj 将 ((A v B) v C) 变为 (A v B v C)，^
也类似
主函数，cnf就是组合了这三个变换。
代码如下所示：
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}
工厂功能完成后，我们有两个帮手。 postorder 以后序方式遍历树，运行 每个节点上的转换函数。 run是个小帮手，最好看例子：
// 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)})`,
})
此调用的结果 stringify 是一个函数，它采用公式并将其 vals 传递给基于其 type 的适当函数。在传递给 run 的配置 object 中提供了适当的公式。这个函数在这里简化了另一个主要函数的实现，所以看起来值得拥有，但我无法为它想出一个好名字，这让我担心它不是一个合适的抽象。尽管如此，它现在仍然有效。早期版本如下所示：
const run = (xs) => ({type, vals}) => xs [type] (vals)
工作正常，但它需要配置 object 来处理每种类型，而不仅仅是它感兴趣的类型。（这对于结构转换功能比 display 更重要和 stringify，无论如何都必须处理它们。）
其他三个主要函数，flattenConjDisj、negNorm和disjOverConj结合run和postorder根据个体type-specific 函数。
我认为前两个的代码相当清楚。如果不是，请添加评论。第三个更棘手。我们将 And 分配给 Or。因为我们的 Or 公式可以有两个以上的 children，所以我们递归地这样做，直到 children 的 none 是一个 And。当我们找到一个 And 时，我们将它的所有 children 与它们的所有对等体结合起来。所以要处理这个：
((A ^ B) v C v (D ^ E))
我们记下第一个 And 并展开它，将其变成
((A v C) ^ (B v C)) v (D ^ E))
然后递归全部扩展第二个And，产生
(((A v C v D) ^ (A v C v E)) ^ ((B v C v D) ^ (B v C v E)))
当我们调用扁平化时，它会变成
((A v C v D) ^ (A v C v E) ^ (B v C v D) ^ (B v C v E))
再次强调，如果不清楚，请在评论中寻求澄清。
一个有趣的问题！
注意：我在输入时意识到我没有处理 xor。在这一点上（临近就寝时间），我将其留作 reader 的练习。它应该是直截了当的。
我看到 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 显示类型：
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 位上。我也想确保我的理解正确。
我的“数据模型”/数据结构的描述是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,
}
})
}
我有一对 AND 和 OR。所以如果你这样写数学：
A ∧ B ∧ C ∧ D ∧ E
在代码中更像这样：
A ∧ (B ∧ (C ∧ (D ∧ E)))
但问题是，我们可能有任意的公式树：
(((A ∧ B) ∧ (C ∧ D)) ∧ (E ∧ F))
与手术室相同。那么你将如何实现这些函数 convertDisjunction 和 convertConjunction，以便它们可以处理那种树数据结构？
我尝试实施 convertConjunction 和 convertDisjunction，但我认为我做对了。
解决问题
您提出的有关嵌套连词表达式的问题可以通过以下方式解决
允许公式实例有多个 base 和 head 操作数。我建议允许
连词和析取具有任意数量的操作数并将它们存储在数组中。所以 A^B^C^D
将只是一个连词。
我在下面提供了一个实现。它定义了一个全局 class Formula 其中包含
sub classes 作为静态成员。
一个Formula实例应该被认为是不可变的。 return 公式的所有方法
return 现有公式不变，或者将创建一个新公式。
使用示例
// 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。该程序不必知道子 classes。
Formula 上的静态方法（即 getVariable 和 parse）将为您提供第一个公式实例，
可以从中产生其他公式。
请注意，制作 CNF 可能会导致大型表达式。此代码不会尝试
通过应用许多可用于命题公式的规则来减少大小。 returned CNF 将永远是
析取的结合，没有简化。所以即使公式只是一个变量，
在其上调用 .cnf() 会将其变成一个参数的合取，而这又是一个参数的析取。
它的字符串表示仍然是变量的名称，因为字符串化不会为连接词添加括号
只有一个参数。
实施
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])));
base 和 head
的替代实施
当表达式嵌套 con/disjunctions 时，您列出的规则有效。由于某些规则的递归性质（先将操作数转换为CNF，然后再转换top-level连接词），树的高度将随着递归回溯而逐渐被修剪。
您在评论中表示您更喜欢：
- 普通 JSON 样式对象
- 较少的语言细节
- 普通函数
- 保持base/head对
所以这里是经过测试的代码，考虑了这些愿望：
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();
我认为你的树数据结构支持任何类型的嵌套公式就好了。请参阅下面的示例，其中我定义了 ((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'},
}
}
你需要的是一种方法来检查 formula 是否是文字的析取（我在代码中简称为 DoL）。有一种方法来检查 formula 是否是 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}
}
现在我们已经准备好实现合取和析取的情况（我留下其他 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));
这是一种尝试遵循该问题中描述的算法的方法，它与维基百科上描述的算法非常接近。
它没有准确回答您的问题，因为我们从一个完全不同的模型开始。我希望它可以作为使用您的方法的指南。
我们创建了一些可以像这样使用的工厂函数：
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} 结构，即使 Not 和 Var 只有一个 child 和 Implies 和 Equiv每个正好有两个。 And 和 Or 可以根据需要有多少，但工厂确实试图暗示你将只用两个来构建它。
这不是 head/tail 列表。我们可以轻松地将它转换为一个数组，但通常数组在 JS 中更容易使用。在这一点上，我们 slice 数组获得初始部分并再次获得最终部分。其中之一对于 pair-based 列表可能会更棘手。 （这并非完全不可能，但我觉得这种方法更简单。）
那么我们就有了三个公式转换函数：
negNormForm转换嵌套的Nots 和Nots应用于连词和析取，并将Implies和Equiv转换为适当的Or/And/Not嵌套结构。disjOverConj分发(P v (Q ^ R))制作((P v Q) ^ (P v R)).
例如，
也类似flattenConjDisj将((A v B) v C)变为(A v B v C)，^
主函数，cnf就是组合了这三个变换。
代码如下所示：
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}
工厂功能完成后，我们有两个帮手。 postorder 以后序方式遍历树，运行 每个节点上的转换函数。 run是个小帮手，最好看例子：
// 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)})`,
})
此调用的结果 stringify 是一个函数，它采用公式并将其 vals 传递给基于其 type 的适当函数。在传递给 run 的配置 object 中提供了适当的公式。这个函数在这里简化了另一个主要函数的实现，所以看起来值得拥有，但我无法为它想出一个好名字，这让我担心它不是一个合适的抽象。尽管如此，它现在仍然有效。早期版本如下所示：
const run = (xs) => ({type, vals}) => xs [type] (vals)
工作正常，但它需要配置 object 来处理每种类型，而不仅仅是它感兴趣的类型。（这对于结构转换功能比 display 更重要和 stringify，无论如何都必须处理它们。）
其他三个主要函数，flattenConjDisj、negNorm和disjOverConj结合run和postorder根据个体type-specific 函数。
我认为前两个的代码相当清楚。如果不是，请添加评论。第三个更棘手。我们将 And 分配给 Or。因为我们的 Or 公式可以有两个以上的 children，所以我们递归地这样做，直到 children 的 none 是一个 And。当我们找到一个 And 时，我们将它的所有 children 与它们的所有对等体结合起来。所以要处理这个：
((A ^ B) v C v (D ^ E))
我们记下第一个 And 并展开它，将其变成
((A v C) ^ (B v C)) v (D ^ E))
然后递归全部扩展第二个And，产生
(((A v C v D) ^ (A v C v E)) ^ ((B v C v D) ^ (B v C v E)))
当我们调用扁平化时，它会变成
((A v C v D) ^ (A v C v E) ^ (B v C v D) ^ (B v C v E))
再次强调，如果不清楚，请在评论中寻求澄清。
一个有趣的问题！
注意：我在输入时意识到我没有处理 xor。在这一点上（临近就寝时间），我将其留作 reader 的练习。它应该是直截了当的。