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
phiis called a weak autarky forFif “phi*Fis a subset ofF” holds, whilephiis an autarky forFifphiis a weak autarky for all sub-clause-setsF'ofF. (Handbook of Satisfiability, p. 355)
What does this mean? Well, it means that in the clause-set {x V y, x} the assignment y=False is a weak autarky, because assigning y to False will lead to a clause that is already in the clause set (the clause x), while the assignment of x=True is a (normal) autarky, because it will satisfy all clauses that x is in. The point of autarkies is that we can remove clauses from the clause set by assigning values to a set of variables, while not changing the (un)satisfiability property of the original problem. In other words, autarkies are a cheap way of reducing the problem size. The only problem is that it seems to be relatively expensive to search for them, so conflict-driven SAT solvers don’t normally search for them (but, some lookahead solvers such as march by Marijn Heule do).
So, what is the idea? Well, I think we can have autarkies for equivalent literals, too. Here is an example CNF:
a V d V -f
-b V d V -f
-a V e
b V e
setting a = -b will not change the satisfiability of the problem.
We can add any number of clause pairs of the form X V Y where Y is any set of literals not in {a, -a, b, -b}, and X is (-)a in clause 1 and (-)b in clause 2. Further, one of the two variables, say, a can be in any clauses at will (in any literal form), though variable b can then only be in clauses defined by the clause pairs. Example:
a V d V -f
-b V d V -f
-a V e
b V e
a V c V -h
a V -f
An extension that is pretty simple from here, is that we can even have clauses whose Y part is somewhat different: some literals can be missing, though again in a controlled way. For example:
a V d
-b V d V -f
-a V e
b V e
is possible. It would restrict b a bit more than necessary, but if a is the only one of the pairs missing literals, we are still OK I believe.
Finally, let me give an example of what these higher-level autarkies are capable of. Let’s assume we have the clause set:
a V d
-b V d V -f
-a V e
b V e
a V c V -h
a V -f
a V b V f V -g
setting a=-b now simplifies this to:
a V d
-a V e
a V c V -h
a V -f
which is equisatisfiable to the first one. Further, if the latter is satisfiable, computing the satisfying solution to the former given a solution to the latter is trivial.
