Solving a Puzzle Using Picat

2021-08-14 18:30

Arrange the numbers 1-32, inclusive, in a circle such that the sum of any two adjacent numbers in the circular chain is a perfect square

Picat is a programming language for solving constraint problems, logic problems etc.
It's quite fast too compared to python z3 solver.
So, here's one way to solve the circle problem in picat

main => go.

go =>

   % decision variables
   N = 32,
   Xs = new_list(N),

   % given constraints
   Xs :: 1..N,
   Sq = [I**2 : I in 2..7],

   % fix one number, to avoid rotation
   Xs[1] #= 1,
   foreach (I in 1..N-1),
       sum([(Xs[I+1]+Xs[I]) #= Sq[J] : J in 1..Sq.length]) #= 1,
   end,
   sum([(Xs[N]+Xs[1]) #= Sq[J] : J in 1..Sq.length]) #= 1,
   all_different(Xs),

   % solve and print
   Res = solve_all(Xs),

   foreach (R in Res),
      println(R),
   end,
   nl.

References:

Solving Mastermind-like Problems Using Z3 Theorem Prover

2020-04-27 23:22

7 2 9 1 - One number is correct but not in right position
4 6 8 7 - One number is correct but not in right position
1 8 7 2 - Two numbers are correct but only one is in right position
5 7 3 9 - Two numbers are correct and both in right position

Assuming all the digits are distinct, what is the 5-digit number?

(Asked on puzzling stackexchange)

This can be quite easily solved using Z3 theorem prover, once we figure out to set up the constraints.

We have 5 variables, \(\{x_i\}, i=0, 1, 2, 3, 4\) which are constrained by

\begin{align*} \displaystyle 0 \le x_i &\le 9 \\ x_i \neq x_j \land i &\neq j\\ [x_0 \neq 4] + [x_1 \neq 7] + [x_2 \neq 2] + [x_3 \neq 9] + [x_4 \neq 1] &= 5\\ [x_0 \neq 9] + [x_1 \neq 4] + [x_2 \neq 6] + [x_3 \neq 8] + [x_4 \neq 7] &= 5\\ [x_0 \neq 3] + [x_1 \neq 1] + [x_2 \neq 8] + [x_3 \neq 7] + [x_4 \neq 2] &= 4\\ [x_0 \neq 1] + [x_1 \neq 5] + [x_2 \neq 7] + [x_3 \neq 3] + [x_4 \neq 9] &= 3\\ \end{align*}

where \([\cdot]\) is the Iverson Bracket notation (1 if the condition holds, 0 otherwise).

When checking the models for which the conditions are satisfied, we will also check that the number of digits satisfying the conditions holds good, using set intersection.

We solve it using python bindings to Z3, which can be installed in python virtual environment by

1	pip install z3-solver

Then, we can solve the above by running the following python code:

from z3 import *

def main():
    sol = Solver()
    cols = 5

    a = [[4,7,2,9,1],
         [9,4,6,8,7],
         [3,1,8,7,2],
         [1,5,7,3,9]]

    # variables
    x = [Int("x[%d]" % j) for j in range(cols)]

    # constraints
    '''
    All are distinct
    '''
    sol.add(Distinct(x))

    '''
    All numbers 0 <= x_i <= 9
    '''
    for i in range(cols):
        sol.add(x[i] >= 0, x[i] <= 9)

    sol.add(Sum([If(x[c] != a[0][c],1,0) for c in range(cols)]) == 5) # no number in correct position
    sol.add(Sum([If(x[c] != a[1][c],1,0) for c in range(cols)]) == 5) # no number in correct position
    sol.add(Sum([If(x[c] != a[2][c],1,0) for c in range(cols)]) == 4) # one number in correct position
    sol.add(Sum([If(x[c] != a[3][c],1,0) for c in range(cols)]) == 3) # two numbers in correct position

    cnt = 0

    while sol.check() == sat:
        mod = sol.model()
        xval = [mod.eval(x[j]).as_long() for j in range(cols)]
        if len(set(xval) & set(a[0])) == 1 and\
           len(set(xval) & set(a[1])) == 1 and\
           len(set(xval) & set(a[2])) == 2 and\
           len(set(xval) & set(a[3])) == 2:
            cnt += 1
            print(xval)
        sol.add(Or([x[i] != mod.eval(x[i]).as_long() for i in range(cols)])) # add constraint to check for different solution

    print("#solutions: ", cnt)

if __name__ == "__main__":
    main()
'''
[6, 5, 0, 3, 2]
#solutions:  1
'''

If we remove the distinct constraint, we get 19 different solutions.

We find that Z3 and other SMT solvers are powerful tools for verification computer programs / hardware designs, perform compiler optimizations, finding bugs etc. And solving Logic puzzles!

References:

A puzzle from New Scientist

2020-04-10 22:25

It is Tom's 7th birthday and he has a cake with seven candles on it, arranged in a circle -- but they are trick candles. If you blow on a lit candle, it will go out, but if you blow on an unlit candle, it will relight itself.

Since Tom is only 7, his aim isn't brilliant. Any time he blows on a particular candle, the two either side also get blown on as well. How can Tom blow out all the candles? What is the fewest number of puffs he can do it in?

This is a nice candidate for the shortest path problem, which can be easily solved in Sagemath as follows:

mat = [[0]*128 for i in range(128)]

'''
Build an adjacency matrix, where three consecutive bits of the adjacent nodes are toggled
'''
for i in range(128):
    mat[i][i^^0b111] = 1
    mat[i][i^^0b1110] = 1
    mat[i][i^^0b11100] = 1
    mat[i][i^^0b111000] = 1
    mat[i][i^^0b1110000] = 1
    mat[i][i^^0b1100001] = 1
    mat[i][i^^0b1000011] = 1

'''
Find the shortest path, from all-lit candles to none
Display the seven candles in binary
'''
mx = Matrix(mat)
g = DiGraph(mx)
[bin(i)[2:].zfill(7) for i in g.shortest_path(u=127, v=0)]
'''
['1111111', '1110001', '0010000', '1100000', '0100011', '0011011', '0000111', '0000000']
'''

Interactive Disassembly

2018-10-28 21:06

Godbolt enables us to interactively see the assembly output of the input source code by the selected compiler.

But it depends on nodejs and there's quite a delay between the modified input and the produced disassembly.

Enter RMSBolt, which is a package for emacs. It's much lighter, more powerful, and more interactive when compared to Godbolt, and perhaps the only alternative to Godbolt. Great way to learn assembly language, and fun too!