I think Day 12 Part 1 and Part 2 are essentially the same, it’s just that Part 2 is much much bigger in a way that forces a different set of solutions.
When I read the problem, I knew I would solve it differently than previous days - instead of throwing the entire problem input at Dusa as one big JSON blob, I was going to throw each line to Dusa separately. I would represent the inputs as a series of facts char N is "#", or char N is ".", or char N is "?", and also capture the number of characters (length is L) and the expected runs as a structured list, so 1,1,3 becomes (cons 1 (cons 1 (cons 3 nil))).
Dusa is supposed to be able to make choices, though I haven’t used that functionality extensively in any previous Advent of Code days. But we can say that the value of a “?” character is exactly one of # or . like this:
**value N is "#" :- char N is "#".
value N is "." :- char N is ".".
value N is { "#", "." } :- char N is "?".**
…and then we can use constraints to check that the solution we randomly guessed was correct, and invalidate the solution if it doesn’t match the expected runs.
Then, the answer for a given line is the number of solutions Dusa generates, rather than having Dusa directly give us the answer within the program. I was excited about this because we’re really interested in the answer sets — the set of all solutions given our rules and constraints.
Here’s the program at dusa.rocks).%0A%0A%0A%0A%0A%0A%0A)
Here’s the program at val.town
I think solution 1 might have worked for Part 1 if I’d solved an unrelated bug. Slowly, but possibly.
The problem with that solution is that Dusa isn’t a very good SAT solver — it’s not something I’ve tried to optimize. So the solver would do silly things like, if there were no runs of length 4 and the end of the string was .###?, it would sometimes guess as its very first guess that that question mark was a #, and then would have to make a bunch of other useless guesses before it realized this was a bad idea. So I added a bunch of other ad-hoc things to try to make solutions get invalidated earlier (invalidation if there are more hashes than possible given the input, invalidation if there are more dots than possible given the input, invalidation partially-completed runs longer than any runs in the input, etc). This extra invalidation logic sped stuff up some, but not, like, an order of magnitude improvement or anything.
But the solution that worked to solve Part 1 with satisfying speed was to process the string from left to right, and only allow Dusa to make a choice about whether a ? was a # or a . if that was position Dusa was looking at.
Here’s the program at dusa.rocks%2C%20value%20N%20is%20%22%23%22.%0Avalue%20N%20is%20%7B%20%22.%22%2C%20%22%23%22%20%7D%20%3A-%0A%20%20%20%20process%20notInRun%20N%20(cons%20Len%20RunList)%2C%20char%20N%20is%20%22%3F%22.%0A%0Aprocess%20notInRun%20(s%20N)%20RunList%20%3A-%0A%20%20%20%20process%20(inRun%200)%20N%20RunList%2C%20char%20N%20is%20_.%0Avalue%20N%20is%20%22.%22%20%3A-%0A%20%20%20%20process%20(inRun%200)%20N%20RunList%2C%20char%20N%20is%20_.%0A%0Aprocess%20(inRun%20Len)%20(s%20N)%20RunList%20%3A-%0A%20%20%20%20process%20(inRun%20(s%20Len))%20N%20RunList%2C%20char%20N%20is%20_.%0Avalue%20N%20is%20%22%23%22%20%3A-%0A%20%20%20%20process%20(inRun%20(s%20Len))%20N%20RunList%2C%20char%20N%20is%20_.%0A%0A%23forbid%20length%20is%20Len%2C%20process%20_%20Len%20(cons%20_%20_).%0A%23forbid%20length%20is%20Len%2C%20process%20(inRun%20(s%20_))%20Len%20_.%0A%0A%0Aresult%200%20is%20%22%22.%0Aresult%20(s%20N)%20is%20(concat%20Accum%20Ch)%20%3A-%0A%20%20result%20N%20is%20Accum%2C%0A%20%20value%20N%20is%20Ch.%0Aresolution%20is%20Str%20%3A-%20length%20is%20Len%2C%20result%20Len%20is%20Str.%0A%0A%0Achar%200%20is%20%22%3F%22.%0Achar%201%20is%20%22%23%22.%0Achar%202%20is%20%22%23%22.%0Achar%203%20is%20%22%23%22.%0Achar%204%20is%20%22%3F%22.%0Achar%205%20is%20%22%3F%22.%0Achar%206%20is%20%22%3F%22.%0Achar%207%20is%20%22%3F%22.%0Achar%208%20is%20%22%3F%22.%0Achar%209%20is%20%22%3F%22.%0Achar%2010%20is%20%22%3F%22.%0Achar%2011%20is%20%22%3F%22.%0Alength%20is%2012.%0Aruns%20is%20(cons%203%20(cons%202%20(cons%201%20nil))).%0A%0A%0A%0A)
Of course, this approach immediately fell on its face for Part 2, which I think just about requires a dynamic programming solution.
This was incredibly annoying. In this section, I’m going to describe the solution I was writing in my head, and then say a little bit about how I painfully program-transformed it into a program that Dusa could run.
The program I wanted to write was a backward-chaining logic program (with memoization), which is a thing that exists and this solution could probably be ported straightforwardly to a system that supports it.
Backward-chaining logic programming is based on a query. Our query will be: for the sequence of springs starting at position 0, which is of course not in the middle of a run of successive #s, how many ways are there of resolving the input list (say, 1,1,3). That query is represented by this proposition, where we know everything to the left of the is but not about what’s to the right of the is