Sudoku Solved in the ProB REPL: Difference between revisions

For this example we try and solve a Sudoku using the REPL (Read-Eval-Print-Loop) of ProB only, without constructing any B machine. The REPL can either be started using probcli's command -repl or by starting the Eval Console in ProB Tcl/Tk.

We will use the new feature of the REPL (available in ProB 1.4) to introduce local variables with the let construct. Below we have started the REPL using probcli -repl and also using the preference -p REPL_UNICODE TRUE to display the formula again using Unicode operators (warning: this can slow down certain terminal applications). We also recommend you use the rlwrap tool available under Unix and Linux to start probcli, so that you have a command history. Every character following the >>> until the end of the line is typed by the user. The next line, starting with ⇝, shows the Unicode rendering of the ASCII expression or predicate typed by the user. The lines below then show the output computed by ProB; the responses are immediate (80 ms or less for all queries below on a Mac Book Air).

probcli -repl -p REPL_UNICODE TRUE
ProB Interactive Expression and Predicate Evaluator 
Type ":help" for more information.

First let us define two useful values: the domain DOM for the numbers to be put inside the Sudoku and the group of indices SUBSQ which can be used to construct the 3x3 sub-squares:

>>> let DOM = 1..9
 ⇝  1 ‥ 9
Expression Value = 
{1,2,3,4,5,6,7,8,9}
>>> let SUBSQ = { {1,2,3}, {4,5,6}, {7,8,9} } 
 ⇝  {{1,2,3},{4,5,6},{7,8,9}}
Expression Value = 
{{1,2,3},{4,5,6},{7,8,9}}

Now let us encode in Diff1 and Diff2 sets of pairs of coordinates at which the values on the Sudoku board have to be different (because they lie on the same column or row respectively):

>>> let Diff1 = {x1,x2,y1,y2| y1:DOM & y2:DOM & x1:DOM & x2:DOM & x1<x2 & y1=y2}
 ⇝  {x1,x2,y1,y2|((((y1 ∈ DOM ∧ y2 ∈ DOM) ∧ x1 ∈ DOM) ∧ x2 ∈ DOM) ∧ x1 < x2) ∧ y1 = y2}
Expression Value = 
#324:{(((1|->2)|->1)|->1),(((1|->2)|->2)|->2),...,(((8|->9)|->8)|->8),(((8|->9)|->9)|->9)}
>>> let Diff2 = {x1,x2,y1,y2| y1:DOM & y2:DOM & x1:DOM & x2:DOM & x1=x2 & y1<y2}
 ⇝  {x1,x2,y1,y2|((((y1 ∈ DOM ∧ y2 ∈ DOM) ∧ x1 ∈ DOM) ∧ x2 ∈ DOM) ∧ x1 = x2) ∧ y1 < y2}
Expression Value = 
#324:{(((1|->1)|->1)|->2),(((1|->1)|->1)|->3),...,(((9|->9)|->7)|->9),(((9|->9)|->8)|->9)}

We have not yet encoded that in each sub-square the values must also all be distinct. Nonetheless, let us try and solve the puzzle as it stands, by looking for a full board (of type DOM --> (DOM --> DOM)) which has distinct values on each row and column:

>>> Board : DOM --> (DOM --> DOM) & !(x1,x2,y1,y2).((x1,x2,y1,y2):Diff1\/Diff2 => Board(x1)(y1) /= Board(x2)(y2))
 ⇝  ∃(Board).(Board ∈ DOM → (DOM → DOM) ∧ ∀(x1,x2,y1,y2).((((x1 ∈ ℤ ∧ x2 ∈ ℤ) ∧ y1 ∈ ℤ) ∧ y2 ∈ ℤ) ∧ ((x1 ↦ x2) ↦ y1) ↦ y2 ∈ Diff1 ∪ Diff2 ⇒ Board(x1)(y1) ≠ Board(x2)(y2)))
Existentially Quantified Predicate over Board is TRUE
Solution: 
       Board = {(1|->{(1|->1),(2|->2),(3|->3),(4|->4),(5|->5),(6|->6),(7|->7),(8|->8),(9|->9)}),(2|->{(1|->2),(2|->1),(3|->4),(4|->3),(5|->6),(6|->5),(7|->8),(8|->9),(9|->7)}),(3|->{(1|->3),(2|->4),(3|->1),(4|->2),(5|->7),(6|->8),(7|->9),(8|->5),(9|->6)}),(4|->{(1|->4),(2|->3),(3|->2),(4|->1),(5|->8),(6|->9),(7|->6),(8|->7),(9|->5)}),(5|->{(1|->5),(2|->6),(3|->7),(4|->8),(5|->9),(6|->1),(7|->2),(8|->3),(9|->4)}),(6|->{(1|->6),(2|->5),(3|->8),(4|->9),(5|->1),(6|->7),(7|->3),(8|->4),(9|->2)}),(7|->{(1|->7),(2|->8),(3|->9),(4|->5),(5|->2),(6|->3),(7|->4),(8|->6),(9|->1)}),(8|->{(1|->8),(2|->9),(3|->6),(4|->7),(5|->4),(6|->2),(7|->5),(8|->1),(9|->3)}),(9|->{(1|->9),(2|->7),(3|->5),(4|->6),(5|->3),(6|->4),(7|->1),(8|->2),(9|->8)})}

Now, we will try and complete the constraints and put pairs of coordinates within each sub-square into the variable Diff3, and computing the union of Diff1, Diff2 and Diff3:

>>> let Diff3 = {x1,x2,y1,y2|#(s1,s2).(s1:SUBSQ & s2:SUBSQ & x1:s1 & x2:s1 & x1>=x2 & (x1=x2 => y1>y2) & y1:s2 & y2:s2 & (x1,y1) /= (x2,y2))}
 ⇝  {x1,x2,y1,y2|(((x1 ∈ ℤ ∧ x2 ∈ ℤ) ∧ y1 ∈ ℤ) ∧ y2 ∈ ℤ) ∧ (((x1 ≥ x2 ∧ (x1 = x2 ⇒ y1 > y2)) ∧ (x1 ↦ y1) ≠ (x2 ↦ y2)) ∧ ∃(s1,s2).(((((s1 ∈ SUBSQ ∧ s2 ∈ SUBSQ) ∧ x1 ∈ s1) ∧ x2 ∈ s1) ∧ y1 ∈ s2) ∧ y2 ∈ s2))}
Expression Value = 
#324:{(((1|->1)|->2)|->1),(((1|->1)|->3)|->1),...,(((9|->9)|->9)|->7),(((9|->9)|->9)|->8)}
>>> let Diff = Diff1 \/ Diff2 \/ Diff3
 ⇝  (Diff1 ∪ Diff2) ∪ Diff3
Expression Value = 
#972:{(((1|->1)|->1)|->2),(((1|->1)|->1)|->3),...,(((9|->9)|->9)|->7),(((9|->9)|->9)|->8)}

A full Sudoku solution, with distinct values in each row, column and sub-square, can now be found as follows:

>>> Board : DOM --> (DOM --> DOM) & !(x1,x2,y1,y2).((x1,x2,y1,y2):Diff => Board(x1)(y1) /= Board(x2)(y2))
 ⇝  ∃(Board).(Board ∈ DOM → (DOM → DOM) ∧ ∀(x1,x2,y1,y2).((((x1 ∈ ℤ ∧ x2 ∈ ℤ) ∧ y1 ∈ ℤ) ∧ y2 ∈ ℤ) ∧ ((x1 ↦ x2) ↦ y1) ↦ y2 ∈ Diff ⇒ Board(x1)(y1) ≠ Board(x2)(y2)))
Existentially Quantified Predicate over Board is TRUE
Solution: 
       Board = {(1|->{(1|->1),(2|->2),(3|->3),(4|->4),(5|->5),(6|->6),(7|->7),(8|->8),(9|->9)}),(2|->{(1|->4),(2|->5),(3|->6),(4|->7),(5|->8),(6|->9),(7|->1),(8|->2),(9|->3)}),(3|->{(1|->7),(2|->8),(3|->9),(4|->1),(5|->2),(6|->3),(7|->4),(8|->5),(9|->6)}),(4|->{(1|->2),(2|->1),(3|->4),(4|->3),(5|->6),(6|->5),(7|->8),(8|->9),(9|->7)}),(5|->{(1|->3),(2|->6),(3|->5),(4|->8),(5|->9),(6|->7),(7|->2),(8|->1),(9|->4)}),(6|->{(1|->8),(2|->9),(3|->7),(4|->2),(5|->1),(6|->4),(7|->3),(8|->6),(9|->5)}),(7|->{(1|->5),(2|->3),(3|->1),(4|->6),(5|->4),(6|->2),(7|->9),(8|->7),(9|->8)}),(8|->{(1|->6),(2|->4),(3|->2),(4|->9),(5|->7),(6|->8),(7|->5),(8|->3),(9|->1)}),(9|->{(1|->9),(2|->7),(3|->8),(4|->5),(5|->3),(6|->1),(7|->6),(8|->4),(9|->2)})}

Let us now try and add some additional constraints for certain pre-established positions on the board, and put those into the variable P and require that the solution Board contains those values:

>>> let P = {(1,1,7), (1,2,8), (1,3,1), (2,1,9)}
 ⇝  {((1↦1)↦7),((1↦2)↦8),((1↦3)↦1),((2↦1)↦9)}
Expression Value = 
{((1|->1)|->7),((1|->2)|->8),((1|->3)|->1),((2|->1)|->9)}
>>> Board : DOM --> (DOM --> DOM) & !(x1,x2,y1,y2).((x1,x2,y1,y2):Diff => Board(x1)(y1) /= Board(x2)(y2)) & !(x,y,z).((x,y,z):P => Board(x)(y)=z)
 ⇝  ∃(Board).((Board ∈ DOM → (DOM → DOM) ∧ ∀(x1,x2,y1,y2).((((x1 ∈ ℤ ∧ x2 ∈ ℤ) ∧ y1 ∈ ℤ) ∧ y2 ∈ ℤ) ∧ ((x1 ↦ x2) ↦ y1) ↦ y2 ∈ Diff ⇒ Board(x1)(y1) ≠ Board(x2)(y2))) ∧ ∀(x,y,z).(((x ∈ ℤ ∧ y ∈ ℤ) ∧ z ∈ ℤ) ∧ (x ↦ y) ↦ z ∈ P ⇒ Board(x)(y) = z))
Existentially Quantified Predicate over Board is TRUE
Solution: 
       Board = {(1|->{(1|->7),(2|->8),(3|->1),(4|->2),(5|->3),(6|->4),(7|->5),(8|->6),(9|->9)}),(2|->{(1|->9),(2|->2),(3|->3),(4|->1),(5|->5),(6|->6),(7|->4),(8|->7),(9|->8)}),(3|->{(1|->4),(2|->5),(3|->6),(4|->7),(5|->8),(6|->9),(7|->1),(8|->2),(9|->3)}),(4|->{(1|->1),(2|->3),(3|->2),(4|->4),(5|->6),(6|->5),(7|->8),(8|->9),(9|->7)}),(5|->{(1|->5),(2|->4),(3|->7),(4|->8),(5|->9),(6|->2),(7|->3),(8|->1),(9|->6)}),(6|->{(1|->6),(2|->9),(3|->8),(4|->3),(5|->1),(6|->7),(7|->2),(8|->4),(9|->5)}),(7|->{(1|->2),(2|->1),(3|->5),(4|->6),(5|->7),(6|->3),(7|->9),(8|->8),(9|->4)}),(8|->{(1|->3),(2|->6),(3|->4),(4|->9),(5|->2),(6|->8),(7|->7),(8|->5),(9|->1)}),(9|->{(1|->8),(2|->7),(3|->9),(4|->5),(5|->4),(6|->1),(7|->6),(8|->3),(9|->2)})}

You can visualise the solution using the show command of the REPL:

>>> :show
Nr        prj1      prj2      
1         1         [7,8,1,2,3,4,5,6,9] 
2         2         [9,2,3,1,5,6,4,7,8] 
3         3         [4,5,6,7,8,9,1,2,3] 
4         4         [1,3,2,4,6,5,8,9,7] 
5         5         [5,4,7,8,9,2,3,1,6] 
6         6         [6,9,8,3,1,7,2,4,5] 
7         7         [2,1,5,6,7,3,9,8,4] 
8         8         [3,6,4,9,2,8,7,5,1] 
9         9         [8,7,9,5,4,1,6,3,2] 

Let us now check that inconsistencies are detected by our tool:

>>> let P = {(1,1,7), (1,2,8), (1,3,1), (2,1,9), (2,2,9)}
 ⇝  {((1↦1)↦7),((1↦2)↦8),((1↦3)↦1),((2↦1)↦9),((2↦2)↦9)}
Expression Value = 
{((1|->1)|->7),((1|->2)|->8),((1|->3)|->1),((2|->1)|->9),((2|->2)|->9)}
>>> Board : DOM --> (DOM --> DOM) & !(x1,x2,y1,y2).((x1,x2,y1,y2):Diff => Board(x1)(y1) /= Board(x2)(y2)) & !(x,y,z).((x,y,z):P => Board(x)(y)=z)
 ⇝  ∃(Board).((Board ∈ DOM → (DOM → DOM) ∧ ∀(x1,x2,y1,y2).((((x1 ∈ ℤ ∧ x2 ∈ ℤ) ∧ y1 ∈ ℤ) ∧ y2 ∈ ℤ) ∧ ((x1 ↦ x2) ↦ y1) ↦ y2 ∈ Diff ⇒ Board(x1)(y1) ≠ Board(x2)(y2))) ∧ ∀(x,y,z).(((x ∈ ℤ ∧ y ∈ ℤ) ∧ z ∈ ℤ) ∧ (x ↦ y) ↦ z ∈ P ⇒ Board(x)(y) = z))
Existentially Quantified Predicate over Board is FALSE

Note, you can use the browse command :b to show the let definitions, and any other identifier available (in our case none, as we have not loaded any pre-existing B specification):

>>> :b
Available SETS: 
Available CONSTANTS: []
Available VARIABLES: []
Available let definitions:
  DOM = {1,2,3,4,5,6,7,8,9}
  SUBSQ = {{1,2,3},{4,5,6},{7,8,9}}
  Diff1 = #324:{(((1|->2)|->1)|->1),(((1|->2)|->2)|->2),...,...
  Diff2 = #324:{(((1|->1)|->1)|->2),(((1|->1)|->1)|->3),...,...
  Diff3 = #324:{(((1|->1)|->2)|->1),(((1|->1)|->3)|->1),...,...
  Diff = #972:{(((1|->1)|->1)|->2),(((1|->1)|->1)|->3),...,...
  P = {((1|->1)|->7),((1|->2)|->8),((1|->3)|->1),((2|->1...

Other useful REPL commands are:

• :t EXPR to display the type of an expression,
• :r to reload a previously loaded B specification (above we did not load any specification), and
• :q to quit the REPL.

Also, many commands available for probcli also work inside the REPL:

• -p PREF VALUE to set preference values, e.g., -p MAX_DISPLAY_SET 999 if you want the pretty printer to display sets up until size 999 in full (above the sets Diff1,... were truncated as the default value is 100,
• -init to intialise a previously loaded specification,
• -animate Nr to animate a certain number of steps,
• -mc Nr to model check the specification, exploring at most Nr states.