Skip to content
Snippets Groups Projects
Commit 34f6927d authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add ProB constraint solver introduction

parent de42ec91
Branches
Tags
No related merge requests found
%% Cell type:markdown id: tags:
We can use ProB to perform computations:
%% Cell type:code id: tags:
``` prob
2**10
```
%% Output
1024
%% Cell type:markdown id: tags:
ProB supports *mathematical* integers without restriction (apart from memmory consumption):
%% Cell type:code id: tags:
``` prob
2**100
```
%% Output
1267650600228229401496703205376
%% Cell type:markdown id: tags:
We can find solutions for equations. Open variables are implicitly existentially quantified:
%% Cell type:code id: tags:
``` prob
x*x=100
```
%% Output
TRUE (x = −10)
%% Cell type:markdown id: tags:
We can find all solutions to a predicate by using the set comprehension notation.
%% Cell type:code id: tags:
``` prob
{x|x*x=100}
```
%% Output
{−10,10}
%% Cell type:markdown id: tags:
We now try and solve the SEND+MORE=MONEY arithmetic puzzle in B, involving 8 distinct digits:
%% Cell type:code id: tags:
``` prob
{S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 &
card({S,E,N,D, M,O,R, Y}) = 8 &
S*1000 + E*100 + N*10 + D +
M*1000 + O*100 + R*10 + E =
M*10000 + O*1000 + N*100 + E*10 + Y
```
%% Output
TRUE (R = 8 ∧ S = 9 ∧ D = 7 ∧ E = 5 ∧ Y = 2 ∧ M = 1 ∧ N = 6 ∧ O = 0)
%% Cell type:markdown id: tags:
Observe how we have used the cardinality constraint to express that all digits are distinct.
If we leave out this cardinality constraint, other solutions are possible:
%% Cell type:code id: tags:
``` prob
{S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 &
// card({S,E,N,D, M,O,R, Y}) = 8 & // commented out
S*1000 + E*100 + N*10 + D +
M*1000 + O*100 + R*10 + E =
M*10000 + O*1000 + N*100 + E*10 + Y
```
%% Output
TRUE (R = 0 ∧ S = 9 ∧ D = 0 ∧ E = 0 ∧ Y = 0 ∧ M = 1 ∧ N = 0 ∧ O = 0)
%% Cell type:markdown id: tags:
We can find all solutions (to the unmodified puzzle) using a set comprehension and make sure that there is just a single soltuion:
%% Cell type:code id: tags:
``` prob
{S,E,N,D, M,O,R, Y |
{S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 &
card({S,E,N,D, M,O,R, Y}) = 8 &
S*1000 + E*100 + N*10 + D +
M*1000 + O*100 + R*10 + E =
M*10000 + O*1000 + N*100 + E*10 + Y }
```
%% Output
{(((((((9↦5)↦6)↦7)↦1)↦0)↦8)↦2)}
%% Cell type:markdown id: tags:
A slightly more complicated puzzle (involving multiplication) is the KISS * KISS = PASSION problem.
%% Cell type:code id: tags:
``` prob
{K,P} <: 1..9 &
{I,S,A,O,N} <: 0..9 &
(1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S)
= 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N &
card({K, I, S, P, A, O, N}) = 7
```
%% Output
TRUE (P = 4 ∧ A = 1 ∧ S = 3 ∧ I = 0 ∧ K = 2 ∧ N = 9 ∧ O = 8)
%% Cell type:markdown id: tags:
Here is how we can solve the famous N-Queens puzzle for n=8.
%% Cell type:code id: tags:
``` prob
n = 8 &
queens : perm(1..n) /* for each column the row in which the queen is in */
&
!(q1,q2).(q1:1..n & q2:2..n & q2>q1
=> queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))
```
%% Output
TRUE (queens = {(1↦1),(2↦5),(3↦8),(4↦6),(5↦3),(6↦7),(7↦2),(8↦4)} ∧ n = 8)
%% Cell type:code id: tags:
``` prob
n = 16 &
queens : perm(1..n) /* for each column the row in which the queen is in */
&
!(q1,q2).(q1:1..n & q2:2..n & q2>q1
=> queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))
```
%% Output
TRUE (queens = {(1↦1),(2↦3),(3↦5),(4↦13),(5↦11),(6↦4),(7↦15),(8↦7),(9↦16),(10↦14),(11↦2),(12↦8),(13↦6),(14↦9),(15↦12),(16↦10)} ∧ n = 16)
%% Cell type:markdown id: tags:
A Puzzle from Smullyan:
Knights: always tell the truth
Knaves: always lie
1: A says: “B is a knave or C is a knave”
2: B says “A is a knight”
What are A & B & C?
Note: A,B,C are equal to TRUE if they are a knight and FALSE if they are a knave.
%% Cell type:code id: tags:
``` prob
(A=TRUE <=> (B=FALSE or C=FALSE)) & // Sentence 1
(B=TRUE <=> A=TRUE) // Sentence 2
```
%% Output
TRUE (A = TRUE ∧ B = TRUE ∧ C = FALSE)
%% Cell type:code id: tags:
``` prob
/* this computes the set of all models: */
{A,B,C| (A=TRUE <=> (B=FALSE or C=FALSE)) &
(B=TRUE <=> A=TRUE) }
```
%% Output
{((TRUE↦TRUE)↦FALSE)}
%% Cell type:code id: tags:
``` prob
```
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment