Self-study plan for quant researcher — Puzzle (Day 2)
Continuing my jouney to becoming a quantitative researcher. This week, we will explore the solution for the Hooks puzzle together.
Again, for readers who are encountering this series for the first time, my purpose is to solve each and every Jane Street’s Puzzles. My code will be published on my GitHub.
✨Please give me a 👏 if you are interested in my sharing, leave a comment 💬 to share your views/thoughts. ✨
Hooks
The puzzle was publised at this link.
In the grid below, enter nine 9’s in the outermost hook, eight 8’s in the next hook, then seen 7’s, six 6’s, and so on, down to the one 1 (already entered), so that the row and column match values given along the border.
Once you’ve completed the puzzle, submit as your answer the sum of the values of the shaded squares (along with any other comments you’d like to provide).
Break down the problem
This is a grid-based puzzle where you have a NxN grid. What we need to do is to fill cells with a number in the outermost hook from 1 to 9, corresponding to the respective colors:
And the number one (1) was already entered in the upper left corner, corresponding to the blue color. Other numbers are filled so that the sums of the rows and columns match the given border values. This implies that it is not neccessary to fill all cells.
In the submission, we need to:
- Complete the puzzle
- Submit the sum of the values of the shaded squares.
Before solving the problem, for those who have not heard about the z3 API in Python, they can refer to the previous part at this link and the Tactic in z3. Otherwise, you can skip that part and move directly to the solution.
Tactic in z3
In the Z3 theorem prover, Optimizer and Tactic are both components used for solving and optimizing mathematical problems. However, they have different purposes and functionality.
1. Tactic:
- A tactic in Z3 is a high-level strategy or a set of rules that guide the search for a solution to a problem. It defines how the solver should approach solving a given problem.
- A tactic is composed of a sequence of solver procedures, each of which tries to solve the problem in a particular way (e.g., using simplification, rewriting, or specific solver engines).
- Tactic can be applied to a goal to attempt to solve or simplify it.
2. Optimizer:
- An optimizer in Z3 is used for optimizing mathematical expressions or finding optimal solutions to optimization problems (e.g., minimizing or maximizing a function subject to constraints).
- The optimizer is used for numerical optimization, where the goal is to find the optimal values of variables that satisfy certain conditions to either maximize or minimize an objective function.
- The Optimizer in Z3 allows you to specify optimization objectives and constraints, and it can search for optimal solutions using various optimization strategies.
In summary, a Tactic is more general and focused on guiding the solving process and simplifying goals, while an Optimizer is specifically designed for numerical optimization problems, attempting to find optimal solutions for given optimization objectives and constraints. Tactics can be used as part of an optimization process to guide how the optimization is performed, but they serve different purposes in the context of Z3.
QF_FD Logic
A specialized logic QF_FD which stands for quantifier-free formulas over finite domains, and its associated incremental solver (that supports push/pop). The QF_FD domain comprises of bit-vectors, enumeration data-types used only in equalities, and bounded integers: Integers used in QF_FD problems have to be constrained by a finite bound.
Here’s a simple example of using z3 with a tactic to solve a quantifier-free formula in the QF_FD logic:
In this instance, we’re trying to address a simple equation,
with constraints,
The solver will guide the search for a solution according to the rules.
# Create Z3 solver
# Use a tactic for solving QF_FD formulas
solver = Tactic('qffd').solver()
# Define variables
x = Int('x')
y = Int('y')
# Create a quantifier-free formula over finite domains (QF_FD)
formula = And(x > 0, y > 0, x < 10, y < 10, x + y == 15)
# Add the formula to the solver
solver.add(formula)
if solver.check() == sat:
print("Satisfiable")
print("Model:")
model = solver.model()
print("x =", model[x])
print("y =", model[y])
elif solver.check() == unsat:
print("Unsatisfiable")
else:
print("Unknown")The output is
Solution
Import necessary modules and packages
import numpy as np
import time
import seaborn as sns
import matplotlib.pyplot as plt
from IPython.display import Markdown
from z3 import *Create a 9 x 9 matrix according to the requirement
grid = np.zeros((9,9)) # all values are 0
for (i,j),e in np.ndenumerate(grid): #increasing the outermost values up 1 unit.
grid[i,j] = max(i,j)+1The values of grid are
Add the numbers outside the grid
# The numbers outside the rows.
row_labels = [31, 19, 45, 16, 5, 47, 28, 49, 45]
# The numbers outside the columns.
col_labels = [26, 42, 11, 22, 42, 36, 29, 32, 45]Create a z3 solver
Since this challenge requires us to follow the brainteaser’s rules to find the result. Thus, I decide to use a tactic for solving QF_FD formulas.
# Create Z3 solver
# Use a tactic for solving QF_FD formulas
solver = Tactic('qffd').solver()Setup up a 9x9 matrix of integer variables
# Setup up a 9x9 matrix of integer variables
X = np.array(IntVector("x",9*9),dtype=object).reshape((9,9))Set up the constraints for the solver
First of all, as mentioned, we can leave the cell blank or fill a number corresponding to the cell’s color. Thus, the logic is “0” for leaving a blank and “1” for putting a number.
s += [Or(x==0,x==1) for _,x in np.ndenumerate(X)] # Because we can leave the cell blank (0) or put a number (1)Secondly, we will enter the number based on the colors respectively for the matrix. Then, summing values in the columns and rows to get values equal to the corresponding given border values.
# Columns
for i in range(9):
s += Sum([X[i][j] * int(grid[i][j]) for j in range(9)]) == col_labels[i]
# Rows
for j in range(9):
s += Sum([X[i][j] * int(grid[i][j]) for i in range(9)]) == row_labels[j]Actually, for those two conditions, it seems to be enough for solving the problem. Now, we can run the solver and get the solution.
Processing — Stage 1
# Solve and print
start = time.time()
if s.check() == sat:
m = s.model()
evalu = np.vectorize(lambda x:m.evaluate(x).as_long())
r = evalu(X)
else:
print("Failed")
display(Markdown("**Solved in {:.4f} seconds. Answer is : {:.0f}**".format(time.time()-start,
sum([e for (i,j),e in np.ndenumerate(r*grid) if (i+j) % 2 ==0])
)))
fig,ax = plt.subplots(1,1,figsize=(3,3))
pretty = np.vectorize(lambda x:str(int(x)).replace('0',''))
ax = sns.heatmap(grid,annot=pretty(r*grid),fmt='',cbar=False,cmap="tab20",linecolor='k',linewidth=2,
xticklabels=row_labels, yticklabels=col_labels, annot_kws={"fontsize":10,"color":"k"},alpha=0.8)
ax.tick_params(left=False, bottom=False,labelleft=False, labelright=True)
plt.xticks(rotation=0,fontsize =10)
plt.yticks(rotation=0,fontsize =10)
plt.tight_layout()
plt.show()After running many times or you can try to run with a large number, there were three solutions obtained,
Oops! Now, we suddenly realise that something is missing here. Yes, the 1 is already entered in the blue cell at the top left corner of the grid. Thus, only the result containing the number one at that position was correct.
However, can we add that condition in our code? Of course, we can. But first, we all can read about another function in z3. It is called PbEq.
PbEq in z3
PbEq in Z3 stands for “pseudo-Boolean equality constraint,” which is a type of constraint used in pseudo-Boolean optimization. Pseudo-Boolean optimization is a generalization of Boolean optimization where variables are allowed to take values from a larger domain (usually integers) rather than just true or false.
In z3, PbEq is a function that creates a pseudo-Boolean equality constraint. The pseudo-Boolean equality constraint is typically expressed as a weighted sum of Boolean variables (often called pseudo-Boolean variables) being equal to a given integer constant. It has the general form:
Here’s a simple example of using PbEq in z3:
In this example, we create a pseudo-Boolean equality constraint,
# Define the Boolean variables
x1 = Bool('x1')
x2 = Bool('x2')
x3 = Bool('x3')
# Define the weights for the Boolean variables
a1 = 2
a2 = -1
a3 = 3
# Define the target integer constant
k = 1
# Create the pseudo-Boolean equality constraint: a1 * x1 + a2 * x2 + a3 * x3 = k
pb_eq_constraint = PbEq([(x1, a1), (x2, a2), (x3, a3)], k)
# Print the pseudo-Boolean equality constraint
print("Pseudo-Boolean equality constraint:", pb_eq_constraint)The output is,
Now, back to the solution. We want to add the number one 1 into the first cell (at column 1, row 1). We need to add this condition to the solver,
# Combine both column and row sums conditions and add 1 to first cell.
s += [PbEq([(e*int(grid[i,j])==n,1) for (i,j),e in np.ndenumerate(X)],n) for n in range(1,10)] Now, running it …
Processing — Stage 2
# Solve and print
start = time.time()
if s.check() == sat:
m = s.model()
evalu = np.vectorize(lambda x:m.evaluate(x).as_long())
r = evalu(X)
else:
print("Failed")
display(Markdown("**Solved in {:.4f} seconds. Answer is : {:.0f}**".format(time.time()-start,
sum([e for (i,j),e in np.ndenumerate(r*grid) if (i+j) % 2 ==0])
)))
fig,ax = plt.subplots(1,1,figsize=(3,3))
pretty = np.vectorize(lambda x:str(int(x)).replace('0',''))
ax = sns.heatmap(grid,annot=pretty(r*grid),fmt='',cbar=False,cmap="tab20",linecolor='k',linewidth=2,
xticklabels=row_labels, yticklabels=col_labels, annot_kws={"fontsize":10,"color":"k"},alpha=0.8)
ax.tick_params(left=False, bottom=False,labelleft=False, labelright=True)
plt.xticks(rotation=0,fontsize =10)
plt.yticks(rotation=0,fontsize =10)
plt.tight_layout()
fig.savefig('result_1.png')
plt.show()Result
Public solution
The best solution was published here.
Hope that this challenge today brings more fun for all of you. Next time, we will continue with another puzzle called “Tile and Trouble.” Spending a Saturday night with a glass of whiskey in your study and try to slove this problem before reading my detailed solution and explanation.
Note: Unless otherwise noted, all images are by the author
Source code
https://github.com/Tayerquach/quant_puzzles
References
https://www.janestreet.com/puzzles/
