# 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 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:

``` 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.