Tag: glues
-
Machine Learning and SAT
I have lately been digging myself into a deep hole with machine learning. While doing that it occurred to me that the SAT community has essentially been trying to imitate some of ML in a somewhat poor way. Let me explain. CryptoMiniSat and clause cleaning strategy selection When CryptoMiniSat won the SAT Race of 2010, […]
-
A note on learnt clauses
Learnt clauses are clauses derived while searching for a solution with a SAT solver in a CNF. They are at the heart of every modern so-called “CDCL” or “Conflict-Driven Clause-Learning” SAT solver. SAT solver writers make a very important difference between learnt and original clauses. In this blog post I’ll talk a little bit about […]
-
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 […]
-
Extended resolution is working!
The subtitle of this post should really say: and I was wrong, again. First, let me explain what I have been wrong about — wrong assumptions are always the most instructive. I have been convinced for the past year that it’s best to have two type of restart and corresponding learnt clause usefulness strategies: the […]