Fibonacci Numbers with Automatic Dynamic Programming - Revision history

Michael Leuschel at 11:05, 23 July 2014

2014-07-23T11:05:53Z

← Older revision		Revision as of 11:05, 23 July 2014
Line 19:		Line 19:

	<pre>		<pre>
	n DOM ProB Kodkod -> Result Fib(n)		n DOM ProB Kodkod -> Result Fib(n)
	10 1..100 0.01 1.93 sec		10 1..100 0.01 1.93 sec
	11 1..200 0.01 5.15 sec		11 1..200 0.01 5.15 sec

Michael Leuschel at 11:05, 23 July 2014

2014-07-23T11:05:43Z

← Older revision		Revision as of 11:05, 23 July 2014
Line 19:		Line 19:

	<pre>		<pre>
	n DOM ProB Kodkod -> Result Fib(n)		n DOM ProB Kodkod -> Result Fib(n)
	10 1..100 0.01 1.93 sec		10 1..100 0.01 1.93 sec
	11 1..200 0.01 5.15 sec		11 1..200 0.01 5.15 sec

Michael Leuschel at 11:05, 23 July 2014

2014-07-23T11:05:33Z

← Older revision		Revision as of 11:05, 23 July 2014
Line 19:		Line 19:

	<pre>		<pre>
	n DOM ProB Kodkod		n DOM ProB Kodkod -> Result Fib(n)
	10 1..100 0.01 1.93 sec		10 1..100 0.01 1.93 sec
	11 1..200 0.01 5.15 sec		11 1..200 0.01 5.15 sec

Michael Leuschel at 13:10, 20 July 2014

2014-07-20T13:10:47Z

← Older revision		Revision as of 13:10, 20 July 2014
Line 29:		Line 29:
	200 INTEGER 0.06 impossible -> 453973694165307953197296969697410619233826		200 INTEGER 0.06 impossible -> 453973694165307953197296969697410619233826
	</pre>		</pre>

			=== How does it work ===

			[TODO: insert explanation]

Michael Leuschel: Created page with 'In this example we show how one can encode the Fibonacci problem in such a way that you get dynamic programming automatically when using ProB to solve the encoding:

 MACHIN…'

2014-07-20T13:09:39Z

Created page with 'In this example we show how one can encode the Fibonacci problem in such a way that you get dynamic programming automatically when using ProB to solve the encoding: <pre> MACHIN…'

New page

In this example we show how one can encode the Fibonacci problem in such a way that you get dynamic programming automatically when using ProB to solve the encoding:

<pre>
MACHINE Fibonacci_Dynamic_Programming
/* an encoding of Fibonacci where we get dynamic programming for free from ProB */
DEFINITIONS
DOM == INTEGER; /* INTEGER : For ProB no restriction necessary; for Kodkod yes */
CONSTANTS n, fib, sol
PROPERTIES
fib : 0..n --> DOM &
fib(0) = 1 & fib(1) = 1 &
!x.(x:2..n => fib(x) = fib(x-1) + fib(x-2))

& n = 200 & sol = fib(n)
END
</pre>

Runtimes on a 1.7 GHz i7 Mac Book Air with ProB 1.4.0-rc2, where we have also used our Kodkod backend with minSAT for comparison. For Kodkod to be applicable, we had to constrain the domain DOM of possible Fibonacci numbers as indicated below:

<pre>
n DOM ProB Kodkod
10 1..100 0.01 1.93 sec
11 1..200 0.01 5.15 sec

10 INTEGER 0.01 impossible
20 INTEGER 0.01 impossible -> 10946
40 INTEGER 0.01 impossible -> 165580141
100 INTEGER 0.02 impossible -> 573147844013817084101
200 INTEGER 0.06 impossible -> 453973694165307953197296969697410619233826
</pre>