Tag: subsumption

  • Implicit binary clauses

    I have lately been trying to get CryptoMiniSat to use implicit binary clauses. The idea is that since binary clauses are very trivial (just two literals), and they don’t really need to keep state (like clause activity), they don’t really need to be stored at a separate location. Instead, they can be stored directly in […]

  • On-the-fly self-subsuming resolution

    I have recently been trying a new method of shortening learnt clauses. There is a learnt clause minimisation paper by Sörensson and Biere, and I have recently been trying to do more. The trick I use, is that many literals can be removed from learnt clauses, if self-subsuming resolution (see my older post) is applied […]

  • Self-subsuming resolution

    Self-subsuming resolution in SAT uses the resolution operator to carry out its magic. Resolution can be used on two clauses if they share a variable, but the sign of the variable is inverted, e.g.v1 V v2-v1 V v3 V v4(where v1..v4 are binary variables and “V” means binary OR) can be resolved on v1, producing […]