Introducing Autarkies for DQCNF

TL;DR

This paper extends the concept of autarkies from SAT to DQCNF, exploring their theoretical properties, computational complexity, and practical systems for finding autarkies using SAT solvers.

Contribution

It introduces the first generalization of autarkies to DQCNF, analyzes their complexity, and discusses autarky-systems and reduction techniques for practical computation.

Findings

Autarkies for DQCNF are as hard to find as satisfying assignments.

Natural autarky-systems can restrict autarkies to feasible domains.

SAT solvers can be used to find reductions related to autarkies.

Abstract

Autarkies for SAT can be used for theoretical studies, pre-processing and inprocessing. They generalise satisfying assignments by allowing to leave some clauses "untouched" (no variable assigned). We introduce the natural generalisation to DQCNF (dependency-quantified boolean CNF), with the perspective of SAT translations for special cases. Finding an autarky for DQCNF is as hard as finding a satisfying assignment. Fortunately there are (many) natural autarky-systems, which allow restricting the range of autarkies to a more feasible domain, while still maintaining the good general properties of arbitrary autarkies. We discuss what seems the most fundamental autarky systems, and how the related reductions can be found by SAT solvers.

Equations

$$F$$

$$F_0$$

$$F$$

$$F_0$$

Full text

1 Introduction

The theory of autarkies for SAT (in CNF) (see [4] for an overview) is used in the study of unsatisfiability and pre/inprocessing ([8] is an early paper). In this work we introduce basic autarky theory for DQBF (see [3] for QBF). Indeed we concentrate on DQCNF. These formulas allow existential quantifiers with specified dependencies on universal variables, where the matrix is a CNF. An autarky for a CNF $F$ is a partial assignment which satisfies every clause of $F$ containing an assigned variable. Clauses satisfied by some autarky can be removed satisfiability-equivalently. This is generalised to DQCNF by considering partial assignments to existential variables and allowing boolean functions as values (fulfilling the dependencies), where the clauses with assigned variables need now to become tautologies. So we start right with the boolean functions in this semantical perspective, and do not extract them as in [1, 10]. Restricted forms of autarkies yield “autarky systems (see [4, Section 11.11]). We present three autarky systems for DQCNF, namely, $\operatorname{A}_{0}$, $\operatorname{A}_{1}$ and $\operatorname{E}_{1}$ (using “A” to denote universal variables, and “E” for existential variables). The basic autarky-systems $\operatorname{A}_{0}$, $\operatorname{A}_{1}$ allow the boolean functions to essentially depend on [math] resp. $1$ universal variable, while $\operatorname{E}_{1}$ only uses one existential variable (for a single autarky). Consider the example

[TABLE]

Since $\overline{y_{2}}$ is pure, we have the $\operatorname{A}_{0}$-autarky $y_{2}\rightarrow 0$ (removing the third clause). Furthermore we have the $\operatorname{A}_{1}$-autarky $y_{3}\rightarrow x_{1}$, removing the fourth and fifth clauses. Both these autarkies are also $\operatorname{E}_{1}$-autarkies. We obtain the reduction result $\forall x_{1},x_{2},x_{3}\exists y_{1}(x_{1},x_{2}):(y_{1}\vee x_{1})\wedge(\overline{y_{1}}\vee x_{2})$, which is equivalent to the QBF $\forall x_{1},x_{2}\exists y_{1}:(y_{1}\vee x_{1})\wedge(\overline{y_{1}}\vee x_{2})$, which doesn’t allow any further autarky. Such a final result of autarky reduction is called the (unique) lean kernel of the original formula.

2 Confluence of autarky reduction

A DQCNF is called lean if it has no non-trivial autarkies. The union of two lean DQCNF with compatible variables and dependencies is again lean, and thus every DQCNF has a largest lean sub-DQCNF, the lean kernel. We denote the lean kernel by $\boldmath{\operatorname{\operatorname{N}_{a}}(F)}$ (“N” like “normal form”). Alternatively one can arrive at the lean kernel via autarky reduction. For an autarky $\varphi$ of a DQCNF we denote by $\varphi*F$ the DQCNF with the clauses removed which are satisfied by $\varphi$.

Lemma 1

$\varphi*F$* is satisfiability-equivalent to $F$ for an autarky $\varphi$ of $F$.*

For two autarkies $\varphi,\psi$ of $F$ one can consider the composition $\varphi\circ\psi$, which on the variables of $\psi$ acts like $\psi$, and otherwise like $\varphi$:

Lemma 2

The composition of two autarkies is again an autarky.

Now the lean kernel is obtained by repeatedly applying autarky-reduction on $F$ as long as possible:

Lemma 3

Consider a DQCNF $F$. The largest lean sub-DQCNF $\operatorname{\operatorname{N}_{a}}(F)$ is also obtained by applying autarky-reduction to $F$ as long as possible (in any order).

Due to the high complexity of general autarky-finding for DQCNF, it is vital to allow restricted notions of autarkies (with lower complexity). For that purpose we generalise the notion of “autarky systems” from [4, Section 11.11]. For a DQCNF $F$ we write $\operatorname{Auk}(F)$ for the set of all autarkies. An autarky system $\mathcal{A}$ allows to consider subsets $\mathcal{A}(F)\subseteq\operatorname{Auk}(F)$. There are two basic conditions which make $\mathcal{A}$ an autarky system. First for DQCNFs $F$ and $\varphi,\psi\in\mathcal{A}(F)$ it must always hold $\varphi\circ\psi\in\mathcal{A}(F)$ (closure under composition). And second for DQCNFs $F\subseteq F^{\prime}$ it must always hold $\mathcal{A}(F^{\prime})\subseteq\mathcal{A}(F)$ (removal of clauses does not remove $\mathcal{A}$-autarkies). $\mathcal{A}$-satisfiability means satisfiability by a series of $\mathcal{A}$-autarkies, while $\mathcal{A}$-leanness means there there are no nontrivial $\mathcal{A}$-autarkies. To have Lemma 3 (and further natural properties) the following four conditions on $\mathcal{A}$ are fundamental:

standardised

variables not actually occurring are irrelevant.

$\bot$-invariant

universal clauses (only having universal variables) are irrelevant.

invariant under variable elimination

removing (existential) variables from the clauses does not affect autarkies of $\mathcal{A}$ which do not use these variables.

invariant under renaming

renaming variables (existential or universal) is respected by the autarky system.

These four conditions are always expected to hold. Additionally we call $\mathcal{A}$ iterative, if we have that if we apply any autarky of $\mathcal{A}$, and take another autarky of $\mathcal{A}$ for the reduction result, then their composition also belongs to $\mathcal{A}$ (for the original DQCNF). For iterative systems every result from autarky reductions can also be obtained by applying a single autarky from the system. Autarky systems fulfilling all five conditions are called normal.

3 A- and E-systems

Consider a DQCNF $F$ and $k\geq 0$:

• •

An $\operatorname{A}_{k}$-autarky for $F$ is an autarky such that all boolean functions assigned depend essentially on at most $k$ variables.

• •

An $\operatorname{E}_{k}$-autarky is an autarky assigns at most $k$ (existential) variables.

$\operatorname{A}_{0}$ is just CNF-autarky, and we concentrate on $\operatorname{A}_{1}$. Generalising [5] one sees that all satisfiable DQ2CNF are satisfiable by an $\operatorname{A}_{1}$-assignment. The composition $\mathcal{E}_{1}+\mathcal{A}_{1}$ one might consider as the basic “clean-up autarky system”.

Since the existence of an ordinary propositional autarky for a clause-set $F$ is NP-complete (see [7]), which is covered by $\operatorname{A}_{0}$-autarkies, deciding whether a DQCNF has a non-trivial $\operatorname{A}_{k}$-autarky is NP-complete for every $k\geq 0$ (boolean functions can be just represented by truth-tables here). Deciding the existence and finding some short $\operatorname{E}_{1}$-autarky can be done in polynomial time (discussed below). The $\operatorname{A}_{k}$-systems are all normal, while the $\operatorname{E}_{k}$ fulfil the basic conditions, but are not iterative for $k\geq 1$.

3.1 $\operatorname{E}_{1}$-autarkies

Consider any DQCNF $F$ and a set $V$ of existential variables. Let the DQCNF $F[V]$ be obtained by restriction to $V$, removing all clauses not containing some variable from $V$, and removing from the remaining clauses all existential literals with variables not from $V$. The existence of any autarky $\varphi$ with given var-set $\operatorname{var}(\varphi)=V$ is equivalent to the DQCNF $F[V]$ being satisfiable, where the satisfying assignments correspond directly to the autarkies.

So searching for an $\operatorname{E}_{1}$-autarky of $F$ can be done by solving for each $v$ the one-existential-variable DQCNF $F[\{v\}]$. This can be done easily, since in general from any clause $C$ we can remove universal literals with variables not in any domain of some existential variable of $C$. So we have a QCNF with prefix $\forall\exists$ and with exactly one existential variable to solve. It is easy to see that the solution-set for $v$ is an interval $A\rightarrow v\rightarrow B$, which can be read off from the positive resp. the negative occurrences of $v$ (as DNF resp. CNF), and where choosing for $v$ either $A$ or $B$ yields easy solutions. We note here that for $\operatorname{E}_{2}$ we do not get a QCNF with two existential variables, but only such a DQCNF.

3.2 $\operatorname{A}_{1}$-autarkies

The main strategy to solve the constraint-satisfaction problem of finding some non-trivial $\operatorname{A}_{1}$-autarky for a given $F$ is: 1. to explicitly list the possible boolean functions as values of the existential variables, 2. to compile for each clause $C\in F$ the minimal possibilities for $C$ to become a tautology, and 3. to make it explicitly part of the SAT-translation that at least one of these minimal possibilities for $C$ is fulfilled, if the selector-variable of $C$ is true (non-triviality of the autarky means that at least one selector-variable is true). For an existential variable $v$ with dependency-set $D(v)$ we thus have $2\lvert D(v)\rvert+2$ possible values to consider, the two constant boolean functions plus for each universal variable the two associated literals. And there are exactly three types of minimal possibilities for $C$ to become a tautology:

some existential $y\in C$ is set to $1$; 2. 2.

for some existential $y\in C$ there is a universal $x\in C$ with $\operatorname{var}(x)\in D(\operatorname{var}(y))$, and $y$ is set to $\overline{x}$; 3. 3.

for some existential $y,y^{\prime}\in C$, $y\neq y^{\prime}$, there is a universal $x\in D(\operatorname{var}(y))$, and $y$ is set to $x$ and $y^{\prime}$ to $\overline{x}$.

The translation into a SAT-problem is now in principle not difficult, but effort is needed for the representation of AMO-constraints (at-most-one), and for encodings of nonboolean values (direct or logarithmic encodings).

Obviously the strength of $\operatorname{E}_{1}$ and $\operatorname{A}_{1}$ in general is incomparable. On the formula in the Introduction indeed the $\operatorname{E}_{1}$-lean kernel is the same as the $\operatorname{A}_{1}$-lean kernel, namely the (absolute) lean kernel. But for example for the following formula they produce different normalforms:

[TABLE]

First consider $\operatorname{E}_{1}$. Variable $y_{1}$ does not yield something, since not pure. While variable $y_{2}$ alone can only be set to true or $\overline{x_{1}}$, due to the second clause, while due to the first and third clause this does not yield an autarky. So $F$ is $\operatorname{E}_{1}$-lean. But this formula is $\operatorname{A}_{1}$-satisfiable with assignment $y_{1}\mapsto 1$ and $y_{2}\mapsto\overline{x_{1}}$. For the opposite consider $\forall\,x_{1},x_{2}\exists y:y\leftrightarrow x_{1}\vee x_{2}$, which is $\operatorname{E}_{1}$-satisfiable, but $\operatorname{A}_{1}$-lean.

With improved SAT-encodings and running standard SAT-solvers, we where able to compute the normalforms quite easily for all over 334 instances in the DQBF track of QBFEVAL’18 ([9]).

4 Conclusion

We consider $\operatorname{E}_{1}+\operatorname{A}_{1}$ only as a first example and appetiser — all the SAT-theory on autarkies can be combined with many interesting classes of boolean functions, to yield interesting autarky systems. The results on the normalforms by the basic autarky systems $\operatorname{A}_{0},\operatorname{A}_{1},\operatorname{E}_{1}$ and their combinations, on all known QCNF and DQCNF instances (as in QBFLIB), will be made available online. After establishing this precise basis, the use of autarkies in pre- and inprocessing is the main question. Theoretical studies of lean DQCNF (see [6] for using $\operatorname{A}_{0}$ for QBF) should also be very interesting.