[Part 8] Raymond Smullyan's Certified Knights and Knaves puzzles Puzzle #6 - Finding solutions using JavaScript

In the previous post, we discussed how to represent an entire column of a truth table as a single integer and how to perform Boolean operations on entire columns in JavaScript.

Here is the code that we wrote last time:

var     A = parseInt("0000000011111111",2);
var    Ac = parseInt("0000111100001111",2);
var     B = parseInt("0011001100110011",2);
var    Bc = parseInt("0101010101010101",2);
var onlyA = parseInt("0000000011010000",2);    
var onlyB = parseInt("0010001000000010",2);
var  both = parseInt("0000000000100000",2);
var  none = parseInt("1101110100001101",2);

function AND(x,y) { return x & y; };
function OR(x,y)  { return x | y; };
function XOR(x,y) { return x ^ y; };
function NOT(x)   { return ~x & 65535; };
function IFF(x,y) { return NOT( XOR(x,y) ); };

In this post, we will complete this program to solve Puzzle #6. 

Recall that we are looking for a formula:

\(\varphi = (A \leftrightarrow \varphi_A)\ \&\ (B \leftrightarrow \varphi_B)\)

that satisfies the requirements represented by the following truth table:

\(A\)	\(Ac\)	\(B\)	\(Bc\)	\(\varphi = (A \leftrightarrow \varphi_A)\ \&\ (B \leftrightarrow \varphi_B)\)
\(F\)	\(F\)	\(F\)	\(F\)	\(F\)
\(F\)	\(F\)	\(F\)	\(T\)	\(F\)
\(F\)	\(F\)	\(T\)	\(F\)	\(T\)	only B
\(F\)	\(F\)	\(T\)	\(T\)	\(F\)
\(F\)	\(T\)	\(F\)	\(F\)	\(F\)
\(F\)	\(T\)	\(F\)	\(T\)	\(F\)
\(F\)	\(T\)	\(T\)	\(F\)	\(T\)	only B
\(F\)	\(T\)	\(T\)	\(T\)	\(F\)
\(T\)	\(F\)	\(F\)	\(F\)	\(T\)	only A
\(T\)	\(F\)	\(F\)	\(T\)	\(T\)	only A
\(T\)	\(F\)	\(T\)	\(F\)	\(T\)	both A and B
\(T\)	\(F\)	\(T\)	\(T\)	\(T\)	only A
\(T\)	\(T\)	\(F\)	\(F\)	\(F\)
\(T\)	\(T\)	\(F\)	\(T\)	\(F\)
\(T\)	\(T\)	\(T\)	\(F\)	\(T\)	only B
\(T\)	\(T\)	\(T\)	\(T\)	\(F\)

More specifically, we are looking for formulas \(\varphi_A\) and \(\varphi_B\) such that the formula \(\varphi\) is:

• always False in the white rows
  AND
• True in one or more green rows 
  AND
• True in one or more red rows

While we are interested in finding as many solutions as possible, we will limit our search to formulas of a given form.

More precisely, we are going to consider all formulas \(\varphi_A\) and \(\varphi_B\) that are either a conjunction or a disjunction of two literals, where a literal is a single proposition or its negation.

Therefore, we build a list (i.e., an array) of all the literals we will need, as follows:

var literals = [A, Ac, B, Bc, NOT(A), NOT(Ac), NOT(B), NOT(Bc)];

that is, the list of our four propositions and their negation.

Similarly, the list of logical connectives or operators (ops, for short) we are considering using in \(\varphi_A\) and \(\varphi_B\) is defined as follows:

var ops = [AND, OR];

where AND and OR are the JavaScript functions that we defined above.

To summarize, we are going to consider for \(\varphi_A\) all formulas of the form:

pA1 opA pA2

where pA1 and pA2 are two distinct propositions (or their negation) and opA is either AND or OR.

Similarly, we are going to consider for \(\varphi_B\) all formulas of the form:

pB1 opB pB2

where pB1 and pB2 are two distinct propositions (or their negation) and opB is either AND or OR.

Since all combinations are possible, the core of our algorithm is a sequence of nested FOR loops that cover all of the combinations just described, namely:

for(let pA1 of literals)
  for(let pA2 of literals) 
    for(let pB1 of literals) 
      for(let pB2 of literals) 
        if ((pA1 < pA2) && (pB1 < pB2)) 
          for(let opA of ops) 
            for(let opB of ops)
              check(pA1, opA, pA2, pB1, opB, pB2);

Note that I added an IF statement to make sure that we do not waste time considering the same literal twice in a formula, or even the same pair of literals in reverse order, since both OR and AND are commutative operators. Since each literal is an integer that is different from all other literals in our list, making sure that one is less than the other is enough to avoid the duplication just mentioned.

The last line of the code above is a call to a function that checks each combination to determine whether or not it yields a formula \(\varphi\) that is a solution to the puzzle.

This check function is coded as follows:

function check(pA1, opA, pA2, pB1, opB, pB2) {
    var phi = AND( IFF(A,opA(pA1,pA2)), IFF(B,opB(pB1,pB2)) );

    if (!(phi & none) && (phi & onlyA) && (phi & onlyB)) {
       printAndSaveIfNewSolution(phi, pA1, opA, pA2, pB1, opB, pB2); 
    }
};

This function first computes the Boolean value of the formula \(\varphi\), which was defined as:

\((A \leftrightarrow \varphi_A)\ \&\ (B \leftrightarrow \varphi_B)\)

The value of \(\varphi\) is stored in the variable phi.

As a second step, this value, which represents an entire column of the truth table corresponding to the formula \(\varphi\), is checked against each one of the three requirements of a solution.

First, it is a solution if it is False in all white rows, that is, if:

phi & none

is equal to zero (i.e., "falsy" in JavaScript). or equivalently, if:

!(phi & none)

is True (note that the ! operator is the Boolean (NOT the bitwise) negation in JavaScript).

Second, it is a solution if it is True in at least one green row, that is, if:

phi & onlyA

is NOT equal to 0  (i.e., "truthy" in JavaScript).

Third, it is a solution if it is True in at least one red row, that is, if:

phi & onlyB

is NOT equal to 0  (i.e., "truthy" in JavaScript).

Since all three conditions must be true, I used the && operator, which is the Boolean (NOT the bitwise) conjunction in JavaScript.

If all three conditions hold, I call the function printAndSaveIfNewSolution that is defined below:

function printAndSaveIfNewSolution(phi, pA1, opA, pA2, pB1, opB, pB2) {
    if (! solutions.includes(phi)) {   // this is a new solution
      solutions.push(phi);             // store it
      ...                              
      var phiStr = ...                 // convert phi to a string ...
      console.log(...);                // ... and print it
    }
};

This function is not that interesting (its full implementation is given below if you really want to dig deeper). It achieves two tasks if the input combination is a new solution:

1. It stores this solution in the solutions array so that later duplicates will be eliminated (this array is initially empty before our nested loops are executed).
2. It prints a human-readable version of the formula to the console.

Before continuing, did you try to solve this puzzle on your own?

If so, how many solutions (i.e., pairs of statements) did you find?

The answers found by my program will be revealed if you click the button below.

Solution #1 
 A <-> (A | Bc)
 B <-> (-B | -Ac) 

Solution #2 
 A <-> (Ac | Bc)
 B <-> (-B | -Ac) 

Solution #3 
 A <-> (B & Bc)
 B <-> (-Ac | -A) 

Solution #4 
 A <-> (B | -A)
 B <-> (-Bc | -Ac)

Solution #5 
 A <-> (B | -Ac)
 B <-> (-Bc | -A) 

Solution #6 
 A <-> (-B | -Ac)
 B <-> (A | -Bc) 

Solution #7 
 A <-> (-Bc | -A)
 B <-> (A & Ac) 

Solution #8 
 A <-> (-Bc | -A)
 B <-> (Ac | B) 

Solution #9 
 A <-> (-Bc | -B)
 B <-> (A & Ac)

Here is the program in full:

var     A = parseInt("0000000011111111",2);
var    Ac = parseInt("0000111100001111",2);
var     B = parseInt("0011001100110011",2);
var    Bc = parseInt("0101010101010101",2);
var onlyA = parseInt("0000000011010000",2);    
var onlyB = parseInt("0010001000000010",2);
var  both = parseInt("0000000000100000",2);
var  none = parseInt("1101110100001101",2);

function AND(x,y) { return x & y; };
function OR(x,y)  { return x | y; };
function XOR(x,y) { return x ^ y; };
function NOT(x)   { return ~x & 65535; };
function IFF(x,y) { return NOT( XOR(x,y) ); };

var literals = [A, Ac, B, Bc, NOT(A), NOT(Ac), NOT(B), NOT(Bc)];
var ops = [AND, OR];
var solutions = [];  // no solutions found yet

for(let pA1 of literals)
  for(let pA2 of literals) 
    for(let pB1 of literals) 
      for(let pB2 of literals) 
        if ((pA1 < pA2) && (pB1 < pB2)) 
          for(let opA of ops) 
            for(let opB of ops)
              check(pA1, opA, pA2, pB1, opB, pB2);

function check(pA1, opA, pA2, pB1, opB, pB2) {
    var phi = AND( IFF(A,opA(pA1,pA2)), IFF(B,opB(pB1,pB2)) );

    if (!(phi & none) && (phi & onlyA) && (phi & onlyB)) {
        // phi meets the requirements of a solution
        printAndSaveIfNewSolution(phi, pA1, opA, pA2, pB1, opB, pB2); 
    }
};

function getLiteral(n) {
    switch (n) {
    case 255:   return "A";
    case 3855:  return "Ac";
    case 13107: return "B";
    case 21845: return "Bc";
    case 65280: return "-A";
    case 61680: return "-Ac";
    case 52428: return "-B";
    case 43690: return "-Bc";
    }
};

function printAndSaveIfNewSolution(phi, pA1, opA, pA2, pB1, opB, pB2) {
  if (! solutions.includes(phi)) {           // this is a new solution
    solutions.push(phi);                     // store it
    var opAstr = opA === ops[0] ? "&" : "|"; // print it
    var opBstr = opB === ops[0] ? "&" : "|";
    var phiAstr = getLiteral(pA1) + " " + opAstr + " " + getLiteral(pA2);
    var phiBstr = getLiteral(pB1) + " " + opBstr + " " + getLiteral(pB2);
    var phiStr = "A <-> (" + phiAstr + ")\n B <-> (" + phiBstr + ")";
    console.log( "Solution #" + solutions.length,"\n",phiStr,"\n");
  }
};

In the next post, we'll take a close look at the solutions that this program finds.