View source for Sudoku Solved in the ProB REPL

You do not have permission to edit this page, for the following reason:
The action you have requested is limited to users in the group: Users.
You can view and copy the source of this page.
For this example we try and solve a [http://en.wikipedia.org/wiki/Sudoku 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 <tt>-repl</tt> or by starting the [[Eval_Console|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 <tt>let</tt> construct.
Below we have started the REPL using <tt>probcli -repl</tt> and also using the preference <tt>-p REPL_UNICODE TRUE</tt> to display the formula again using Unicode operators (warning: this can slow down certain terminal applications). We also recommend you use the <tt>rlwrap</tt> tool available under Unix and Linux to start probcli, so that you have a command history.
Every character following the <tt>>>></tt> 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.


 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 <tt>DOM</tt> for the numbers to be put inside the Sudoku and the group of indices <tt>SUBSQ</tt> which can be used to construct the 3x3 sub-squares:
<pre>
>>> 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}}
</pre>

Now let us encode in <tt>Diff1</tt> and <tt>Diff2</tt> 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):

<pre>
>>> 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)}
</pre>

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 <tt>DOM --> (DOM --> DOM)</tt>) which has distinct values on each row and column:

<pre>
>>> 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)})}
</pre>

Now, we will try and complete the constraints and put pairs of co-ordinates within each sub-square into the variable <tt>Diff3</tt>, and computing the union of <tt>Diff1</tt>, <tt>Diff2</tt> and <tt>Diff3</tt>:

<pre>
>>> 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)}
</pre>

A full Sudoku solution, with distinct values in each row, column and sub-square, can now be found as follows:
<pre>
>>> 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)})}
</pre>

Let us now try and add some additional constraints for certain pre-established positions on the board, and put those into the variable <tt>P</tt> and require that the solution <tt>Board</tt> contains those values:
<pre>
>>> 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)})}
</pre>


You can visualise the solution using the show command of the REPL:
<pre>
>>> :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] 
</pre>


Let us now check that inconsistencies are detected by our tool:
<pre>
>>> 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
</pre>

Note, you can use the browse command <tt>:b</tt> to show the let definitions, and any other identifier available (in our case none, as we have not loaded any pre-existing B specification):
<pre>
>>> :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...
</pre>

Other useful REPL commands are:
* <tt>:t EXPR</tt> to display the type of an expression,
* <tt>:r</tt> to reload a previously loaded B specification (above we did not load any specification), and
* <tt>:q</tt> to quit the REPL.

Also, many [[http://www.stups.uni-duesseldorf.de/ProB/index.php5/Using_the_Command-Line_Version_of_ProB|commands available for probcli] also work inside the REPL:
* <tt>-p PREF VALUE</tt>,  e.g., <tt>-p MAXINT 999</tt>,
* <tt>-init</tt> to intialise a previously loaded specification
* <tt>-animate Nr</tt> to animate a certain number of steps
* <tt>-mc Nr</tt> to model check the specification, exploring at most Nr states
Return to Sudoku Solved in the ProB REPL.