Tag: simplification
-
Why it’s hard to eliminate variables
Let’s examine why it’s hard to eliminate variables. I remember the code I looked at in SatElite that did it: it was crazy clean code and looked like it was pretty easy to perform. In this post I’ll examine how that simple code became more than a 1’000 lines of code today. What needs to […]
-
On benchmark randomization
As many of you have heard, the SAT Competition for this year has been announced. You can send in your benchmarks between the 12th and the 22nd of April, so get started. I have a bunch of benchmarks I have already submitted about 2 years ago, still waiting for any reply from those organizers — […]
-
Note to self: higher level autarkies
While reading this thesis, I have had a thought about autarkies. Let me first define what an autarky in SAT solving is: A partial assignment phi is called a weak autarky for F if “phi*F is a subset of F” holds, while phi is an autarky for F if phi is a weak autarky for […]
-
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 […]