This is somewhat interesting, but some of the terminology is idiosyncratic ("lambda closures") to the point of being downright confusing ("attack vector").
The pre-analysis in the derive-known-plaintext is particularly interesting because it's the key to making this tractable. But pieces are missing... Does anyone understand this well enough to explain what known-plaintext and matrix-match would be? I can't even work out their types with confidence.
OK, I took what I understood the idea of this preprocessing to be and implemented it in Prolog (257 lines including data and comments, maybe 100 lines of "real" code): http://pastebin.com/fLXKRKQ6
Some findings:
- I was wondering why the linked blog post didn't show the results of derive-known-plaintext (what I call "preprocessing"). It turns out, this may be because this forward propagation solves the puzzle completely. There is no need for backtracking search, so there is no need for the whole fancy Screamer framework.
- Since preprocessing solves the problem completely, applying the constraints to its result to "finalize" the solution is instantaneous in Prolog. With Screamer this takes 3 seconds. Screamer doesn't seem to be all that impressive... At least not for this particular problem.
- In the case where there are no initial marks on the board, after preprocessing having marked almost everything, Prolog finds the four possible solutions in 0.037 seconds on my 2015 laptop. Preprocessing takes a second.
Author here again: and thank you Tom for your feedback. I'm not the author of Screamer so am not going to defend it's runtime properties. These were not of interest to me and yes I could recode much of what I did in C++ which I am more familiar with than Prolog. I work in low latency trading, so I am happy to take any challenge from Prolog in C++. Bummer would be that I could not publish my solution. The reason Screamer is in there is to allow the problem to be expressed declaratively in terms of universal quantification. See also
> The reason Screamer is in there is to allow the problem to be expressed declaratively in terms of universal quantification.
Sure, though this particular example doesn't show its strengths very well. Your pre-analysis is so powerful that even in the case where you start with the empty board, any hand-written primitive brute force enumeration technique should be blazingly fast.
> I work in low latency trading, so I am happy to take any challenge from Prolog in C++.
I'm not saying Prolog is always faster than C++ or Common Lisp :-) I guess I'm saying that every embedding of a Prolog-like system in some other language I have seen so far was less powerful, less elegant, and much less performant than Prolog. This is only partly gloating from a Prolog fan. Another part of me would very much like to have better such systems integrated with other languages.
One drawback of Prolog, of course, is that Prolog can be a bit painful to interface with the rest of your application. Unless, of course, you write everything in Prolog...
My suggestion would just be to email the author; his email in the text of the link below and right above "Licensed under the GNU General Public License", but after the word email:
Author here: Ok thank you Tom for your feedback. "Lambda closures" is a term that is ubiquitous in C++, chiefly owing to how closures are implemented in that language. Sorry if that confused non developers. An "attack vector" is any method, approach or means by which a analyst gains an advantage against the security of a system. A more formal definition maybe found here. http://searchsecurity.techtarget.com/definition/attack-vecto... I broadly used the term to denote building up known plaintext ahead of the application of the solver.
The pre-analysis in the derive-known-plaintext is particularly interesting because it's the key to making this tractable. But pieces are missing... Does anyone understand this well enough to explain what known-plaintext and matrix-match would be? I can't even work out their types with confidence.