figure a

1 Introduction

Given a Boolean formula \(\exists Y\mathpunct {.}\varphi \) with free variables X, quantifier elimination (also called projection) is the problem to find a formula \(\psi \equiv \exists Y\mathpunct {.}\varphi \) that only contains variables X. Closely related, the functional synthesis problem is to find a function \(f_y:2^X\rightarrow \mathbb {B}\) for all \(y\in Y\), such that \(\varphi [Y \mapsto f_y(X)]\equiv \exists Y\mathpunct {.}\varphi \).

Quantifier elimination and functional synthesis are fundamental operations in automated reasoning, computer-aided design, and verification. Hence, progress in algorithms for these problems benefits a broad range of applications of formal methods. For example, typical algorithms for reactive synthesis reduce to computing the safe region of a safety game through repeated quantifier eliminations [1,2,3] or directly employ functional synthesis [4]. Until today, algorithms for quantifier elimination often involve (reduced ordered) Binary Decision Diagrams (BDDs) [5]. However, BDDs often grow exponentially for applications in verification, and extracting formulas (or strategies, etc.) from BDDs typically results in huge expressions. The search for alternatives resulted in CEGAR-style algorithms [6,7,8,9,10].

In this work, we take look at the closely related field of QBF solving. There pure CEGAR solving [11,12,13] on the CNF representation is not competitive anymore [14], and it has been augmented by preprocessing [15, 16], circuit representations [17,18,19,20,21], and Incremental Determinization (ID) [22]. It may hence be fruitful to leverage some of the recent developments of QBF.

The contribution of this work is a simple modification of ID to enable quantifier elimination and functional synthesis. Incremental Determinization (ID) is an algorithm for solving quantified Boolean formulas of the shape \(\forall X\mathpunct {.}\exists Y\mathpunct {.}\varphi \), where \(\varphi \) is a propositional formula in conjunctive normal form (CNF), i.e. 2QBF. It follows a proof-theoretic approach, very similar to a SAT solver, alternating between building a model (i.e. Skolem functions for the existential variables Y) and a refutation proof [23]. This allows ID to provide a model (i.e. a Skolem function) when it determines that a formula is true, which sets it apart from other QBF algorithms.

The modification of ID to enable quantifier elimination for a given formula \(\exists Y\mathpunct {.}\varphi \) is very simple: We run ID on the formula as if it was a quantified Boolean formula \(\forall X\mathpunct {.}\exists Y\mathpunct {.}\varphi \), where X are the free variables, but add \(\varphi \) to the conflict check within ID. This suppresses the UNSAT result in the ID algorithm and it is hence forced to terminate with a model (that is, a function), which is guaranteed to satisfy the functional synthesis requirements. Quantifier elimination is then only a substitution away.

Our experimental evaluation shows that ID significantly outperforms previous algorithms for functional synthesis and quantifier elimination.

This paper is structured as follows: We review related work in Sect. 2 and introduce standard notation in Sect. 3. In Sect. 4 we first review the Incremental Determinization algorithm before introducing the change necessary to lift it to functional synthesis. The experimental evaluation is in Sect. 5. We summarize the current state of the tool CADET in Sect. 6 and conclude the paper in Sect. 7.

2 Related Work

Functional Synthesis. Early works on functional synthesis tried to exploit Craig interpolation, but did not scale well enough [24]. This was followed by first attempts to use CEGAR [6], which failed, however, to surpass the performance of BDDs [7]. More recent works revisited the use of BDDs, e.g. the tools SSyft [25] and RSynth [26, 27]. This motivated the search for alternatives to BDDs [8,9,10]. At their core, these new algorithms all rely on counter-example guided abstraction refinement (CEGAR) [28], but they apply it in clever, compositional ways. However, they still inherit the well-known weaknesses of CEGAR (as, for example, discussed in the QBF literature): For the simple formula \(\varphi = \bigwedge _{i<n} x_i\leftrightarrow y_i\), where \(n=|X|=|Y|\) and \(x_i\in X\) and \(y_i\in Y\), CEGAR needs to browse through \(2^n\) satisfying assignments just to recover that the function we were looking for is \(f(x)=x\).

The Back-and-Forth algorithm explores stronger abstraction using MaxSAT solvers as a means to reduce the number of assignments that CEGAR needs to explore [8]. ParSyn attempts to combat the problem with parallel compute power and a compositional approach [9]. This compositional approach has later been refined using a wDNNF decomposition [10].

QBF Certification. Some solvers and preprocessors for QBF have the ability to not only provide a yes/no answer, but also produce a certificate (i.e. Skolem functions) for their result [13, 22, 29, 30]. While most QBF approaches suffer heavy performance penalties when asked to provide a certificate, Incremental Determinization naturally computes Skolem functions that can be extracted easily from the final state [22].

3 Preliminaries

Boolean formulas over a finite set of variables \(x\in X\) with domain \(\mathbb {B} = \{\mathbf {0},\mathbf {1}\}\) are generated by the following grammar:

$$\begin{aligned} \varphi := \mathbf {0}\mid \mathbf {1}\mid x \mid \lnot \varphi \mid (\varphi ) \mid \varphi \vee \varphi \mid \varphi \wedge \varphi \end{aligned}$$

Other logical operations, such as implication, XOR, and equality, are considered syntactic sugar with the usual definitions.

An assignment \(\mathbf {x}\) to a set of variables X is a function \(\mathbf {x} : X \rightarrow \mathbb B\) that maps each variable \(x \in X\) to either \(\mathbf {1}\) or \(\mathbf {0}\). We denote the space of assignments to some set of variables X with \(2^X\).

Given formulas \(\varphi \) and \(\varphi '\), and a variable x, we denote the substitution of x by \(\varphi '\) in \(\varphi \) as \(\varphi [x\rightarrow \varphi ']\). We lift substitutions to sets of variables \(\varphi [X\mapsto t_x]\) when \(t_x\) maps each \(x\in X\) to a formula \(\varphi '\).

A literal l is either a variable \(x \in X\), or its negation \(\lnot x\). We use \(\overline{l}\) to denote the literal that is the logical negation of l. A disjunction of literals \((l_1 \vee \ldots \vee l_n)\) is called a clause and their conjunction \((l_1 \wedge \ldots \wedge l_n)\) is called a cube. We denote the variable of a literal by \( var (l)\) and lift the notion to clauses \( var (l_1\vee \dots \vee l_n) = \{ var (l_1),\dots , var (l_n)\}\).

A formula is in conjunctive normal form (CNF), if it is a conjunction of clauses. Throughout this exposition, we assume that the input formula is given in CNF. (The output, however, can be a non-CNF formula.) It is trivial to lift the approach to general Boolean formulas: Given a Boolean formula \(\varphi \) over variables X, the Tseitin transformation provides us a formula \(\psi \) with \(\varphi \equiv \exists Z.\psi \), where Z are fresh variables [31]. Note that eliminating a group of variables \(X'\subseteq X\) in \(\varphi \) is then the same as eliminating \(X'\cup Z\) in \(\psi \).

Resolution is a well-known proof rule that allows us to merge two clauses as follows. Given two clauses \(C_1\vee v\) and \(C_2\vee \lnot v\), we call \(C_1\otimes _v C_2 = C_1\vee C_2\) their resolvent with pivot v. The resolution rule states that \(C_1\vee v\) and \(C_2 \vee \lnot v\) imply their resolvent. Resolution is refutationally complete for Boolean formulas in CNF, i.e. given a formula in CNF that is equivalent to false, we can derive the empty clause using only resolution.

4 Lifting Incremental Determinization

In the sequel, we formally define functional synthesis, review the working principle of Incremental Determinization for 2QBF, discuss how the solver state corresponds to functions, and then introduce the modification to Incremental Determinization to turn it into an algorithm for functional synthesis. The functional synthesis problem is to find a function \(f_y:2^X\rightarrow \mathbb {B}\) for all \(y\in Y\), such that \(\varphi [Y\mapsto f_y(X)]\equiv \exists Y\mathpunct {.}\varphi \). Functional synthesis is closely related to solving 2QBF: Given a true 2QBF problem \(\forall X\mathpunct {.}\exists Y\mathpunct {.}\varphi \), any Skolem function that is a model for the formula is also a solution to the functional synthesis problem for variable sets X and Y. Only for false 2QBF there is a difference between the problems: if there is an assignment \(\mathbf {x}\) to X for which there is no assignment to Y, the 2QBF cannot be proven with a Skolem function, but the functional synthesis problem still requires us to produce a function f. It is clear that for input \(\mathbf {x}\) the f can produce any output. We will exploit this similarity between 2QBF and functional synthesis in the following to lift the Incremental Determinization algorithm to functional synthesis.

4.1 Working Principle of Incremental Determinization for 2QBF

ID was originally introduced as an algorithm for 2QBF, the fragment of quantified Boolean formulas with at most one quantifier alternation. Given a formula \(\forall X\mathpunct {.}\exists Y\mathpunct {.}\varphi \), ID alternates between constructing a model (i.e. a Skolem function) to prove the formula correct, and constructing a Q-resolution proof to refute the formula [32]. During model construction, ID identifies which variables in Y have unique Skolem functions considering the current set of clauses. When all variables with unique Skolem functions are identified, ID greedily introduces additional clauses to reduce the space of possible Skolem functions, such that the remaining variables may get unique Skolem functions, too. Whenever the model construction ends up in a dead-end (=conflict), ID switches to constructing a refutation proof [32] and derives clauses using resolution. As soon as ID found a clause that prevents the model construction from trying the same partial model again, it switches back to the model search. Since there are only finitely many clauses and models, either the model construction or the refutation proof must eventually finish [22, 23].

Example 1

We will use the following formula as a running example:

$$ \begin{array}{rl} \forall x_1, x_2\mathpunct {.}\exists y_1, y_2, y_3\mathpunct {.}&{} (x_1\vee \lnot y_1)\wedge (\lnot x_1 \vee y_1)~\wedge \\ &{} (y_1 \vee \lnot y_2)\wedge (\lnot y_1 \vee \lnot x_2 \vee y_2)~\wedge \\ &{} (\lnot y_1 \vee y_3) \wedge (y_2 \vee \lnot y_3) \wedge (x_2 \vee \lnot y_3) \end{array} $$

Looking at the first two clauses it is clear that \(y_1\) is uniquely determined by \(x_1\) and \(y_1\)’s Skolem function must be \(f_{y_1}(X)=x_1\). For this step, we intentionally ignore all clauses of \(y_1\) that contain \(y_2\) and \(y_3\), as they do not yet have a Skolem function and we have to consider them as undefined. The other clauses containing \(y_1\) will only become relevant when looking for Skolem functions for \(y_2\) and \(y_3\).

Variables \(y_2\) and \(y_3\) do not have unique Skolem functions in the formula above. ID would now greedily add a decision clause, such as \((x_2\vee \lnot y_2)\), to also make the Skolem function for \(y_2\) unique. The added clause, plus clauses 3 and 4 in the formula define: \(f_{y_2}(X)=f_{y_1}(X)\wedge x_2\).

This results in the situation that there is no Skolem function for \(y_3\): For the assignment \(x_1\mapsto \mathbf {1},~x_2\mapsto \mathbf {0}\), the functions for \(y_1\) and \(y_2\) assign \(y_1\mapsto \mathbf {1},~y_2\mapsto \mathbf {0}\). Then clauses 4 and 5 cannot be satisfied both by \(y_3\), which means there is a conflict for this assignment to the universals. During conflict analysis, ID would now resolve clauses 5 and 6 to obtain clause \((\lnot y_1 \vee y_2)\), and then backtrack to the point before introducing the decision clause.   \(\lhd \)

4.2 Representation of Functions

What is particularly interesting about ID is its ability to produce Skolem functions when it has proven a formula correct. Other than previous QBF algorithms, these Skolem functions are produced without any overhead.

ID avoids costly representations of Skolem functions: It maintains a set \(D\subseteq Y\) of variables that have a unique Skolem function, and its state includes a formula \(\delta \) characterizing the input-output behavior of the Skolem functions for variables D. Formula \(\delta \) satisfies \(\forall X\mathpunct {.}\exists !D\mathpunct {.}\delta \), where \(\exists !D\) means that there exists exactly one assignment to D. We can thus think of \(\delta \) also as a function \(f_{\delta }\) mapping X assignments to D assignments.

Example 2

Back to our running example. After identifying a unique Skolem function for \(y_1\), formula \(\delta \) consists exactly of the first two clauses of the formula, \((x_1\vee \lnot y_1) \wedge (\lnot x_1 \vee y_1)\). After adding the decision clause and identifying a unique Skolem function for \(y_2\), \(\delta \) consists exactly of the first four clauses and the decision clause.   \(\lhd \)

4.3 Conflict Checks in ID

The formulas representing functions have primarily one purpose: to check for the existence of conflicts. Whenever we attempt to grow the set D by a variable v, we need to check whether v has a unique Skolem function. This check consists of two parts; given an arbitrary universal assignment \(\mathbf {x}\in 2^X\),

  1. (1)

    is there at most one legal assignment to v, and

  2. (2)

    is there at least one legal assignment to v?

To formally define this, let us consider the clauses \((d_1\vee \dots \vee d_n\vee l)\) in \(\varphi \) that contain a literal l of variable v and otherwise only contain literals \(d_i\) of variables in D and X. We call these the clauses with unique consequence, as they can be read as implications \((\lnot d_1\wedge \dots \wedge \lnot d_n\Rightarrow l)\), and we call \(\lnot d_1\wedge \dots \wedge \lnot d_n\) the antecedent of that clause. Further, we define \(\mathcal A_l\) as the disjunction over all antecedents of literal l. (Note that \(\mathcal A_l\) depends on D and therefore changes as the state of the solver progresses.)

The two checks from above can now be defined as follows:

  1. (1)

    \(\exists X\mathpunct {.}\delta \wedge \lnot \mathcal A_v \wedge \lnot \mathcal A_{\lnot v}\)

  2. (2)

    \(\exists X\mathpunct {.}\delta \wedge ~~ \mathcal A_v \wedge ~~ \mathcal A_{\lnot v}\)

Checking for case (1) can be efficiently approximated [22], but checking for case (2) cannot easily be avoided. We thus query a SAT solver with \(\delta \wedge \mathcal A_v \wedge \mathcal A_{\lnot v}\) to perform a conflict check.

Example 3

We revisit the conflict described in Example 1. The starting point is the situation when \(D=\{y_1,y_2\}\) and \(\delta \) consists of the first four clauses of the formula as well as the decision clause \((x_2\vee \lnot y_2)\). The antecedents of \(y_3\) are \(\mathcal A_{y_3}=y_1\) and \(\mathcal A_{\lnot y_3}=\lnot y_2 \vee \lnot x_2\). It is easy to verify that the universal assignment \(x_1\mapsto \mathbf {1},~x_2\mapsto \mathbf {0},y_1\mapsto \mathbf {1},~y_2\mapsto \mathbf {0}\) satisfies the conflict criterion \(\delta \wedge \mathcal A_v \wedge \mathcal A_{\lnot v}\).   \(\lhd \)

4.4 Functional Synthesis

Remember that in the case of functional synthesis for \(\varphi \) over sets of variables X and Y, we search for a function \(f:2^X\rightarrow 2^Y\) such that f produces a satisfying assignment whenever it can, but can produce anything when there is no assignment to Y satisfying the formula. In case there are satisfying assignments to Y for all X, we can simply run ID as if it was a QBF \(\forall X\mathpunct {.}\exists \mathpunct {.}\varphi \) to obtain a Skolem function that also satisfies the functional synthesis criterion. In the other case, that there is an X for which there is no assignment to Y satisfying \(\varphi \), ID for 2QBF would eventually detect a conflict that did not depend on a decision and return with UNSAT.

In order to lift ID to functional synthesis, we want to ignore universal assignments that have no satisfying assignment to Y. A simple way to suppress these conflicts is to add \(\varphi \) to the conflict check. In order for an assignment to X to remain a conflict, we must now additionally find an assignment to Y that demonstrates that the conflict could be prevented by a different decision.

All other parts of ID, including the extraction of functions, remain untouched. In particular, termination is still guaranteed, as the greedy model construction either results in a function for all variables in Y or in a conflict, upon which at least one model is excluded through resolution.

Example 4

For the conflict in our running example, the universal assignment \(x_1\mapsto \mathbf {1},~x_2\mapsto \mathbf {0}\) is excluded in the modified conflict check. Consider the UNSAT core consisting of clauses 2, 5, and 7 for that universal assignment: propagate \(y_1\mapsto \mathbf {1}\) using clause 2; propagate \(y_3\mapsto \mathbf {1}\) using clause 5; and finally propagate \(y_3\mapsto \mathbf {0}\) using clause 7. So, instead of going into conflict analysis and backtracking, ID for functional synthesis concludes that it has found a function for all existential variables and terminates.

4.5 Quantifier Elimination

Given a formula \(\exists Y\mathpunct {.}\varphi \) with free variables X, quantifier elimination is the problem to find a formula \(\psi \equiv \exists Y\mathpunct {.}\varphi \) over variables X only. Hence, given a solution f to the functional synthesis problem for \(\varphi \), we only have to substitute Y by f in \(\varphi \) to obtain the projected formula.

5 Experimental Evaluation

We implemented the modifications to ID in CADET,Footnote 1 a competitive 2QBF solver [22]. In this section, we compare CADET experimentally with existing algorithms for functional synthesis. Additionally, we implemented a certificate checker for functional synthesis and for quantifier elimination, to make sure that the computed functions are correct. The certificate checker only shares the code for AIGER circuits and the SAT solver (of which we have tried several), but is completely independent otherwise to reduce the chance of correlated bugs. The results of CADET have been checked with the proof checker; running times reported below are excluding the time to check the certificates.

Fig. 1.
figure 1

Log-scale cactus plot comparing the performance over all instances.

Full size image

So far, there is no standard benchmark for functional synthesis or quantifier elimination. Like previous works on functional synthesis, we resort to using the 2QBF benchmark from QBFEVAL’17 [14], and re-interpret them as functional synthesis problems. The 2QBF benchmark from QBFEVAL’17 is a collection of 384 formulas from various domains, mostly from software verification, program synthesis, and logical equivalences [33,34,35,36].

We compare CADET to the most recent tools on functional synthesis, BaFSyn [8] and BFSS [10], the latter of which has been shown to consistently outperform the earlier, BDD-based tools SSyft [25] and RSynth [26, 27]. We ran CADET in two configurations: with (CADET+) and without (CADET) its CEGAR module [23]. We present the results as a cactus plot, which is obtained by running each tool on all formulas, sorting the running times for each tool separately. A point x, y in this plot means that x formulas were solved in less than time y. Note that the time axis is in log-scale (Fig. 1).

CADET shows a clear edge in performance: it is one to two orders of magnitude faster than its strongest competitor, BFSS, and can solve significantly more formulas. But despite the clear performance advantage in this aggregate view, BaFSyn and BFSS can be faster for individual formulas or subfamilies of QBFEval, as shown in previous works [8, 10].

6 The Current State of CADET

Originally designed as an experimentation platform, CADET has grown to become a performant and versatile tool for the synthesis of Boolean functions. It consistently wins awards at the annual QBFEVAL competitions, and is the only such tool able to prove all its results [14].

CADET reads specifications in the QDIMACS and the QAIGER formats, and now supports the synthesis of Boolean functions for 2QBF, functional synthesis, and quantifier elimination with the command line options -c [file], -f [file], and -e [file]. The functions computed by CADET are much smaller compared to those found by CEGAR-based algorithms [22], and in its default configuration, CADET double-checks its results before reporting them. This can be deactivated by the flag --dontverify.

It has also been integrated in py-aiger [37], a Python package for the convenient handling of circuits due to Marcell Vazquez-Chanlatte, which enables us to easily model and prototype new approaches. For example, we can write:

figure b

CADET also has an experimental reinforcement learning interface that allows us to automatically learn decision heuristics with the help of graph neural networks. A recent effort shows that there is huge potential in learning better branching heuristics from scratch [38].

7 Conclusions

In this work, we extended ID with the ability to solve functional synthesis and quantifier elimination problems. The extension is very simple—we only need to add the clauses of the original formula to its conflict check. The resulting algorithm significantly outperforms previous algorithms for functional synthesis.