Wonderings of a SAT geek

Tag: glucose

  • Clause glues are a mystery to me

    Note: the work below has been done in collaboration with Vegard Nossum, but the wording and some of the (mis-)conculsions are mine. If you are interested, check out his master thesis, it’s quite incredible Anyone who has ever tried to really understand clause glues in SAT solvers have probably wondered what they really mean. Their […]

  • Propagating binary clauses

    Binary clauses are somewhat special. They are clauses that look like: -v1 or v20 = true-v1 or v21 = true which basically mean: if v1 is TRUE, then both v20 and v21 must be TRUE. We put these clauses into a special datastructure, that looks like this: watchlist[-v1] = v20,v21, … This makes us all […]