[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.

[Part 8] Raymond Smullyan's Knights, Knaves, and Normals puzzles Fourth puzzle, on the island of Bahava

For our fourth puzzle, we will use the \(46^{th}\) (and last) puzzle in Chapter 3 of Raymond Smullyan's 1978 book entitled "What Is the Name of This Book?: The Riddle of Dracula and Other Logical Puzzles". This puzzle takes place again on the island of Bahava, on which marriage is highly regulated. As stated on pages 25-26 of the 2011, paperback Dover Recreational Math edition [ISBN: 9780486481982], the puzzle reads:

[...] Thus, given any married couple, either they are both normal, or one of them is a knight and the other a knave. [...]

This problem concerns two married couples on the island of Bahava, Mr. and Mrs. A, and Mr. and Mrs. B. They are being interviewed, and three of the four people give the following testimony:

Mr. A: Mr B. is a knight.

Mrs. A: My husband is right; Mr. B is a knight.  

Mrs. B: That's right. My husband is indeed a knight.  

What are each of the four people, and which of the three statements are true?

As always in this series, the following axioms represent the possible types for all inhabitants:

Kni(x) | Kna(x) | Nor(x).

-Kni(x) | -Kna(x).

-Kni(x) | -Nor(x).

-Kna(x) | -Nor(x).

Like in the previous post, we represent the fact that two inhabitants A and B are married with the formula:

Mar(A,B).

 Since the "married" relationship is symmetrical, we add the following axiom:

Mar(x,y) -> Mar(y,x).

Then we represent the marriage restrictions based on types with the axiom:

Mar(x,y) -> ((Nor(x) & Nor(y)) | (Kni(x) & Kna(y))).

Finally, we encode the fact that polygamy is not allowed with the axiom:

(Mar(x,y) & Mar(x,z)) -> y = z.

This concludes our representation of the island of Bahava's general conditions.

Turning to our specific puzzle, we represent the fact that we have two couples made of four distinct islanders, and that there are no other islanders in this puzzle, as follows:

Mar(MrA,MrsA).

Mar(MrB,MrsB).

MrA != MrsA & MrA != MrB & ...  [formula continued on the next line]

... MrA != MrsB & MrsA != MrB & MrsA != MrsB | MrB != MrsB.

x = MrA | x = MrsA | x = MrB | x = MrsB.

Finally, we represent the three statements using our usual representation principle for the knights/knaves/normals puzzle, yielding the three formulas:

(Kni(MrA) & Kni(MrB)) | (Kna(MrA) & -Kni(MrB)) | Nor(MrA). 

(Kni(MrsA) & Kni(MrB)) | (Kna(MrsA) & -Kni(MrB)) | Nor(MrsA). 

(Kni(MrsB) & Kni(MrB)) | (Kna(MrsB) & -Kni(MrB)) | Nor(MrsB).

The entire input given to Mace4 is thus:

and its output is:

The only model in this output demonstrates that there is only one solution to this puzzle: all four islanders are normals; therefore all three statements are false.