I invented some new way to describe the puzzle to the SAT solver (after having a closer look into the solver from ais)... and now the performance definitely outbeats all the others! The "benchmark" puzzle is solved in just one minute for both the shortest and the fastest solution... So here comes the best solutions for these:
(Sorry for all those long posts, but I think these news are worth it... There are still some bugs left, I'll fix them before this gets released.)
The parameters given:
Download main.cppLanguage: cpp
int main()
{
PolariumPuzzle *p = new PolariumPuzzle();
Solution s;
unsigned char puz[] = {
1,0,0,0,0,0,0,0,
0,0,0,0,0,0,0,1,
1,0,0,0,0,0,0,0,
0,0,0,0,0,0,0,1,
1,0,0,0,0,0,0,0,
0,0,0,0,0,0,0,1,
1,0,0,0,0,0,0,0,
0,0,0,0,0,0,0,1
};
p->SetPuzzle(puz, 8, 8);
//p->Solve();
// prove that all solutions require at least 63 frames
p->ConvertToCNF(s, 62, -1, -1);
// prove that all solutions are at least 44 tiles long.
p->ConvertToCNF(s, -1, 43, -1);
// find a solution which is exactly 44 tiles long.
p->ConvertToCNF(s, -1, 44, -1);
// find a solution which requires 63 frames
p->ConvertToCNF(s, 63, -1, -1);
delete p;
}
Download output.txtLanguage: txt
solvingpattern[0]:
0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0
0 0 1 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 1 0 0
0 0 1 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 1 0 0
0 0 1 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 1 0 0
0 0 1 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 1 0 0
0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0
solvingpattern[1]:
0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 1 1 1 1 1 1 1 0 0
0 0 1 1 1 1 1 1 1 0 0 0
0 0 0 1 1 1 1 1 1 1 0 0
0 0 1 1 1 1 1 1 1 0 0 0
0 0 0 1 1 1 1 1 1 1 0 0
0 0 1 1 1 1 1 1 1 0 0 0
0 0 0 1 1 1 1 1 1 1 0 0
0 0 1 1 1 1 1 1 1 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0
validpattern[0]:
0 0 0 0 0 0 0 0 0 0 0 0
0 1 1 1 1 1 1 1 1 1 1 0
0 1 1 0 0 0 0 0 0 0 1 0
0 1 0 0 0 0 0 0 0 1 1 0
0 1 1 0 0 0 0 0 0 0 1 0
0 1 0 0 0 0 0 0 0 1 1 0
0 1 1 0 0 0 0 0 0 0 1 0
0 1 0 0 0 0 0 0 0 1 1 0
0 1 1 0 0 0 0 0 0 0 1 0
0 1 0 0 0 0 0 0 0 1 1 0
0 1 1 1 1 1 1 1 1 1 1 0
0 0 0 0 0 0 0 0 0 0 0 0
validpattern[1]:
0 0 0 0 0 0 0 0 0 0 0 0
0 1 1 1 1 1 1 1 1 1 1 0
0 1 0 1 1 1 1 1 1 1 1 0
0 1 1 1 1 1 1 1 1 0 1 0
0 1 0 1 1 1 1 1 1 1 1 0
0 1 1 1 1 1 1 1 1 0 1 0
0 1 0 1 1 1 1 1 1 1 1 0
0 1 1 1 1 1 1 1 1 0 1 0
0 1 0 1 1 1 1 1 1 1 1 0
0 1 1 1 1 1 1 1 1 0 1 0
0 1 1 1 1 1 1 1 1 1 1 0
0 0 0 0 0 0 0 0 0 0 0 0
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
| |
| Number of variables: 35815 |
| Number of clauses: 137659 |
| Parse time: 0.14 s |
| Eliminated clauses: 0.40 Mb |
| Simplification time: 0.45 s |
| |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
| 100 | 23005 125256 477030 | 45927 99 10 | 2.706 % |
| 250 | 23005 125256 477030 | 50519 249 10 | 2.706 % |
| 475 | 23005 125256 477030 | 55571 474 10 | 2.706 % |
| 812 | 23004 125128 476476 | 61129 810 10 | 2.708 % |
| 1318 | 23003 123653 469868 | 67242 1315 10 | 2.711 % |
| 2077 | 23002 122891 466414 | 73966 2073 12 | 2.714 % |
| 3216 | 23001 122161 463177 | 81362 3211 14 | 2.717 % |
| 4924 | 23000 121392 459678 | 89499 4918 15 | 2.720 % |
| 7486 | 22998 119946 453165 | 98449 7478 16 | 2.725 % |
| 11330 | 22998 119946 453165 | 108293 11322 16 | 2.725 % |
| 17096 | 22998 119946 453165 | 119123 17088 16 | 2.725 % |
===============================================================================
restarts : 82
conflicts : 22894 (1192 /sec)
decisions : 31340 (0.00 % random) (1632 /sec)
propagations : 46316550 (2411667 /sec)
conflict literals : 354771 (43.34 % deleted)
Memory used : 25.00 MB
CPU time : 19.2052 s
UNSATISFIABLE
no solution found!
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
| |
| Number of variables: 50568 |
| Number of clauses: 130856 |
| Parse time: 0.13 s |
| Eliminated clauses: 0.71 Mb |
| Simplification time: 0.52 s |
| |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
| 100 | 29069 113210 375677 | 41510 98 11 | 1.805 % |
| 250 | 29048 113210 375677 | 45661 246 10 | 1.847 % |
| 475 | 29048 112702 373494 | 50227 471 13 | 1.847 % |
| 812 | 29048 112702 373494 | 55250 808 13 | 1.847 % |
| 1318 | 29048 112702 373494 | 60775 1314 15 | 1.847 % |
| 2077 | 28988 105341 340930 | 66852 941 11 | 1.966 % |
===============================================================================
restarts : 15
conflicts : 2575 (1617 /sec)
decisions : 4631 (0.00 % random) (2909 /sec)
propagations : 3351230 (2104913 /sec)
conflict literals : 35041 (49.05 % deleted)
Memory used : 29.00 MB
CPU time : 1.5921 s
UNSATISFIABLE
no solution found!
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
| |
| Number of variables: 51271 |
| Number of clauses: 133003 |
| Parse time: 0.13 s |
| Eliminated clauses: 0.72 Mb |
| Simplification time: 0.53 s |
| |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
| 100 | 29110 114006 379144 | 41802 98 9 | 1.818 % |
| 250 | 29110 113932 378991 | 45982 248 10 | 1.818 % |
| 475 | 29110 113932 378991 | 50580 473 13 | 1.818 % |
| 812 | 29110 113932 378991 | 55638 810 14 | 1.818 % |
| 1318 | 29090 113874 378875 | 61202 1315 14 | 1.857 % |
===============================================================================
restarts : 10
conflicts : 1545 (1215 /sec)
decisions : 5911 (0.00 % random) (4647 /sec)
propagations : 2194265 (1724944 /sec)
conflict literals : 21216 (47.44 % deleted)
Memory used : 29.00 MB
CPU time : 1.27208 s
SATISFIABLE
row 1 was NOT flipped
row 2 was flipped
row 3 was NOT flipped
row 4 was flipped
row 5 was flipped
row 6 was NOT flipped
row 7 was NOT flipped
row 8 was flipped
VISITED FIELDS:
0000000000
1100000000
1111111100
1100000000
1111111100
1011111110
1000000011
1100000001
0111111101
0000000111
START: (5,4)
END: (10,7)
SOLUTION:
. . . . . . . . . .
x-x . . . . . . . .
| |
x x-x-x-x-x-x-x . .
|
x-x . . . . . . . .
|
x-x x-x-x-x x-x . .
| | | | |
x . x-x-x x-x x-x .
| |
x . . . . . . . x-x
| |
x-x . . . . . . . x
| |
. x-x-x-x-x-x-x . x
| |
. . . . . . . x-x-x
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
| |
| Number of variables: 36148 |
| Number of clauses: 138325 |
| Parse time: 0.14 s |
| Eliminated clauses: 0.39 Mb |
| Simplification time: 0.44 s |
| |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
| 100 | 23495 127201 483784 | 46640 98 8 | 3.093 % |
| 250 | 23494 127201 483784 | 51304 247 8 | 3.096 % |
| 475 | 23494 127201 483784 | 56434 472 8 | 3.096 % |
| 812 | 23492 125965 479068 | 62078 805 9 | 3.101 % |
| 1318 | 23491 123842 469597 | 68286 1310 12 | 3.104 % |
| 2077 | 23319 123319 467901 | 75114 2062 14 | 3.580 % |
| 3216 | 23319 123319 467901 | 82626 3201 16 | 3.580 % |
| 4924 | 23318 122580 464582 | 90888 4908 17 | 3.582 % |
| 7486 | 23317 121841 461269 | 99977 7469 18 | 3.585 % |
| 11330 | 23317 121841 461269 | 109975 11313 17 | 3.585 % |
| 17096 | 23317 121841 461269 | 120973 17079 17 | 3.585 % |
| 25745 | 23317 121841 461269 | 133070 25728 17 | 3.585 % |
===============================================================================
restarts : 116
conflicts : 31424 (1238 /sec)
decisions : 45215 (0.00 % random) (1782 /sec)
propagations : 54177150 (2135179 /sec)
conflict literals : 523569 (43.51 % deleted)
Memory used : 25.00 MB
CPU time : 25.3736 s
SATISFIABLE
row 1 was NOT flipped
row 2 was flipped
row 3 was flipped
row 4 was NOT flipped
row 5 was flipped
row 6 was flipped
row 7 was NOT flipped
row 8 was flipped
VISITED FIELDS:
0000000000
1100000000
1111111100
1011111111
1000000011
1011111111
1111111101
0100000001
0111111101
0000000111
START: (3,2)
END: (14,7)
SOLUTION:
. . . . . . . . . .
x-x . . . . . . . .
| |
x x-x-x-x-x-x-x . .
| |
x . x-x-x-x-x-x x-x
| | |
x . . . . . . . x x
| | |
x . x-x-x-x-x-x-x x
| | |
x-x x-x-x-x-x-x . x
| |
. x . . . . . . . x
| |
. x-x-x-x-x-x-x . x
| |
. . . . . . . x-x-x
--------------------------------------------------------------------------------------
Yay, now everything is done, even some fine-tuning.
Now it can even solve a benchmark puzzle which is a lot harder:
Download puzzle_benchmark3.txtLanguage: txt
12 12
1 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 1
1 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 1
1 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 1
1 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 1
1 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 1
1 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 1
It takes one hour to find the shortest, and the fastest solution, and it takes about 20 minutes to verify that a given solution is optimal. Note that no attempt was done for finding the fastest solution for a given amount of steps, but that's possible too. The solutions take 97 tiles, or 109 frames.
So the solutions:
Download fastest_puzzle_benchmark3.txtLanguage: txt
SOLUTION:
X#X#X . . . . . . . . . . .
# #
X . X#X#X#X#X#X#X#X#X#X#X .
# #
X . . . . . . . . . . . X#X
# #
X#X . . . . . . . . . . . X
# #
X#X X#X#X#X#X#X#X#X#X#E . X
# # #
X . X#X#X#X#X#X#X#X#X#X#X X
# # #
X . . . . . . . . . . . X#X
#
X#X . . . . . . . . . . . .
#
X#X X#X#X#X#X#X#X#X#X#S . .
# #
X . X#X#X#X#X#X#X#X#X#X#X .
# #
X . . . . . . . . . . . X#X
# #
X#X . . . . . . . . . . . X
# #
. X#X#X#X#X#X#X#X#X#X#X . X
# #
. . . . . . . . . . . X#X#X
Download shortest_puzzle_benchmark3.txtLanguage: txt
SOLUTION:
X#X#X . . . . . . . . . . .
# #
X . X#X#X#X#X#X#X#X#X#X#X .
# #
X . . . . . . . . . . . X#X
# #
X#X . . . . . . . . . . . X
# #
. X#X X#X X#X X#X E#X#X . X
# # # # # # # # #
. . X#X X#X X#X X#X#X#X X#X
#
. . . . . . . . . . . . X#X
#
X#X . . . . . . . . . . . X
# # #
X X#X X#X X#X X#X X#X S . X
# # # # # # # # # # # #
X . X#X X#X X#X X#X X#X X#X
# #
X . . . . . . . . . . . X#X
# #
X#X . . . . . . . . . . . X
# #
. X#X#X#X#X#X#X#X#X#X#X . X
# #
. . . . . . . . . . . X#X#X