Wonderings of a SAT geek

Tag: transitive reduction

  • 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 […]

  • 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 […]