"[2018-06-04 13:54:15,603, T+25452] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 62613\n",
"[2018-06-04 13:54:15,605, T+25454] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47762\n",
"[2018-06-04 17:10:22,773, T+7878724] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 57165\n",
"[2018-06-04 17:10:22,774, T+7878725] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 52908\n",
"Relational inverse (.~) and relational image .[.] :"
]
...
...
@@ -985,7 +993,17 @@
"source": [
"## Constraint Solving Applications ##\n",
"Constraint solving has many applications in formal methods in general and B in particular.\n",
"\n",
"\n"
]
},
{
"cell_type": "markdown",
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
"source": [
"#### Animation ####\n",
"It is required to animate implicit specifications.\n",
"Take for example an event\n",
...
...
@@ -1150,7 +1168,11 @@
{
"cell_type": "code",
"execution_count": 32,
"metadata": {},
"metadata": {
"slideshow": {
"slide_type": "skip"
}
},
"outputs": [
{
"data": {
...
...
@@ -1173,7 +1195,7 @@
},
{
"cell_type": "code",
"execution_count": 33,
"execution_count": 16,
"metadata": {},
"outputs": [
{
...
...
@@ -1192,13 +1214,13 @@
"\tO = 0"
]
},
"execution_count": 33,
"execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"{S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 & \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",
...
...
@@ -1207,7 +1229,11 @@
},
{
"cell_type": "markdown",
"metadata": {},
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
"source": [
"We can find all solutions (to the unmodified puzzle) using a set comprehension and make sure that there is just a single soltuion:"
]
...
...
@@ -1237,6 +1263,37 @@
" M*10000 + O*1000 + N*100 + E*10 + Y }"
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"|Nr|S|E|N|D|M|O|R|Y|\n",
"|---|---|---|---|---|---|---|---|---|\n",
"|1|9|5|6|7|1|0|8|2|\n"
],
"text/plain": [
"Nr\tS\tE\tN\tD\tM\tO\tR\tY\n",
"1\t9\t5\t6\t7\t1\t0\t8\t2\n"
]
},
"execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":table {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": {
...
...
@@ -1331,13 +1388,27 @@
},
{
"cell_type": "markdown",
"metadata": {},
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
"source": [
"### Booleans ###\n",
"\n",
"If we have only booleans, constraint solving is equivalent to SAT solving.\n",
"Internally, ProB has an interpreter which does **not** translate to CNF (conjunctive normal form), but is otherwise similar to DPLL: deterministic propagations are carried out first (unit propagation) and there are heuristics to choose the next boolean variable to enumerate.\n",
"(We do not translate to CNF also because of well-definedness issues.)\n",
"(We do not translate to CNF also because of well-definedness issues.)\n"
]
},
{
"cell_type": "markdown",
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
"source": [
"\n",
"#### Knights and Knave Puzzle####\n",
"Here is a puzzle from Smullyan involving an island with only knights and knaves.\n",
...
...
@@ -1356,7 +1427,11 @@
{
"cell_type": "code",
"execution_count": 37,
"metadata": {},
"metadata": {
"slideshow": {
"slide_type": "fragment"
}
},
"outputs": [
{
"data": {
...
...
@@ -1391,45 +1466,7 @@
"\n",
"Let us take the integer constraint ```x*x=100``` which we saw earlier.\n",
"This constraint is actually more complicated than might appear at first sight: the constraint is not linear and the domain of x is not bounded. Indeed, B supports mathematical integers without any bit size restriction.\n",
"So, let us first look at some simpler constraints, where the domains of the variables are all bounded.\n",
"Let us consider a small arithmetic puzzle \n",
"```\n",
" X Y\n",
"+ X Y\n",
"-----\n",
" Y 0\n",
"```"
]
},
{
"cell_type": "code",
"execution_count": 38,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tX = 2\n",
"\tY = 5"
]
},
"execution_count": 38,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"X:1..9 & Y:0..9 & X*10 + Y + X*10 + Y = Y*10"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Given that we know the domain of X and Y one can represent the integers by binary numbers and convert the constraint to a SAT problem."
"So, let us first look at some simpler constraints, where the domains of the variables are all bounded."
]
},
{
...
...
@@ -1440,7 +1477,8 @@
}
},
"source": [
"Let us look at an even simpler constraint X:0..3 & Y:0..3 & X+Y=2. As you can see there are three solutions for this constraint:\n"
"Let us look at the simple constraint ```X:0..3 & Y:0..3 & X+Y=2```.\n",
"As you can see there are three solutions for this constraint:\n"
]
},
{
...
...
@@ -1472,11 +1510,15 @@
},
{
"cell_type": "markdown",
"metadata": {},
"metadata": {
"slideshow": {
"slide_type": "slide"
}
},
"source": [
"#### Solving constraints by translating to SAT ####\n",
"Given that we know the domain of X and Y in the constraint ``` X:0..3 & Y:0..3 & X+Y=2``` one can represent the integers by binary numbers and convert the constraint to a SAT problem.\n",
"The number 2 is 10 in binary and we can represent X and Y each by two bits X0,X1 and Y0,Y1.\n",
"Given that we know the *domain* of X and Y in the constraint ``` X:0..3 & Y:0..3 & X+Y=2```, we can represent the integers by binary numbers and convert the constraint to a **SAT** problem.\n",
"The number 2 is ```10``` in binary and we can represent X and Y each by two bits X0,X1 and Y0,Y1.\n",
"We can translate the addition to a propositional logic formula:\n",
"\n",
"Bit1 | Bit0\n",
...
...
@@ -1486,7 +1528,7 @@
" |\n",
" Z1 | Z0\n",
" \n",
"Let us find one solution to this constraint, by encoding addition using an additional carry bit:"
"Let us find one solution to this constraint, by encoding addition using an additional carry bit ```CARRY0```:"
]
},
{
...
...
@@ -1525,7 +1567,11 @@
{
"cell_type": "code",
"execution_count": 41,
"metadata": {},
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
"outputs": [
{
"data": {
...
...
@@ -1557,7 +1603,11 @@
{
"cell_type": "code",
"execution_count": 42,
"metadata": {},
"metadata": {
"slideshow": {
"slide_type": "fragment"
}
},
"outputs": [
{
"data": {
...
...
@@ -1602,7 +1652,11 @@
{
"cell_type": "code",
"execution_count": 43,
"metadata": {},
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
"outputs": [
{
"name": "stdout",
...
...
@@ -1676,12 +1730,28 @@
},
{
"cell_type": "markdown",
"metadata": {},
"metadata": {
"slideshow": {
"slide_type": "slide"
}
},
"source": [
"#### Translation to SMTLib ####\n",
"At iFM'2016 we (Krings, L.) presented a translation to SMTLib format to use either the Z3 or CVC4 SMT solver.\n",
"Compared to the Kodkod backend, no translation to SAT is performed, SMTLib supports integer predicates and operators in the language.\n",
"Here is ProB's SMTLib/Z3 API calls for the constraint:\n",
"At iFM'2016 we (Krings, L.) presented a translation to SMTLib format to use either the **Z3** or **CVC4** SMT solver.\n",
"Compared to the Kodkod backend, no translation to SAT is performed, SMTLib supports **integer** predicates and integer operators in the language.\n",
"\n",
"\n"
]
},
{
"cell_type": "markdown",
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
"source": [
"Here is ProB's SMTLib/Z3 API calls for the constraint ``` X:0..3 & Y:0..3 & X+Y=2```:\n",
"- mk_var(integer,x) $\\rightarrow$ 2\n",
"- mk_var(integer,y) $\\rightarrow$ 3\n",
"- mk_int_const(0) $\\rightarrow$ 4\n",
...
...
@@ -1726,7 +1796,7 @@
"cell_type": "markdown",
"metadata": {
"slideshow": {
"slide_type": "subslide"
"slide_type": "slide"
}
},
"source": [
...
...
@@ -1749,11 +1819,34 @@
" - x=2 $\\leadsto$ x:2..2, y:0..0"
]
},
{
"cell_type": "markdown",
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
"source": [
"Let us now examine the three approaches for the KISS-PASSION puzzle:"
]
},
{
"cell_type": "code",
"execution_count": 46,
"execution_count": 17,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"Execution time: 0.050491290 seconds"
],
"text/plain": [
"Execution time: 0.050491290 seconds"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/plain": [
...
...
@@ -1769,46 +1862,63 @@
"\tO = 8"
]
},
"execution_count": 46,
"execution_count": 17,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":solve 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"
":time :solve 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"
]
},
{
"cell_type": "code",
"execution_count": 47,
"metadata": {},
"execution_count": 18,
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
"outputs": [
{
"ename": "CommandExecutionException",
"evalue": ":solve: Computation not completed: no solution found (but one might exist)",
"evalue": ":time: :solve: Computation not completed: no solution found (but one might exist)",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
"\u001b[1m\u001b[31m:time: :solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
]
}
],
"source": [
":solve z3 {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"
":time :solve z3 {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"
]
},
{
"cell_type": "code",
"execution_count": 48,
"execution_count": 19,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[2018-06-04 14:01:42,085, T+471934] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: K : 1 .. 9 & P : 1 .. 9 & I : 0 .. 9 & S : 0 .. 9 ... ints: irange(0,99980001), intatoms: irange(0,9)\u001b[0m\n",
"[2018-06-04 14:01:42,086, T+471935] \"ProB Output Logger for instance 1ede3ed1\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [373]\u001b[0m\n"
"[2018-06-04 21:43:31,067, T+24267018] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: K : 1 .. 9 & P : 1 .. 9 & I : 0 .. 9 & S : 0 .. 9 ... ints: irange(0,99980001), intatoms: irange(0,9)\u001b[0m\n",
"[2018-06-04 21:43:31,069, T+24267020] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).\u001b[0m\n",
"[2018-06-04 21:43:31,069, T+24267020] \"ProB Output Logger for instance 17752aaa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [636]\u001b[0m\n"
]
},
{
"data": {
"text/markdown": [
"Execution time: 2.287290784 seconds"
],
"text/plain": [
"Execution time: 2.287290784 seconds"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/plain": [
...
...
@@ -1824,18 +1934,22 @@
"\tO = 8"
]
},
"execution_count": 48,
"execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":solve kodkod {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"
":time :solve kodkod {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"
]
},
{
"cell_type": "markdown",
"metadata": {},
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
"source": [
"Result for KISS*KISS=PASSION puzzle:\n",
"\n",
...
...
@@ -1848,7 +1962,11 @@
},
{
"cell_type": "markdown",
"metadata": {},
"metadata": {
"slideshow": {
"slide_type": "slide"
}
},
"source": [
"### Unbounded integers ###\n",
"The SAT translation via Kodkod/Alloy requires to determine the bid width.\n",
...
...
@@ -2020,7 +2138,8 @@
}
},
"source": [
"Here is an inconsistency which cannot be detected by CLP(FD)'s interval propagation. ProB can detect it with CHR enabled, but without the module the result is **UNKNOWN**."
"Here is an inconsistency which cannot be detected by CLP(FD)'s interval propagation.\n",
"ProB can detect it with CHR (Constraint Handling Rules) enabled, but without the module the result is **UNKNOWN**."
]
},
{
...
...
@@ -2072,7 +2191,11 @@
},
{
"cell_type": "markdown",
"metadata": {},
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
"source": [
"### Summary for Integer Arithmetic ###\n",
"\n",
...
...
@@ -2195,7 +2318,11 @@
},
{
"cell_type": "markdown",
"metadata": {},
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
"source": [
"This translation to SAT is exactly what the Kodkod backend does:"
]
...
...
@@ -2299,7 +2426,11 @@
},
{
"cell_type": "markdown",
"metadata": {},
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
"source": [
"Also, in the following constraint, the set x is unbounded and no translation to SAT is feasible (without a very clever analysis of the universal implications)."
" - works well for large sets and semi-deterministic computation\n",
" - works well for animation, data validation, disproving\n",
" - limitations trigger for symbolic model checking (IC3,...)\n",
" - Future work: improve combination with Z3, improve list representation (maybe use a bit-vector like representation) \n",
" - limitations appear for symbolic model checking (IC3,...)\n",
" - Future work: improve combination with Z3/Kodkod, improve list representation (maybe use a bit-vector like representation, and CLP(FD) cardinality variable) \n",
" "
]
},
{
"cell_type": "markdown",
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
"source": [
"### Integrations of Approaches ###\n",
"\n",
"ProB provides the joint application of the CLP(FD) and SMT backend (preference ```SMT_SUPPORTED_INTERPRETER```.\n",
"Constraints are posted both to ProB and Z3/CVC4, with the hope that Z3/CVC4 prune infeasible branches.\n",
"The main motivation was new symbolic validation techniques such as IC3.\n",
"\n",
"The Kodkod integration also passes higher-order/unbounded constraints to ProB, after solving the first order finite constraints with Kodkod/Alloy.\n",
"However, this kind of integration is rarely useful (most of the generated solutions get rejected by ProB).\n",
"\n",
"A more promising, fine-grained integration has been presented at PADL'18."
]
},
{
"cell_type": "markdown",
"metadata": {
...
...
@@ -3829,7 +4074,11 @@
},
{
"cell_type": "markdown",
"metadata": {},
"metadata": {
"slideshow": {
"slide_type": "subslide"
}
},
"source": [
"In the following the inverse operator seems to pose problems to Z3:"
]
...
...
@@ -3880,7 +4129,11 @@
},
{
"cell_type": "markdown",
"metadata": {},
"metadata": {
"slideshow": {
"slide_type": "slide"
}
},
"source": [
"### Comparison ###\n",
"Some further examples for comparison of the backends"
"[2018-06-04 14:09:21,622, T+931471] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 63550\n",
"[2018-06-04 14:09:21,622, T+931471] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47978\n",
"[2018-06-04 16:47:00,347, T+6476298] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 55595\n",
"[2018-06-04 16:47:00,348, T+6476299] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 52301\n",
"[2018-06-04 14:09:39,778, T+949627] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 63572\n",
"[2018-06-04 14:09:39,779, T+949628] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47990\n",
"[2018-06-04 15:03:07,015, T+242966] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 51091\n",
"[2018-06-04 15:03:07,018, T+242969] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 50312\n",
[2018-06-04 13:54:15,603, T+25452] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 62613
[2018-06-04 13:54:15,605, T+25454] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47762
[2018-06-04 17:10:22,773, T+7878724] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 57165
[2018-06-04 17:10:22,774, T+7878725] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 52908
For animation and constraint solving purposes, ProB will instantiate deferred sets to some finite set (the size of which can be controlled and is partially inferred).
%% Cell type:code id: tags:
``` prob
Points
```
%% Output
{Points1,Points2}
%% Cell type:markdown id: tags:
### Pairs ###
B also has pairs of values, which can be written in two ways:
B provides many operators which return values, such as the usual arithmetic operators but also many operators for sets, relations and functions.
For example set union and set difference:
%% Cell type:code id: tags:
``` prob
(1..3 \/ 5..10) \ (2..6)
```
%% Output
{1,7,8,9,10}
%% Cell type:code id: tags:
``` prob
(1..3 ∪ 5..10) \ (2..6)
```
%% Output
{1,7,8,9,10}
%% Cell type:markdown id: tags:
The range of a relation or function:
%% Cell type:code id: tags:
``` prob
ran({(thomas↦1),(gordon↦2)})
```
%% Output
{1,2}
%% Cell type:markdown id: tags:
Function application:
%% Cell type:code id: tags:
``` prob
{(thomas↦1),(gordon↦2)} (thomas)
```
%% Cell type:markdown id: tags:
Relational inverse (.~) and relational image .[.] :
%% Cell type:code id: tags:
``` prob
{(thomas↦1),(gordon↦2)}~[2..3]
```
%% Cell type:markdown id: tags:
## Predicates
ProB can also be used to evaluate predicates (B distinguishes between expressions which have a value and predicates which are either true or false).
%% Cell type:code id: tags:
``` prob
2>3
```
%% Output
FALSE
%% Cell type:code id: tags:
``` prob
3>2
```
%% Output
TRUE
%% Cell type:markdown id: tags:
Within predicates you can use **open** variables, which are implicitly existentially quantified.
ProB will display the solution for the open variables, if possible.
%% Cell type:code id: tags:
``` prob
x*x=100
```
%% Output
TRUE
Solution:
x = −10
%% Cell type:markdown id: tags:
We can find all solutions to a predicate by using the set comprehension notation.
Note that by this we turn a predicate into an expression.
%% Cell type:code id: tags:
``` prob
{x|x*x=100}
```
%% Output
{−10,10}
%% Cell type:markdown id: tags:
### Substitutions ###
B also has a rich syntax for substitutions, aka statements.
For example ```x := x+1``` increments the value of x by 1.
We will not talk about substitutions in the rest of this presentation.
The major differences between classical B and Event-B lie in the area of substitutions, machine composition and refinement.
%% Cell type:markdown id: tags:
## Definition of Constraint Solving ##
Constraint solving is determine whether a predicate with open/existentially quantified variables is satisfiable and providing values for the open variables in case it is.
We have already solved the predicate ```x*x=100``` above, yielding the solution ```x=-10```.
The following is an unsatisfiable predicate:
%% Cell type:code id: tags:
``` prob
x*x=1000
```
%% Output
FALSE
%% Cell type:markdown id: tags:
The difference to **proof** is that in constraint solving one has to produce a solution (aka a model). The difference to **execution** is that not all variables are known.
%% Cell type:markdown id: tags:
## Constraint Solving Applications ##
Constraint solving has many applications in formal methods in general and B in particular.
%% Cell type:markdown id: tags:
#### Animation ####
It is required to animate implicit specifications.
Take for example an event
```
train_catches_up = any t1,t2,x where t1:dom(train_position) & t2:dom(train_position) &
train_position(t1) < train_position(t2) &
x:1..(train_position(t2)-train_position(t1)-1) then
train_position(t1) := train_position(t1)+x end
```
To determine whether the event is enabled, and to obtain values for the parameters of the event in a given state of the model, we have to solve the following constraint:
Suppose that we have the invariant, ```train_position:TRAINS-->1..10000``` we can check whether the event is **feasible** in at least one valid state by solving:
{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
%% Cell type:code id: tags:
``` prob
{S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 &
{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
Solution:
R = 8
S = 9
D = 7
E = 5
Y = 2
M = 1
N = 6
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:code id: tags:
``` prob
:table {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
|Nr|S|E|N|D|M|O|R|Y|
|---|---|---|---|---|---|---|---|---|
|1|9|5|6|7|1|0|8|2|
Nr S E N D M O R Y
1 9 5 6 7 1 0 8 2
%% Cell type:markdown id: tags:
#### KISS PASSION Puzzle####
A slightly more complicated puzzle (involving multiplication) is the KISS * KISS = PASSION problem.
Finally, a simple puzzle involving sets is to find a subset of numbers from 1..5 whose sum is 14:
%% Cell type:code id: tags:
``` prob
x <: 1..5 & SIGMA(y).(y:x|y)=14
```
%% Output
TRUE
Solution:
x = {2,3,4,5}
%% Cell type:markdown id: tags:
## How to solve (set) constraints in B ##
We will now examine how one can perform constraint solving for B.
%% Cell type:markdown id: tags:
### Booleans ###
If we have only booleans, constraint solving is equivalent to SAT solving.
Internally, ProB has an interpreter which does **not** translate to CNF (conjunctive normal form), but is otherwise similar to DPLL: deterministic propagations are carried out first (unit propagation) and there are heuristics to choose the next boolean variable to enumerate.
(We do not translate to CNF also because of well-definedness issues.)
%% Cell type:markdown id: tags:
#### Knights and Knave Puzzle####
Here is a puzzle from Smullyan involving an island with only knights and knaves.
We know that:
- Knights: always tell the truth
- Knaves: always lie
We are given the following information about three persons A,B,C on the island:
1. A says: “B is a knave or C is a knave”
2. B says “A is a knight”
What are A, B and C?
Note: we model A,B,C as boolean variables which 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
Solution:
A = TRUE
B = TRUE
C = FALSE
%% Cell type:markdown id: tags:
### Integers ###
Let us take the integer constraint ```x*x=100``` which we saw earlier.
This constraint is actually more complicated than might appear at first sight: the constraint is not linear and the domain of x is not bounded. Indeed, B supports mathematical integers without any bit size restriction.
So, let us first look at some simpler constraints, where the domains of the variables are all bounded.
Let us consider a small arithmetic puzzle
```
X Y
+ X Y
-----
Y 0
```
%% Cell type:code id: tags:
``` prob
X:1..9 & Y:0..9 & X*10 + Y + X*10 + Y = Y*10
```
%% Output
TRUE
Solution:
X = 2
Y = 5
%% Cell type:markdown id: tags:
Given that we know the domain of X and Y one can represent the integers by binary numbers and convert the constraint to a SAT problem.
%% Cell type:markdown id: tags:
Let us look at an even simpler constraint X:0..3 & Y:0..3 & X+Y=2. As you can see there are three solutions for this constraint:
Let us look at the simple constraint ```X:0..3 & Y:0..3 & X+Y=2```.
As you can see there are three solutions for this constraint:
%% Cell type:code id: tags:
``` prob
{X,Y|X:0..3 & Y:0..3 & X+Y=2}
```
%% Output
{(0↦2),(1↦1),(2↦0)}
%% Cell type:markdown id: tags:
We will now study how such constraints can be solved.
%% Cell type:markdown id: tags:
#### Solving constraints by translating to SAT ####
Given that we know the domain of X and Y in the constraint ``` X:0..3 & Y:0..3 & X+Y=2``` one can represent the integers by binary numbers and convert the constraint to a SAT problem.
The number 2 is 10 in binary and we can represent X and Y each by two bits X0,X1 and Y0,Y1.
Given that we know the *domain* of X and Y in the constraint ``` X:0..3 & Y:0..3 & X+Y=2```, we can represent the integers by binary numbers and convert the constraint to a **SAT** problem.
The number 2 is ```10``` in binary and we can represent X and Y each by two bits X0,X1 and Y0,Y1.
We can translate the addition to a propositional logic formula:
Bit1 | Bit0
-----|-----
X1 | X0
+ Y1 | Y0
|
Z1 | Z0
Let us find one solution to this constraint, by encoding addition using an additional carry bit:
Let us find one solution to this constraint, by encoding addition using an additional carry bit```CARRY0```:
In ProB, we can use **Kodkod** backend to achieve such a translation to SAT.
- Kodkod (https://github.com/emina/kodkod) is the API to the **Alloy** (http://alloytools.org) constraint analyzer and takes relational logic predicates and translates them to SAT.
- The SAT problem can be solved by any SAT solver (Sat4J, minisat, glucose,...).
- ProB translates parts of B to the Kodkod API and translates the results back to B values.
- Prior to the translation, ProB performs an interval analysis to determine possible ranges for the integer decision variables.
The details were presented at FM'2012 (Plagge, L.).

%% Cell type:code id: tags:
``` prob
:solve kodkod x:0..2 & y:0..2 & x+y=2
```
%% Output
[2018-06-04 14:01:28,941, T+458790] "ProB Output Logger for instance 1ede3ed1" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: x : 0 .. 2 & y : 0 .. 2 & x + y = 2 ints: irange(0,4), intatoms: none[0m
[2018-06-04 14:01:28,941, T+458790] "ProB Output Logger for instance 1ede3ed1" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).[0m
[2018-06-04 14:01:28,942, T+458791] "ProB Output Logger for instance 1ede3ed1" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [2,5,2][0m
TRUE
Solution:
x = 2
y = 0
%% Cell type:markdown id: tags:
We can find all solutions and check that we find exactly the three expected solutions:
%% Cell type:code id: tags:
``` prob
:solve kodkod {x,y|x:0..2 & y:0..2 & x+y=2}=res
```
%% Output
[2018-06-04 14:01:31,052, T+460901] "ProB Output Logger for instance 1ede3ed1" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: {x,y|x : 0 .. 2 & y : 0 .. 2 & x + y = 2} = res ints: irange(0,4), intatoms: irange(0,2)[0m
[2018-06-04 14:01:31,054, T+460903] "ProB Output Logger for instance 1ede3ed1" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1][0m
TRUE
Solution:
res = {(0↦2),(1↦1),(2↦0)}
%% Cell type:markdown id: tags:
#### Translation to SMTLib ####
At iFM'2016 we (Krings, L.) presented a translation to SMTLib format to use either the Z3 or CVC4 SMT solver.
Compared to the Kodkod backend, no translation to SAT is performed, SMTLib supports integer predicates and operators in the language.
Here is ProB's SMTLib/Z3 API calls for the constraint:
At iFM'2016 we (Krings, L.) presented a translation to SMTLib format to use either the **Z3** or **CVC4** SMT solver.
Compared to the Kodkod backend, no translation to SAT is performed, SMTLib supports **integer** predicates and integer operators in the language.

%% Cell type:markdown id: tags:
Here is ProB's SMTLib/Z3 API calls for the constraint ``` X:0..3 & Y:0..3 & X+Y=2```:
ProB's default solver makes use of constraint logic programming.
For arithmetic, it builts on top of CLP(FD), the finite domain library of SICStus Prolog.
In CLP(FD):
- every integer variable is associated with a domain of possible values, typically an interval
- when adding a new constraints, the domains of the involved variables are updated, or more precisely narrowed down.
- at some point we need to chose variables for enumeration; typically ProB chooses the value with the smallest domain.
Let us use a slightly adapted constraint ```x:0..9 & y:0..9 & x+y=2``` to illustrate how constraint processing works:
- x:0..9 $\leadsto$ x:0..9, y:$-\infty$..$\infty$
- y:0..9 $\leadsto$ x:0..9, y:0..9
- x+y=2 $\leadsto$ x:0..2, y:0..2
- Enumerate (label) variable x
- x=0 $\leadsto$ x:0..0, y:2..2
- x=1 $\leadsto$ x:1..1, y:1..1
- x=2 $\leadsto$ x:2..2, y:0..0
%% Cell type:markdown id: tags:
Let us now examine the three approaches for the KISS-PASSION puzzle:
%% Cell type:code id: tags:
``` prob
:solve 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
:time :solve 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
Execution time: 0.050491290 seconds
TRUE
Solution:
P = 4
A = 1
S = 3
I = 0
K = 2
N = 9
O = 8
%% Cell type:code id: tags:
``` prob
:solve z3 {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
:time :solve z3 {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
:solve: Computation not completed: no solution found (but one might exist)
:time: :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags:
``` prob
:solve kodkod {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
:time :solve kodkod {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
[2018-06-04 14:01:42,085, T+471934] "ProB Output Logger for instance 1ede3ed1" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: K : 1 .. 9 & P : 1 .. 9 & I : 0 .. 9 & S : 0 .. 9 ... ints: irange(0,99980001), intatoms: irange(0,9)[0m
[2018-06-04 14:01:42,086, T+471935] "ProB Output Logger for instance 1ede3ed1" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [373][0m
[2018-06-04 21:43:31,067, T+24267018] "ProB Output Logger for instance 17752aaa" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: K : 1 .. 9 & P : 1 .. 9 & I : 0 .. 9 & S : 0 .. 9 ... ints: irange(0,99980001), intatoms: irange(0,9)[0m
[2018-06-04 21:43:31,069, T+24267020] "ProB Output Logger for instance 17752aaa" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).[0m
[2018-06-04 21:43:31,069, T+24267020] "ProB Output Logger for instance 17752aaa" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [636][0m
Execution time: 2.287290784 seconds
TRUE
Solution:
P = 4
A = 1
S = 3
I = 0
K = 2
N = 9
O = 8
%% Cell type:markdown id: tags:
Result for KISS*KISS=PASSION puzzle:
Solver | Runtime
-------|-------
ProB Default | 0.01 sec
Kodkod Backend | 1 sec
Z3 Backend | ? > 100 sec
%% Cell type:markdown id: tags:
### Unbounded integers ###
The SAT translation via Kodkod/Alloy requires to determine the bid width.
It cannot be applied to unbounded integers.
Even for bounded integers it is quite tricky to get the bid widths correct: one needs also to take care of intermediate results. Alloy can detect incorrect models where an overflow occured, but to our understanding not where an overflow prevented a model (e.g., use inside negation or equivalence, see ```#(V.SS->V.SS)=0 iff no V.SS``` in paper at ABZ conference).
SMTLib is more tailored towards proof than towards model finding; as such it has typically no/less issues with unbounded values.
The ProB default solver can also deal with unbounded integers: it tries to narrow down domains to finite ones. If this fails, an unbounded variable is enumerated (partially) and an **enumeration warning** is generated. In case a solution is found, this warning is ignored, otherwise the result of ProB's analysis is **UNKNOWN**.
Some inconsistencies cannot be detected by interval/domain propagation; here it helps to activate ProB's CHR module which performs some additional inferences.
Let us perform some experiments. Both ProB and Z3 can solve the following:
%% Cell type:code id: tags:
``` prob
:solve z3 x*x=100
```
%% Output
TRUE
Solution:
x = −10
%% Cell type:markdown id: tags:
Here is an example where ProB generates an enumeration warning, but finds a solution:
:solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags:
``` prob
:solve z3 x>100 & x mod 2000 = 1 & x mod 3000 = 1 & (x+x) mod 4501 = 0
```
%% Output
TRUE
Solution:
x = 6756001
%% Cell type:markdown id: tags:
Here is an inconsistency which cannot be detected by CLP(FD)'s interval propagation. ProB can detect it with CHR enabled, but without the module the result is **UNKNOWN**.
Here is an inconsistency which cannot be detected by CLP(FD)'s interval propagation.
ProB can detect it with CHR (Constraint Handling Rules) enabled, but without the module the result is **UNKNOWN**.
%% Cell type:code id: tags:
``` prob
:solve z3 x>y & y>x
```
%% Output
FALSE
%% Cell type:code id: tags:
``` prob
:solve prob x>y &y>x
```
%% Output
[2018-06-04 14:01:54,055, T+483904] "ProB Output Logger for instance 1ede3ed1" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Timeout when posting constraint:[0m
:solve: Computation not completed: no solution found (but one might exist)
%% Cell type:markdown id: tags:
### Summary for Integer Arithmetic ###
Solver | Unbounded | Model Finding | Inconsistency Detection (Unbounded)
------|------------|---------------|---
ProB CLP(FD) | yes | very good | limited with CHR
ProB Z3 | yes | reasonable | very good
ProB Kodkod | no | good | -
%% Cell type:markdown id: tags:
### Deferred and Enumerated Sets ###
Given an enumerated set ```Trains = {thomas, gordon}``` we associate a variable ```x:Trains``` with
an integer decision variable in the range 1..2.
Similarly, deferred sets are given a finite cardinality $n$, and a decision variables are in the range 1..n.
%% Cell type:code id: tags:
``` prob
x:Trains & y:Trains & x/=y
```
%% Output
TRUE
Solution:
x = thomas
y = gordon
%% Cell type:markdown id: tags:
## Set Constraints ##
After booleans, integers and enumerated set elements, let us now move to constraint solving involving set variables.
### Translation to SAT ###
The Kodkod/Alloy backend translates sets bit vectors. The size of the vector is the number of possible elements.
Take for example the following constraint:
%% Cell type:code id: tags:
``` prob
x <: 1..2 & y <: 1..2 & x \/ y = 1..2 & 1:x & x <<: y
```
%% Output
TRUE
Solution:
x = {1}
y = {1,2}
%% Cell type:code id: tags:
``` prob
{x1,x2,y1,y2} <: BOOL &
x1=TRUE or y1=TRUE & x2=TRUE or y2=TRUE & // x \/ y = 1..2
x1=TRUE & // 1:x
(x1=TRUE => y1=TRUE) & (x2=TRUE => y2=TRUE) & (x1/=y1 or x2/=y2) // x <<: y
```
%% Output
TRUE
Solution:
y1 = TRUE
x1 = TRUE
y2 = TRUE
x2 = FALSE
%% Cell type:markdown id: tags:
This translation to SAT is exactly what the Kodkod backend does:
%% Cell type:code id: tags:
``` prob
:solve kodkod x <: 1..2 & y<: 1..2 & x \/ y = 1..2 & 1:x & x <<: y
```
%% Output
[2018-06-04 14:02:32,427, T+522276] "ProB Output Logger for instance 1ede3ed1" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: x <: 1 .. 2 & y <: 1 .. 2 & x \/ y = 1 .. 2 & 1 : ... ints: irange(1,2), intatoms: irange(1,2)[0m
[2018-06-04 14:02:32,428, T+522277] "ProB Output Logger for instance 1ede3ed1" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1][0m
TRUE
Solution:
x = {1}
y = {1,2}
%% Cell type:markdown id: tags:
Limitations of translating set constraints to SAT:
- this cannot deal with **unbounded** sets: we need to know a finite type for each set, so that we can generate a finite bit vector
- this approach cannot usually deal with **higher order** sets (sets of sets), as the size of the bit vector would be prohibitively large
Given that:
%% Cell type:code id: tags:
``` prob
card(POW(1..100))
```
%% Output
1267650600228229401496703205376
%% Cell type:markdown id: tags:
translating the following constraint to SAT would require a bit vector of length 1267650600228229401496703205376.
%% Cell type:code id: tags:
``` prob
x <: POW(1..100) & {100}:x & !y.(y:x => {card(y)}:x)
```
%% Output
TRUE
Solution:
x = {{100},{1}}
%% Cell type:markdown id: tags:
Also, in the following constraint, the set x is unbounded and no translation to SAT is feasible (without a very clever analysis of the universal implications).
For the following set, ProB tries to expand it and then an enumeration warning occurs (also called a **virtual timeout**, ProB realises that no matter what time budget it would be given a timeout would occur).
The set is then kept symbolic and can again be used in various ways.
%% Cell type:code id: tags:
``` prob
inf = {x|x>1000 & x mod 25 = 0} & 1025 ∈ inf & not(1000∈inf) & res = (900..1100) ∩ inf
res = ((900 ‥ 1100) ∩ {x∣x > 1000 ∧ x mod 25 = 0})
%% Cell type:markdown id: tags:
The virtual timeout message can be removed (and performance improved) by adding the symbolic pragma:
%% Cell type:code id: tags:
``` prob
inf = /*@symbolic*/ {x|x>1000 & x mod 25 = 0} & 1025 ∈ inf & not(1000∈inf) & res = (900..1100) ∩ inf
```
%% Output
TRUE
Solution:
inf = {x∣x > 1000 ∧ x mod 25 = 0}
res = ((900 ‥ 1100) ∩ {x∣x > 1000 ∧ x mod 25 = 0})
%% Cell type:markdown id: tags:
Internally, a symbolic representation is a **closure** in functional programming terms: all dependent variables are *compiled* into the closure: the closure can be passed as a value and evaluated without needing access to an environment. In Prolog this is represented as a tuple:
- closure(Parameters,Types,CompiledPredicate)
For example, a set {x|x>v} where v has the value 17 is compiled to:
- closure([x],[integer],```x>17```)
%% Cell type:markdown id: tags:
#### List representation ####
The list representation is used when a finite set is partially known and constraint solving has to determine the set.
x = {3,5,6,7,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,1,2,4,8,16,32,64}
y = {200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,256}
n = 100
%% Cell type:markdown id: tags:
In the appendix there are more examples which analyse the performance for such examples.
%% Cell type:markdown id: tags:
ProB employs the *Andorra* principle: deterministic computations are done first.
As there are multiple set representations, there are actually two kinds of deterministic computations:
- deterministic computations that generate an efficient representation, e.g., an AVL set representation
- and other deterministic computations
The ProB solver has a **WAITFLAG store** where choice points and enumerations are registered with a given priority.
- Priority 0 means that an efficient representation can be generated
- Priority 1 is a deterministic computation not guaranteed to produce an efficient representation
- Priority k is a choice point/enumeration which may generate k possible values
At each solving step one waitflag is activated, the one with the lowest priority.
CLP(FD) variables are also registered in the WAITFLAG store and are enumerated before a waitflag of the same priority is activated. For tie breaking one typically uses the **most attached constraints first** (ffc) heuristic.
#### Example ####
Let us examine how ```x = 1..n & y = 2*n..3*n & n = 100 & xy = x \/ y``` is solved.
- all constraints are registered
- in phase 0 ```n=100``` is run
- this means that ```1..n``` can be efficiently computed
- this means that ```x = 1..n``` triggers in phase 0
- then ```2*n``` and ```3*n``` can be computed, followed by ```2*n..3*n```
- this means that ```y = 2*n..3*n``` triggers in phase 0
- again, this means that ```x \/ y``` can be efficiently computed
- finally ```xy = x \/ y``` can be executed in phase 0
No enumeration was required. In this case ProB's constraint solver works similar to a topological sorting algorithm.
%% Cell type:markdown id: tags:
#### Dealing with unbounded enumeration ####
Note: if an unbounded enumeration is encountered, the solver registers an **enumeration warning** in the current scope (every quantification / comprehension set results in a new inner scope). Depending on the kind of scope (existential/universal) and on whether a solution is found, the warning gets translated into an **UNKNOWN** result.
%% Cell type:markdown id: tags:
### Functional Programming ###
Some functions are automatically detected as infinite by ProB, are kept symbolic but can be applied in several ways:
%% Cell type:code id: tags:
``` prob
f = %x.(x:INTEGER|x*x) &
r1 = f(100000) &
r2 = f[1..10] &
r3 = ([2,3,5,7,11] ; f) &
r4 = iterate(f,3)(2) &
f(sqrt) = 100
```
%% Output
TRUE
Solution:
r2 = {1,4,9,16,25,36,49,64,81,100}
r3 = [4,9,25,49,121]
r4 = 256
sqrt = 10
f = λx·(x ∈ INTEGER∣x ∗ x)
r1 = 10000000000
%% Cell type:code id: tags:
``` prob
f = {x,y|x:NATURAL & y**2 >= x & (y-1)**2 <x } & // integer square root function
[2018-06-04 14:08:39,826, T+889675] "ProB Output Logger for instance 1ede3ed1" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] [0m[31m[1m! Keeping comprehension-set symbolic (you may want to use the /*@symbolic*/ pragma to prevent this message, unless it was due to a WD-Error), identifiers: [x,y][0m
[2018-06-04 14:08:39,827, T+889676] "ProB Output Logger for instance 1ede3ed1" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] [0m[31m[1m! Line: 1 Column: 9 until 44[0m
From A\/B=D we and D=C we could infer A<:C and hence A/\C=C and hence A={} which is in conflict with A/={}.
ProB (as well as Kodkod and Z3 backends) can only infer the conflict for finite domains:
%% Cell type:code id: tags:
``` prob
A \/ B = D & A /\ C = {} & D=C & A /= {} & A:POW(BOOL)
```
%% Output
FALSE
%% Cell type:code id: tags:
``` prob
:solve kodkod A \/ B = D & A /\ C = {} & D=C & A /= {} & A:POW(BOOL)
```
%% Output
[2018-06-04 14:08:48,854, T+898703] "ProB Output Logger for instance 1ede3ed1" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: A \/ B = D & A /\ C = {} & D = C & A /= {} ints: none, intatoms: none[0m
[2018-06-04 14:08:48,854, T+898703] "ProB Output Logger for instance 1ede3ed1" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [][0m
FALSE
%% Cell type:code id: tags:
``` prob
:solve z3 A \/ B = D & A /\ C = {} & D=C & A /= {} & A:POW(BOOL)
```
%% Output
FALSE
%% Cell type:markdown id: tags:
Setlog has problems with larger sets. For example, the following takes 24 seconds using the latest stable release 4.9.1 of Setlog from http://people.dmi.unipr.it/gianfranco.rossi/setlog.Home.html:
```
{log}=> diff(int(1,200),{50},R).
R = {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200}
Another solution? (y/n)
```
In ProB this is instantenous:
%% Cell type:code id: tags:
``` prob
:time R= (1..200) \ {50}
```
%% Output
Execution time: 0.005074849 seconds
TRUE
Solution:
R = {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200}
%% Cell type:markdown id: tags:
## Summary of Set Constraint Solving Approaches ##
- SAT Translation (Kodkod backend):
- needs finite and small base type, no unbounded or higher-order sets
- can be very effective for complex constraints involving image, transitive closure,...
- limited performance for large sets
- SMTLib Translation (Z3/CVC4 backend):
- can deal with unbounded and large sets
- due to heavy use of quantifiers, some finite constraints get translated into infinite ones: limited model finding capabilities
- works well for large sets and semi-deterministic computation
- works well for animation, data validation, disproving
- limitations trigger for symbolic model checking (IC3,...)
- Future work: improve combination with Z3, improve list representation (maybe use a bit-vector like representation)
- limitations appear for symbolic model checking (IC3,...)
- Future work: improve combination with Z3/Kodkod, improve list representation (maybe use a bit-vector like representation, and CLP(FD) cardinality variable)
%% Cell type:markdown id: tags:
### Integrations of Approaches ###
ProB provides the joint application of the CLP(FD) and SMT backend (preference ```SMT_SUPPORTED_INTERPRETER```.
Constraints are posted both to ProB and Z3/CVC4, with the hope that Z3/CVC4 prune infeasible branches.
The main motivation was new symbolic validation techniques such as IC3.
The Kodkod integration also passes higher-order/unbounded constraints to ProB, after solving the first order finite constraints with Kodkod/Alloy.
However, this kind of integration is rarely useful (most of the generated solutions get rejected by ProB).
A more promising, fine-grained integration has been presented at PADL'18.
%% Cell type:markdown id: tags:
## Appendix ##
%% Cell type:markdown id: tags:
### Explicit Computations ####
What about explicit computations? How well does the SMTLib translation fare here?
%% Cell type:code id: tags:
``` prob
:solve z3 x = 1..1000 /\ (200..300)
```
%% Output
:solve: Computation not completed: no solution found (but one might exist)
%% Cell type:code id: tags:
``` prob
:time :solve z3 x = 1..40 /\ (6..15)
```
%% Output
Execution time: 0.175097068 seconds
TRUE
Solution:
x = {6,7,8,9,10,11,12,13,14,15}
%% Cell type:code id: tags:
``` prob
:time :solve z3 x = 1..60 /\ (6..15)
```
%% Output
Execution time: 0.754973438 seconds
TRUE
Solution:
x = {6,7,8,9,10,11,12,13,14,15}
%% Cell type:code id: tags:
``` prob
:time :solve z3 x = 1..80 /\ (6..15)
```
%% Output
Execution time: 2.369086566 seconds
TRUE
Solution:
x = {6,7,8,9,10,11,12,13,14,15}
%% Cell type:code id: tags:
``` prob
:time :solve prob x = 1..80 /\ (6..15)
```
%% Output
Execution time: 0.004883079 seconds
TRUE
Solution:
x = (6 ‥ 15)
%% Cell type:markdown id: tags:
In the following the inverse operator seems to pose problems to Z3:
f = {(1↦1),(2↦2),(3↦3),(4↦4),(5↦5),(6↦6),(7↦7),(8↦8),(9↦9),(10↦10),(11↦11),(12↦12),(13↦13),(14↦14),(15↦15),(16↦16),(17↦17),(18↦18),(19↦19),(20↦20),(21↦21),(22↦22),(23↦23),(24↦24),(25↦25),(26↦26),(27↦27),(28↦28),(29↦29),(30↦30),(31↦31),(32↦32),(33↦33),(34↦34),(35↦35),(36↦36),(37↦37),(38↦38),(39↦39),(40↦40),(41↦41),(42↦42),(43↦43),(44↦44),(45↦45),(46↦46),(47↦47),(48↦48),(49↦49),(50↦50)}
[2018-06-04 14:09:10,559, T+920408] "ProB Output Logger for instance 1ede3ed1" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: f : 1 .. n --> 1 .. n & !x.(x : 2 .. n => f(x) = f... ints: irange(1,50), intatoms: irange(1,50)[0m
[2018-06-04 14:09:10,560, T+920409] "ProB Output Logger for instance 1ede3ed1" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [1185][0m
Execution time: 3.657044854 seconds
TRUE
Solution:
f = {(3↦3),(5↦5),(6↦6),(7↦7),(9↦9),(10↦10),(11↦11),(12↦12),(13↦13),(14↦14),(15↦15),(17↦17),(18↦18),(19↦19),(20↦20),(21↦21),(22↦22),(23↦23),(24↦24),(25↦25),(26↦26),(27↦27),(28↦28),(29↦29),(30↦30),(31↦31),(33↦33),(34↦34),(35↦35),(36↦36),(37↦37),(38↦38),(39↦39),(40↦40),(41↦41),(42↦42),(43↦43),(44↦44),(45↦45),(46↦46),(47↦47),(48↦48),(49↦49),(50↦50),(1↦1),(2↦2),(4↦4),(8↦8),(16↦16),(32↦32)}
[2018-06-04 14:09:21,622, T+931471] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 63550
[2018-06-04 14:09:21,622, T+931471] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47978
[2018-06-04 16:47:00,347, T+6476298] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 55595
[2018-06-04 16:47:00,348, T+6476299] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 52301
[2018-06-04 14:09:25,781, T+935630] "ProB Output Logger for instance 2d81a536" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).[0m
[2018-06-04 14:09:25,782, T+935631] "ProB Output Logger for instance 2d81a536" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [][0m
Execution time: 0.837816834 seconds
FALSE
%% Cell type:code id: tags:
``` prob
:time :solve z3 edges : NODES5 <-> NODES5 &
edges~=edges &
not(#(n1,n2).(n1:NODES5 & n2:NODES5 & n2/=n1 &
card(edges[{n1}]) = card(edges[{n2}]))) &
dom(edges)=NODES5 & id(NODES5) /\ edges = {}
```
%% Output
:time: :solve: Computation not completed: no solution found (but one might exist)
%% Cell type:markdown id: tags:
So with Kodkod we proved the theorem for 5 nodes in about a second.
[2018-06-04 14:09:34,585, T+944434] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 63565
[2018-06-04 14:09:34,585, T+944434] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47984
[2018-06-04 14:09:38,480, T+948329] "ProB Output Logger for instance 79d26131" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).[0m
[2018-06-04 14:09:38,480, T+948329] "ProB Output Logger for instance 79d26131" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [2][0m
[2018-06-04 14:09:39,778, T+949627] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 63572
[2018-06-04 14:09:39,779, T+949628] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47990
[2018-06-04 15:03:07,015, T+242966] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 51091
[2018-06-04 15:03:07,018, T+242969] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 50312
[2018-06-04 14:09:41,873, T+951722] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 63578
[2018-06-04 14:09:41,874, T+951723] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 47994