Tag: hyper-binary resolution
-
TreeLook and transitive reduction
The paper by Heule et al. about hyper-binary resolution using intree-based lookahead is pretty funky. The idea is actually quite simple (and as usual, not exactly trivial to come up with): we re-use past propagations by reversing the order in which literals are normally enqueued. A simple example First, a queue is built that starts […]
-
Certified UNSAT and CryptoMiniSat
Marijn Heule kindly sent me an email on the 10th of April about DRUP, the new system used this year in the SAT Competition’13 for the UNSAT track. He kindly encouraged me to implement the DRUP system. He personally implemented it into Minisat which was a very helpful lead for me. In this post I […]
-
On hyper-binary resolution
Hyper-binary resolution is actually quite straightforward, or at least appears to be. Let’s take the following example. The clauses in our database are the following: -a V b -a V c -b V -c V g -b V -c V d -d V g Let’s set a to true, and see what happens. Immediately, b […]
-
Visiting Linz
I had the pleasure of visiting Linz, the workplace of Armin Biere, one of the leading SAT experts, and the creator of PrecoSat and lingeling award-winning SAT solvers. In Linz, I had the pleasure to listen to Armin Biere’s exposé on lingeling’s datastructures, and I also gave a small talk on SAT solver architectures.
-
Hyper-binary resolution: I was wrong, again
I am not perfect, so I make mistakes. One of the more memorable mistakes I have made has been regarding hyper-binary resolution. More specifically, in this post I wrote that I cannot add as many binary clauses using hyper-binary resolution as Armin Biere, one of the leading SAT solver experts, and I proposed a reason […]