[Part 10] Raymond Smullyan's Certified Knights and Knaves puzzles Puzzle #6 - A new variant

Now that we have a JavaScript program to solve the following puzzle (see the last four posts):

On another particularly interesting occasion I came across two natives A and B each of whom made a statement such that I could infer that at least one of them must be an uncertified knight, but there was no way to tell which one it was. From neither statement alone could one have deduced this.

What two statements would work? [This problem is not easy!]

we can modify this program to solve a new puzzle, namely:

On another particularly interesting occasion I came across two natives A and B, only one of whom made a statement such that I could infer that at least one of them must be an uncertified knight, but there was no way to tell which one it was. From neither statement alone could one have deduced this.

What statement would work? [This problem is easy if you can program an automatic solver for it.]

So, can you modify our program (listed below) to solve this puzzle?

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 printAndSaveIfNewSolution(phi, pA1, opA, pA2, pB1, opB, pB2) {
  if (! solutions.includes(phi)) {           // this is a new solution
    solutions.push(phi);                     // store it
    /* printing of the solution is omitted (see full code in Part 8) */
  }
};

In my solution, I assumed that the statement was made by A (say) and had the following structure:

\(A \leftrightarrow (\ (l_1\ op_2\ l_2)\  op_1\ (l_3\ op_3\ l_4)\ )\)

in which \(l_1\), \(l_2\), \(l_3\), and \(l_4\) are literals chosen from the same list as above and \(op_1\), \(op_2\), and \(op_3\) are logical operators chosen from the list:

ops = [AND, OR, XOR];

Note that I added XOR as a usable logical connective in this puzzle.

I hope that you'll have fun solving this puzzle!

For reference, here are the only three solutions that my program found:

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

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

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

I think that the second solution is easiest to state concisely in English, namely:

A: "B is an uncertified knight or I am not a certified knight."

This solution is easy to check informally:

• If A is a knight:
• A's statement must be true. Therefore, either B is an uncertified knight or A is (since A is a knight but not a certified one), or both.
• If A is a knave:
• A's statement must be false. Therefore, both disjuncts must be false, including the second one, which implies that A must be a certified knight, which contradicts this case's assumption (i.e., A is a knave).

Therefore, in this solution, A must be a knight, but we do not know whether or not A is certified. However, if A is certified, then B must be an uncertified knight. So both A and B could be uncertified knights.

We can also check this solution formally with a truth table:

\(A\)	\(Ac\)	\(B\)	\(Bc\)	\(B\ \&\ {-Bc}\)	\({-A}\ |\ {-Ac}\)	\((B\ \&\ {-Bc})\ |\ ({-A}\ |\ {-Ac})\)	Sol. #2
\(F\)	\(F\)	\(F\)	\(F\)	\(F\)	\(T\)	\(T\)
\(F\)	\(F\)	\(F\)	\(T\)	\(F\)	\(T\)	\(T\)
\(F\)	\(F\)	\(T\)	\(F\)	\(T\)	\(T\)	\(T\)		only B
\(F\)	\(F\)	\(T\)	\(T\)	\(F\)	\(T\)	\(T\)
\(F\)	\(T\)	\(F\)	\(F\)	\(F\)	\(T\)	\(T\)
\(F\)	\(T\)	\(F\)	\(T\)	\(F\)	\(T\)	\(T\)
\(F\)	\(T\)	\(T\)	\(F\)	\(T\)	\(T\)	\(T\)		only B
\(F\)	\(T\)	\(T\)	\(T\)	\(F\)	\(T\)	\(T\)
\(T\)	\(F\)	\(F\)	\(F\)	\(F\)	\(T\)	\(T\)	✓	only A
\(T\)	\(F\)	\(F\)	\(T\)	\(F\)	\(T\)	\(T\)	✓	only A
\(T\)	\(F\)	\(T\)	\(F\)	\(T\)	\(T\)	\(T\)	✓	both A and B
\(T\)	\(F\)	\(T\)	\(T\)	\(F\)	\(T\)	\(T\)	✓	only A
\(T\)	\(T\)	\(F\)	\(F\)	\(F\)	\(F\)	\(F\)
\(T\)	\(T\)	\(F\)	\(T\)	\(F\)	\(F\)	\(F\)
\(T\)	\(T\)	\(T\)	\(F\)	\(T\)	\(F\)	\(T\)	✓	only B
\(T\)	\(T\)	\(T\)	\(T\)	\(F\)	\(F\)	\(F\)

Can you check the other two solutions for correctness?

Can you translate them into English?