The problem of out-competing the SAT solver with MultiwayDeletionsGraph apparently took me about 3-4 hours to knock out. Here are the results, starting with the SAT solver benchmark:

And here are the results from MultiwayDeletionsGraph:

Again, the MDG times are an order of magnitude faster and we get the same results in terms of cardinality for completed atlases $2\times 2$ or $3 \times 3$. However, in this case it was necessary to impose a fairly strict order which would cause the MDG to be a tree rather than a DAG. Especially for the $3 \times 3$ case it makes no sense to place a next tile unless it is adjacent to one of the previous tiles.