From 34f6927d95240c6814943a9297b23129fca2be98 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Fri, 11 May 2018 08:05:00 +0200
Subject: [PATCH] add ProB constraint solver introduction
---
notebooks/tutorials/prob_solver_intro.ipynb | 372 ++++++++++++++++++++
1 file changed, 372 insertions(+)
create mode 100644 notebooks/tutorials/prob_solver_intro.ipynb
diff --git a/notebooks/tutorials/prob_solver_intro.ipynb b/notebooks/tutorials/prob_solver_intro.ipynb
new file mode 100644
index 0000000..2a3ea5c
--- /dev/null
+++ b/notebooks/tutorials/prob_solver_intro.ipynb
@@ -0,0 +1,372 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "We can use ProB to perform computations:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "1024"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "2**10"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "ProB supports *mathematical* integers without restriction (apart from memmory consumption):"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "1267650600228229401496703205376"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "2**100"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "We can find solutions for equations. Open variables are implicitly existentially quantified:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "TRUE (x = −10)"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x*x=100"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "We can find all solutions to a predicate by using the set comprehension notation."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "{−10,10}"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{x|x*x=100}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "We now try and solve the SEND+MORE=MONEY arithmetic puzzle in B, involving 8 distinct digits:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "TRUE (R = 8 ∧ S = 9 ∧ D = 7 ∧ E = 5 ∧ Y = 2 ∧ M = 1 ∧ N = 6 ∧ O = 0)"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ " {S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 & \n",
+ " card({S,E,N,D, M,O,R, Y}) = 8 & \n",
+ " S*1000 + E*100 + N*10 + D +\n",
+ " M*1000 + O*100 + R*10 + E =\n",
+ " M*10000 + O*1000 + N*100 + E*10 + Y"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Observe how we have used the cardinality constraint to express that all digits are distinct.\n",
+ "If we leave out this cardinality constraint, other solutions are possible:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "TRUE (R = 0 ∧ S = 9 ∧ D = 0 ∧ E = 0 ∧ Y = 0 ∧ M = 1 ∧ N = 0 ∧ O = 0)"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ " {S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 & \n",
+ " // card({S,E,N,D, M,O,R, Y}) = 8 & // commented out\n",
+ " S*1000 + E*100 + N*10 + D +\n",
+ " M*1000 + O*100 + R*10 + E =\n",
+ " M*10000 + O*1000 + N*100 + E*10 + Y"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "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",
+ "execution_count": 7,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "{(((((((9↦5)↦6)↦7)↦1)↦0)↦8)↦2)}"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ " {S,E,N,D, M,O,R, Y |\n",
+ " {S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 & \n",
+ " card({S,E,N,D, M,O,R, Y}) = 8 & \n",
+ " S*1000 + E*100 + N*10 + D +\n",
+ " M*1000 + O*100 + R*10 + E =\n",
+ " M*10000 + O*1000 + N*100 + E*10 + Y }"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "A slightly more complicated puzzle (involving multiplication) is the KISS * KISS = PASSION problem."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "TRUE (P = 4 ∧ A = 1 ∧ S = 3 ∧ I = 0 ∧ K = 2 ∧ N = 9 ∧ O = 8)"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ " {K,P} <: 1..9 &\n",
+ " {I,S,A,O,N} <: 0..9 &\n",
+ " (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) \n",
+ " = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N &\n",
+ " card({K, I, S, P, A, O, N}) = 7"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Here is how we can solve the famous N-Queens puzzle for n=8."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "TRUE (queens = {(1↦1),(2↦5),(3↦8),(4↦6),(5↦3),(6↦7),(7↦2),(8↦4)} ∧ n = 8)"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ " n = 8 & \n",
+ " queens : perm(1..n) /* for each column the row in which the queen is in */\n",
+ " &\n",
+ " !(q1,q2).(q1:1..n & q2:2..n & q2>q1\n",
+ " => queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "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)"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "n = 16 & \n",
+ " queens : perm(1..n) /* for each column the row in which the queen is in */\n",
+ " &\n",
+ " !(q1,q2).(q1:1..n & q2:2..n & q2>q1\n",
+ " => queens(q1)+(q2-q1) /= queens(q2) & queens(q1)+(q1-q2) /= queens(q2))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "A Puzzle from Smullyan:\n",
+ " Knights: always tell the truth\n",
+ " Knaves: always lie\n",
+ "\n",
+ " 1: A says: “B is a knave or C is a knave”\n",
+ " 2: B says “A is a knight”\n",
+ "\n",
+ " What are A & B & C?\n",
+ " Note: A,B,C are equal to TRUE if they are a knight and FALSE if they are a knave."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "TRUE (A = TRUE ∧ B = TRUE ∧ C = FALSE)"
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ " (A=TRUE <=> (B=FALSE or C=FALSE)) & // Sentence 1\n",
+ " (B=TRUE <=> A=TRUE) // Sentence 2"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "{((TRUE↦TRUE)↦FALSE)}"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "/* this computes the set of all models: */ \n",
+ "{A,B,C| (A=TRUE <=> (B=FALSE or C=FALSE)) &\n",
+ " (B=TRUE <=> A=TRUE) }"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
--
GitLab