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 terminals). We also recommend you use the rlwrap tool available under Unix and Linux to 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:

>>> 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 coordinates at which the values on the Sudoku board have to be different:

>>> 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:

>>> 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 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

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...