Cost of solving HunterBig goals on 12-core Intel CPU chip

Seconds, sorry.   Like 34,000 seconds.  Longer than your average gaming clock. 

This leads to the topic of my P-Complete post in this Implementation section. There is work being done to parallelize Clingo on GPU. However Kaminski is saying the core algorithm in Clasp is not amenable to GPU-style threads with relatively low dependency between threads, because P-Complete.

There wasn't much talk about complexity in the Coursera course. It is nice to see that we can mechanically reduce a GDL into a Clingo LP, and search for a model (move leading to goal 100), and nice to know that the reduction results in a P-Complete problem. If you wanted to be academic about it, you could then ask what subsets or patterns of GDL usage lead to sub-P-complete problems in LP, and what GDL simplifications such as factoring are not happening in the Clingo solver, and could they be adapted for use inside Clingo, and would that lead to faster solutions in some cases, and so on. There's enough work there for multiple PhD theses in the intersection of GGP, ASP, complexity theory and computational symbolic logic.

I didn't see much talk in Coursera course boards on the complexity of decision procedures in logic sublanguages.   For example, the work of Cantone, Schwartz, Davis and Omodeo in  Computational Logic and Set Theory: Applying Formalized Logic to Analysis, Set Theory for Computing and Computable Set Theory: Volume 1.  Or Decision Procedures: An Algorithmic Point of View by Kroening, Strichman and Bryant.  Or this article by Melven Robert Krom, A decision procedure for a class of formulas of first order predicate calculus.
Which is to say there is a lot of hard-core work in the literature on decidable sublanguages done by somewhat more hard-core logicians, i.e. someone who would subscribe to the Journal of Symbolic Logic as a matter of course.  Somebody might/should bite my head off, but the Stanford Logic Group doesn't really seem to have that kind of pedigree, i.e. training and a chain of thesis advisors and grand-thesis-advisors for the faculty that leads back to people like Stephen Kleene, Alonzo Church, Jacques Herbrand, or more recent names like Dana Scott, Martin Davis, Peter Andrews and Jack Schwartz.  Davis, Andrews, Scott and Kleene were students of Church.  But just because you weren't born there doesn't mean you can't sample the cuisine.