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 all sub-clause-sets`F'`

of`F`

. (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:

1 2 3 4 |
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:

1 2 3 4 5 6 |
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:

1 2 3 4 |
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:

1 2 3 4 5 6 7 |
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:

1 2 3 4 |
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.