From 83f267a178bc7f4b056b7f9c78e5d7244838a256 Mon Sep 17 00:00:00 2001 From: Robert Kleffner Date: Fri, 14 Jan 2022 23:56:42 +0000 Subject: [PATCH 1/5] Implement Jaco's idea, with some Boolean identities that make the MGUs minimal in a lot of common cases. --- src/BoolUnification.js | 29 ++++++++++------------------- src/Bools.js | 40 ++++++++++++++++++++++++++++++++++++++-- 2 files changed, 48 insertions(+), 21 deletions(-) diff --git a/src/BoolUnification.js b/src/BoolUnification.js index 7440db3..77d41e0 100644 --- a/src/BoolUnification.js +++ b/src/BoolUnification.js @@ -27,22 +27,20 @@ export function boolUnify(f1, f2) { throw new Error(`Illegal argument 'y': ${f2}.`) } - // Special case for when one side of the equation is a variable. This will generate a - // 'simpler' substitution than SVE, especially when the equation side has lots of variables. - if (isSingleVarSpecialCase(f1, f2)) { - let subst = {[f1.name]: f2} - return {status: "success", subst: subst} - } - if (isSingleVarSpecialCase(f2, f1)) { - let subst = {[f2.name]: f1} - return {status: "success", subst: subst} - } - // The boolean expression we want to show is 0. let query = mkOr(mkAnd(f1, mkNot(f2)), mkAnd(mkNot(f1), f2)) // The free variables in the query. - let fvs = boolFreeVars(query) + // Idea by Jaco van de Pol: We check to see if one + // side of the equation has a single variable here, and put + // it first in the list of free variables, so that SVE will + // eliminate one side first. SVE will generate a smaller, more + // intuitive MGU as a result. + let fvsF1 = boolFreeVars(f1) + let fvsF2 = boolFreeVars(f2) + let fvs = fvsF2.length == 1 + ? [...fvsF2,...fvsF1] + : [...fvsF1,...fvsF2] try { let subst = successiveVariableElimination(query, fvs) @@ -128,13 +126,6 @@ function satisfiable(f) { } } -/** - * Check whether an equation is of the form `Var(X) =? Equation`, where X not in free(Equation). - */ -function isSingleVarSpecialCase(maybeVar, maybeAssigned) { - return isVar(maybeVar) && !boolFreeVars(maybeAssigned).includes(maybeVar.name); -} - /** * A custom exception used in the successive variable elimination algorithm. */ diff --git a/src/Bools.js b/src/Bools.js index 026bc56..949fb4b 100644 --- a/src/Bools.js +++ b/src/Bools.js @@ -109,7 +109,7 @@ export function mkNot(f) { /** * Returns the conjunction of the two formulas `f1` and `f2`. */ -export function mkAnd(f1, f2) { + export function mkAnd(f1, f2) { if (f1 === undefined || !isBool(f1)) throw new Error(`Illegal argument 'f1': ${f1}.`) if (f2 === undefined || !isBool(f2)) throw new Error(`Illegal argument 'f2': ${f2}.`) @@ -123,13 +123,19 @@ export function mkAnd(f1, f2) { return FALSE } else if (isSyntacticEq(f1, f2)) { return f1 + } else if (isComplement(f1, f2)) { + return FALSE + } else if (isAndAbsorption(f1, f2)) { + return f1 + } else if (isAndAbsorption(f2, f1)) { + return f2 } return {type: 'AND', f1: f1, f2: f2} } /** - * Returns the disjunction of the two formulas `f1` and `f2`. + * Returns the inclusive disjunction of the two formulas `f1` and `f2`. */ export function mkOr(f1, f2) { if (f1 === undefined || !isBool(f1)) throw new Error(`Illegal argument 'f1': ${f1}.`) @@ -145,11 +151,41 @@ export function mkOr(f1, f2) { return f1 } else if (isSyntacticEq(f1, f2)) { return f1 + } else if (isComplement(f1, f2)) { + return TRUE + } else if (isOrAbsorption(f1, f2)) { + return f1 + } else if (isOrAbsorption(f2, f1)) { + return f2 } return {type: 'OR', f1: f1, f2: f2} } +/** + * Returns `true` if `f1` is the syntactic complement of `f2`. + */ +function isComplement(f1, f2) { + return (isNot(f2) && isSyntacticEq(f1, f2.f)) + || (isNot(f1) && isSyntacticEq(f2, f1.f)) +} + +/** + * Returns `true` if `f` is a syntactic component of `absorb`, + * e.g. `f && (? || f) = true` or `f && (f || ?) = true` + */ + function isAndAbsorption(f, absorb) { + return isOr(absorb) && (isSyntacticEq(f, absorb.f2) || isSyntacticEq(f, absorb.f1)) +} + +/** + * Returns `true` if `f` is a syntactic component of `absorb`, + * e.g. `f || (? && f) = true` or `f || (f && ?) = true` + */ +function isOrAbsorption(f, absorb) { + return isAnd(absorb) && (isSyntacticEq(f, absorb.f2) || isSyntacticEq(f, absorb.f1)) +} + /** * Returns `true` if the Boolean formulas `f1` and `f2` are *syntactically* equal. */ From e90c4e72ba409319495dd2865966289e4ae20f6d Mon Sep 17 00:00:00 2001 From: Robert Kleffner Date: Sat, 15 Jan 2022 00:08:25 +0000 Subject: [PATCH 2/5] Make sure duplicate vars from both sides of equation don't get eliminated twice by SVE. --- src/BoolUnification.js | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/BoolUnification.js b/src/BoolUnification.js index 77d41e0..23aff03 100644 --- a/src/BoolUnification.js +++ b/src/BoolUnification.js @@ -39,8 +39,8 @@ export function boolUnify(f1, f2) { let fvsF1 = boolFreeVars(f1) let fvsF2 = boolFreeVars(f2) let fvs = fvsF2.length == 1 - ? [...fvsF2,...fvsF1] - : [...fvsF1,...fvsF2] + ? [...fvsF2,...fvsF1.filter(v => !fvsF2.includes(v))] + : [...fvsF1,...fvsF2.filter(v => !fvsF1.includes(v))] try { let subst = successiveVariableElimination(query, fvs) From cc18208d4821ebc54cb1011926d54f29cd9df15b Mon Sep 17 00:00:00 2001 From: Robert Kleffner Date: Sat, 15 Jan 2022 00:35:51 +0000 Subject: [PATCH 3/5] Cleanup after looking at diff. --- src/BoolUnification.js | 2 +- src/Bools.js | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/BoolUnification.js b/src/BoolUnification.js index 23aff03..1c00583 100644 --- a/src/BoolUnification.js +++ b/src/BoolUnification.js @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -import {FALSE, boolFreeVars, isBool, isFalse, isTrue, mkAnd, mkNot, mkOr, mkVar, showBool, TRUE, isVar} from "./Bools.js"; +import {FALSE, boolFreeVars, isBool, isFalse, isTrue, mkAnd, mkNot, mkOr, mkVar, showBool, TRUE} from "./Bools.js"; import {applySubst} from "./Substitution"; /** diff --git a/src/Bools.js b/src/Bools.js index 949fb4b..6e49052 100644 --- a/src/Bools.js +++ b/src/Bools.js @@ -109,7 +109,7 @@ export function mkNot(f) { /** * Returns the conjunction of the two formulas `f1` and `f2`. */ - export function mkAnd(f1, f2) { +export function mkAnd(f1, f2) { if (f1 === undefined || !isBool(f1)) throw new Error(`Illegal argument 'f1': ${f1}.`) if (f2 === undefined || !isBool(f2)) throw new Error(`Illegal argument 'f2': ${f2}.`) @@ -135,7 +135,7 @@ export function mkNot(f) { } /** - * Returns the inclusive disjunction of the two formulas `f1` and `f2`. + * Returns the disjunction of the two formulas `f1` and `f2`. */ export function mkOr(f1, f2) { if (f1 === undefined || !isBool(f1)) throw new Error(`Illegal argument 'f1': ${f1}.`) From fcdc1fbba07c8ea79069810c30347f9e57496c21 Mon Sep 17 00:00:00 2001 From: Robert Kleffner Date: Sat, 15 Jan 2022 17:12:47 +0000 Subject: [PATCH 4/5] Slight generalization of Jaco's idea. Easy minimization cases that work for all free variable counts. A couple additional identities. --- src/BoolUnification.js | 12 ++++++------ src/Bools.js | 27 ++++++++++++++++++++++----- 2 files changed, 28 insertions(+), 11 deletions(-) diff --git a/src/BoolUnification.js b/src/BoolUnification.js index 1c00583..72b8de3 100644 --- a/src/BoolUnification.js +++ b/src/BoolUnification.js @@ -31,14 +31,14 @@ export function boolUnify(f1, f2) { let query = mkOr(mkAnd(f1, mkNot(f2)), mkAnd(mkNot(f1), f2)) // The free variables in the query. - // Idea by Jaco van de Pol: We check to see if one - // side of the equation has a single variable here, and put - // it first in the list of free variables, so that SVE will - // eliminate one side first. SVE will generate a smaller, more - // intuitive MGU as a result. + // Generalization of an idea by Jaco van de Pol: We check to see + // if one side of the equation has fewer free variables, and put + // those first in the list of free variables, so that SVE will + // eliminate the smaller side first. SVE will generate a smaller, + // more intuitive MGU as a result. let fvsF1 = boolFreeVars(f1) let fvsF2 = boolFreeVars(f2) - let fvs = fvsF2.length == 1 + let fvs = fvsF2.length < fvsF1.length ? [...fvsF2,...fvsF1.filter(v => !fvsF2.includes(v))] : [...fvsF1,...fvsF2.filter(v => !fvsF1.includes(v))] diff --git a/src/Bools.js b/src/Bools.js index 6e49052..74ed920 100644 --- a/src/Bools.js +++ b/src/Bools.js @@ -174,7 +174,7 @@ function isComplement(f1, f2) { * Returns `true` if `f` is a syntactic component of `absorb`, * e.g. `f && (? || f) = true` or `f && (f || ?) = true` */ - function isAndAbsorption(f, absorb) { +function isAndAbsorption(f, absorb) { return isOr(absorb) && (isSyntacticEq(f, absorb.f2) || isSyntacticEq(f, absorb.f1)) } @@ -320,15 +320,15 @@ export function truthRow(f, fvs) { if (fvs.length === 0) { if (isTrue(f)) { - return "T" + return [f] } else if (isFalse(f)) { - return "F" + return [f] } else { throw new Error(`Unexpected value 'f': ${f}.`) } } else { let [x, ...xs] = fvs - return truthRow(applySubst({[x]: TRUE}, f), xs) + truthRow(applySubst({[x]: FALSE}, f), xs) + return truthRow(applySubst({[x]: TRUE}, f), xs).concat(truthRow(applySubst({[x]: FALSE}, f), xs)) } } @@ -459,6 +459,14 @@ entries.forEach(elm => { MinTable[key] = parseSExp(formula) }); +function truthElemString(b) { + if (isTrue(b)) { + return "T" + } else { + return "F" + } +} + /** * Looks up the formula `f` in the cached table of minimal formulas. */ @@ -473,8 +481,17 @@ function lookup(f) { let fvs = boolFreeVars(f) let resultVector = truthRow(f, fvs) + // Easy cases that work without any table, for any number of variables. + if (resultVector.every((r) => r == FALSE)) { + return FALSE + } else if (resultVector.every((r) => r == TRUE)) { + return TRUE + } + + let resultId = resultVector.map(truthElemString) + // Look it up in the table. - let minimal = MinTable[resultVector] + let minimal = MinTable[resultId] if (minimal === undefined) { // Not found. return f From d4ed1328528a7d011bd6af90382831e77a29b908 Mon Sep 17 00:00:00 2001 From: Robert Kleffner Date: Sat, 15 Jan 2022 17:42:09 +0000 Subject: [PATCH 5/5] Fix bug in making a minimization table accessor. --- src/Bools.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Bools.js b/src/Bools.js index a344b79..2022a3a 100644 --- a/src/Bools.js +++ b/src/Bools.js @@ -499,7 +499,7 @@ function lookup(f) { return TRUE } - let resultId = resultVector.map(truthElemString) + let resultId = resultVector.map(truthElemString).join("") // Look it up in the table. let minimal = MinTable[resultId]