Convert a "single-used tile" Bloxorz game, which is a NP-Complete problem [1] into a CNF formula, then use MiniSAT to check whether there exist a path from start node to the goal hole
make
./bloxorz <input map file>
reference: Cellular Automata Method for Generating Random Cave-Like Levels
It adopt cellular automata to generate cave-like structures. First fille the map randomly. The basic rule is, a tile becomes a wall if it was a wall and 4 or more of its eight neighbors were walls, or if it was not a wall and 5 or more neighbors were. Put more succinctly, a tile is a wall if the 3x3 region centered on it contained at least 5 walls
generate map
To randomly generate a MxN map, with p% area being occupied, r1_cutoff, r2_cutoff, r iterations (the more iterations, the less noise), type
cd input
./mapGen M N r1_cutoff r2_cutoff r
1 represents tile, 0 represent boundary, for strat node (2) and end node 3, you need to add them in manual. For example, m1.in.
011110
110311
110111
010111
110111
000211
Test cases
Maps are stores in ./input directory, 1 represents tiles, 2 represents start node, 3 represents goal hole, 0 represents boundaries.
Output results
Results are stored in ./output directory
Example
If it is SAT, it will also print out a possible paths and actions you should adapt
Result of m1.in
map boundary (_m, _n) = (6, 6), size = 26
starting index = (5, 3)
ending index = (1, 3)
nodes size = 78
moves size = 312
unary var size = 2028
===== Begin to solve =====
==============================[MINISAT]===============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Clauses Literals | Clauses Literals Lit/Cl | |
======================================================================
| 6 | 21270 45150 | 3 8 2.7 | 0.000 % |
======================================================================
SAT
state U_5_3_S_0
step 0 : UP
state U_5_4_Ly_1
step 1 : LEFT
state U_4_4_Ly_2
step 2 : LEFT
state U_3_4_Ly_3
step 3 : LEFT
state U_2_4_Ly_4
step 4 : LEFT
state U_1_4_Ly_5
step 5 : DOWN
state U_1_3_S_6
Total memory usage: 5980
Total time usage: 0.036443 s
[1] Van Der Zanden, Tom C., and Hans L. Bodlaender. "PSPACE-completeness of Bloxorz and of games with 2-buttons." arXiv preprint arXiv:1411.5951 (2014).
[2] Costa, Diogo M. "Computational complexity of games and puzzles." arXiv preprint arXiv:1807.04724 (2018).
[3] Zhou, Neng-Fa. "In pursuit of an efficient SAT encoding for the Hamiltonian cycle problem." International Conference on Principles and Practice of Constraint Programming. Springer, Cham, 2020