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.
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 add the co-ordinates within each sub-square:
>>> 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 can now be found:
>>> 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 positions on the board:
>>> 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)})}
Let us now check that inconsistencies are detected:
>>> 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
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]
The browse command can be used to show our definitions:
>>> :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...