Simpler unifiers for equations with fewer variables on one of the sides

src/BoolUnification.js

@@ -50,7 +50,16 @@ export function boolUnify(f1, f2) {
     let query = mkXor(f1, f2)
 
     // The free variables in the query.
-    let fvs = boolFreeVars(query)
+    // 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 < fvsF1.length
+        ? [...fvsF2,...fvsF1.filter(v => !fvsF2.includes(v))]
+        : [...fvsF1,...fvsF2.filter(v => !fvsF1.includes(v))]
 
     try {
         let subst = successiveVariableElimination(query, fvs)

src/Bools.js

@@ -123,6 +123,12 @@ 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}
@@ -145,6 +151,12 @@ 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}
@@ -161,6 +173,30 @@ export function mkXor(f1, f2) {
     return mkOr(mkAnd(f1, mkNot(f2)), mkAnd(mkNot(f1), 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.
  */
@@ -295,15 +331,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))
     }
 }
 
@@ -434,6 +470,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.
  */
@@ -448,8 +492,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).join("")
+
         // Look it up in the table.
-        let minimal = MinTable[resultVector]
+        let minimal = MinTable[resultId]
         if (minimal === undefined) {
             // Not found.
             return f