Fibonacci Numbers with Automatic Dynamic Programming: Difference between revisions
No edit summary |
No edit summary |
||
| (2 intermediate revisions by the same user not shown) | |||
| 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 | ||
Latest revision as of 11:05, 23 July 2014
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:
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
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:
n DOM ProB Kodkod -> Result Fib(n) 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
How does it work
[TODO: insert explanation]