# secondorder_quantified_boolean_logic__16fc6b9d.pdf

Second-Order Quantified Boolean Logic

Jie-Hong R. Jiang

Graduate Institute of Electronics Engineering, National Taiwan University, Taipei, Taiwan Department of Electrical Engineering, National Taiwan University, Taipei, Taiwan jhjiang@ntu.edu.tw

Second-order quantified Boolean formulas (SOQBFs) generalize quantified Boolean formulas (QBFs) by admitting second-order quantifiers on function variables in addition to first-order quantifiers on atomic variables. Recent endeavors establish that the complexity of SOQBF satisfiability corresponds to the exponential-time hierarchy (EXPH), similar to that of QBF satisfiability corresponding to the polynomialtime hierarchy (PH). This fact reveals the succinct expression power of SOQBFs in encoding decision problems not efficiently doable by QBFs. In this paper, we investigate the second-order quantified Boolean logic with the following main results: First, we present a procedure of quantifier elimination converting SOQBFs to QBFs and a game interpretation of SOQBF semantics. Second, we devise a sound and complete refutation-proof system for SOQBF. Third, we develop an algorithm for countermodel extraction from a refutation proof. Finally, we show potential applications of SOQBFs in system design and multi-agent planning. With these advances, we anticipate practical tools for development.

1 Introduction

Theoretical and practical advancements in Boolean satisfiability (SAT) (Biere et al. 2021) have made it an important technology enabling various complex computation tasks in artificial intelligence, hardware design, software engineering, among others. The frontiers of satisfiability research are continuously extended to (non-)Boolean queries involving different types of quantifiers. Notably, the quantified Boolean formula (QBF) allows existential and universal quantifiers to appear in an expression. The dependency quantified Boolean formula (DQBF) (Peterson and Reif 1979) further extends QBF by allowing Henkin quantifiers (Henkin 1961) to explicitly specify the dependencies of existential variables on universal variables. These extensions make the underlying computational complexity lifted from the NP-completeness of SAT (Cook 1971), to the PSPACEcompleteness of QBF (Stockmeyer and Meyer 1973), and to the NEXP-completeness of DQBF (Peterson and Reif 1979). To date, practical decision procedures for checking the QBF and DQBF satisfiability are under active research,

Copyright 2023, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

and various solvers and preprocessors are available (Biere et al. 2021; Scholl and Wimmer 2018). The second-order quantified Boolean formula (SOQBF) extends QBF in the allowance of function variables and their quantification. Its satisfiability checking has complexity corresponding to the exponential-time hierarchy (EXPH) (Dawar, Gottlob, and Hella 1998), as was established in (Lohrey 2012; L uck 2016). The connection between SOQBF and EXPH is similar to that between QBF and the polynomial-time hierarchy (PH) (Stockmeyer 1976). Essentially, DQBFs are an elementary class of SOQBFs with only one level of existential quantifiers over function variables. SOQBFs can be powerful to succinctly encode decision problems that have no succinct QBF encoding. There are recent efforts studying variants (Hannula et al. 2016) and special fragments (Hannula et al. 2020) of SOQBFs. In this work, we study second-order quantified Boolean logic in the aspects of representation and interpretation, proof system, and countermodel extraction. The main results include presenting a procedure of quantifier elimination converting SOQBFs to QBFs and a game interpretation of SOQBF semantics (Section 3), devising a sound and complete refutation proof system (Section 4), developing an algorithm of extracting a countermodel, namely, a winning strategy under the game-theoretic interpretation of SOQBF, from a refutation proof (Section 5), and showing potential applications of SOQBFs in system design and multi-agent planning (Section 6). With these advances, we anticipate practical tools whose development may open new avenues for tackling computation problems too challenging to be formulated previously.

2 Preliminaries In this work, we are concerned with two types of variables, including atomic variables, represented with lower-case letters, e.g., x, y, and function variables, represented with, e.g., f, g. In the sequel, we do not specify a variable type when it is clear from the context. A variable set is represented with a upper-case letter, e.g., X = {x1, . . . , xn}, F = {f1, . . . , fn}. The cardinality of a set X is denoted as |X|.

The Thirty-Seventh AAAI Conference on Artificial Intelligence (AAAI-23)

For notational convention, Boolean connectives are denoted with (sometimes omitted) for conjunction, for disjunction, for implication, for biconditional, and for negation. A literal is a variable (positive polarity) or the negation of a variable (negative polarity). A clause is a disjunction of literals; a cube is a conjunction of literals. A conjunctive normal form (CNF) formula is a conjunction of clauses. Alternatively, a clause or cube is denoted with a set of literals, and a CNF formula is denoted with a set of clauses. In the sequel, we assume that a CNF formula is free of tautological clauses, namely, clauses containing literals of the same variable of opposite polarities are removed. When an atomic variable x is valuated, denoted [[x]], it takes on a value from the Boolean domain B = {0, 1}. A function variable f is associated with a set of atomic variables, called the support set of f, denoted S(f). When f is valuated, denoted [[f]], it takes on a Boolean function [[f]] : B|S(f)| B over variables S(f). We remark that the support set of a function variable may, in general, contain function variables. However, in the context of second order quantified Boolean logic, the dependency imposed by g S(f), for some function variable g, can be rewritten by replacing g in S(f) with a fresh new atomic variable xg and asserting the equivalence xg g. Hence, without loss of generality, we assume the support set of a function variable consists of only atomic variables. An assignment α over atomic variables X is a mapping α : X B for X X that valuates each x X . We alternatively represent an assignment on atomic variables as a cube. E.g., the assignment α over X = {x1, x2} with α(x1) 7 1, α(x2) 7 0 is represented as α = x1 x2; in the special case when X = , the cube representation of the corresponding assignment is α = 1, i.e., a cube without any literals. An assignment α is called full with respect to an atomic variable set X if every variable xi X appears in the cube representation of α. Otherwise, α is called partial with respect to X. Given an assignment α over variables X, its projection on variables X , denoted α X , is a submapping of α on variables X X . E.g., the projection of assignment α = x1 x2 on X = {x2, x3} is α X = x2. Similarly, an assignment α over function variables F maps each f F to a function α(f) : Bk B for k = |S(f)|. In the sequel, we do not specify the domain type (atomic or function variables) of an assignment when it is clear from the context. Given a formula ϕ, we define the cofactor of ϕ with respect to an assignment α over atomic variables X, denoted ϕ|α, as the induced formula of ϕ after substituting variables X with their respective mapped values under α, and replacing every function variable f, for S(f) X = , with a new function variable f α S(f) with support set S(f) \ X, which denotes an instantiated version of f under assignment α S(f). E.g., for formula ϕ = ( f1 f2 x1 x3)(f1 f2 x2 x3) with S(f1) = {x1, x3} and S(f2) = {x2, x3} and assignment α = x1 x2, we have ϕ|α = (f x1 1 f x2 2 x3). Note that the valuation [[f α S(f)]] is a function referring only to variables S(f) \ X and it equals the function [[f]] induced under assignment α.

That is, [[f α S(f)]] is a projected function valuation of f with respect to assignment α S(f).

3 Second-Order Quantified Boolean Formula

A second-order quantified Boolean formula (SOQBF) Φ can be inductively defined in the Backus-Naur form with the following rules.

Φ ::= 0 | 1 | x | f | Φ | Φ1 Φ2 | x.Φ | f.Φ (1)

for x and f being atomic and function variables, respectively. A quantifier or is called a first-order (resp. second-order) quantifier if the variable bound by it is an atomic (resp. a function) variable. I.e., in the above construction rules, the quantifiers for x and f are first-order and second-order quantifiers, respectively. For brevity, the construction rules with quantifier and Boolean connective are not shown as they are similar to those of quantifier and Boolean connective , and also can be constructed by the and rules and the and rules, respectively. A function variable in an SOQBF is specified with a fixed arity. There are two possible choices to describe the arguments of an n-ary function variable. One is to list all its arguments explicitly, and in this case a function variable may have multiple appearances in a formula with different arguments. E.g., in expression f(f(x, y), z), the 2-ary function variable f appears twice with different arguments. The other is to assume that an n-ary function variable always appear in a formula with fixed arguments. E.g., in expression (x f g)(z f g), assume f and g are 2ary and 3-ary function variables with fixed arguments (x, y) and (x, y, z), respectively. We note that the former can always be converted to the latter through Ackermann s expansion (Ackermann 1954). E.g., f(f(x, y), z) is converted to w.f1(w, z) (w f2(x, y)) along with the constraint x, y, z, w.((x w) (y z)) (f1(w, z) f2(x, y)) for w being a fresh new atomic variable. The formulas before and after the conversion are equisatisfiable. Therefore, without loss of generality, we assume a function variable has fixed arguments. Any SOQBF can be converted to the following prenex form

Q1F1, Q2F2, . . . , Qn Fn, Q1X1, . . . , Qm Xm.ϕ, (2)

where Qi, Qj { , }, for Qi = Qi+1 and Qj = Qj+1, Fi and Xj are nonempty sets of function and atomic variables, respectively, with S(f) X for any f Fi, and ϕ is a quantifier-free formula expressed in terms of variables F1 . . . Fn X1 . . . Xm. In Eq. (2), the quantifier part on the left is called the prefix, and ϕ is called the matrix. A function variable f Fi bound by quantifier Qi is said to be of (second-order) quantification level i, denoted lev(f) = i. Similarly, an atomic variable x Xi bound by quantifier Qi is said to be of first-order quantification level i. Also, we use the notation qnt(f) to refer to the quantifier type of variable f. In this work, we assume a formula is totally quantified, that is, every variable is bound by some quantifier.

(a) Block diagram of matrix circuit.

(b) Detailed circuit for the function-variable block in (a).

Figure 1: Matrix circuit of an SOQBF.

As to be shown, Eq. (2) can always be rewritten into an SOQBF with a single first-order quantification level, i.e., m = 1, of the form

Q1F1, Q2F2, . . . , Qn Fn, X.ϕ, or (3) Q1F1, Q2F2, . . . , Qn Fn, X.ϕ. (4)

As Eq. (3) and Eq. (4) are dual to each other, any property obtained for Eq. (3) can be carried to Eq. (4) by duality. Hence, in the sequel, we shall primarily consider Eq. (3).

Consider the SOQBF Φ of Eq. (2). The matrix ϕ over function variables f1, f2, . . . and atomic variables X = Sm i=1 Xi can be viewed as a circuit as illustrated in Fig. 1, where each box fi of the circuit in Fig. 1(a) corresponds to a multiplexer tree (or a binary decision diagram) controlled by the support set S(fi) X of fi, |S(fi)| = k as shown in Fig. 1(b). An assignment to function variable fi corresponds to determining the truth-table values t0, . . . , t2k 1, for k = |S(fi)|, the red boxes in Fig. 1(b). For an assignment α to the function variables, the truth or falsity of the SOQBF Φ is determined by the QBF Q1X1, . . . , Qm Xm.ϕ , where ϕ is the circuit induced by substituting all the truth-table values with constant 0 or 1 according to α. Therefore, the SOQBF Φ can be evaluated by a series of QBF evaluations with respect to function variable assignments following the second-order quantifiers Q1F1, Q2F2, . . . , Qn Fn.

Consequently, the SOQBF of Eq. (2) is true if there exists a model, namely, a set of Skolem functionals for the existential function variables such that substituting each existential function variable with its corresponding Skolem functional makes the induced formula true. The Skolem functional of variable f Fi for Qi = is a higher-order function that maps every assignment to variables S

j<i,Qj= Fj to an assignment to variable f. On the contrary, an SOQBF is false if there exists a countermodel, namely, a set of Herbrand functionals for the universal function variables such that substituting each universal function variable with its corresponding Herbrand functional makes the induced formula false. The Herbrand functional of variable f Fi for Qi = is a higher-order function that maps every assignment to variables S

j<i,Qj= Fj to an assignment to variable f. The truth and falsity of SOQBFs can be interpreted from a game-theoretic viewpoint. An SOQBF game is played by the exist-player, who controls the assignments to the existential function variables, and the forall-player, who controls the universal function variables. They take turns to assign function variables in ascending order of the quantification levels in the prefix. The former aims to satisfy the formula, whereas the latter aims to falsify the formula. The SOQBF is true if the exist-player has a winning strategy and false if the forall-player has a winning strategy. The winning strategy of the exist-player is effectively the model of Skolem functionals, and that of the forall-player is effectively the countermodel of Herbrand functionals. As an SOQBF is either true or false, the SOQBF game is determined, that is, either the exist-player or the forall-player has a winning strategy. This determinacy contrasts with the indeterminacy of the DQBF game, where the Henkin quantifier results in the asymmetric roles between the forall-player and the (multiple) exist-players (Balabanov, Chiang, and Jiang 2014). Note that when a DQBF is converted to an SOQBF by Skolemization, the converted SOQBF is of one level of function-variable quantification, in the form F1, X.ϕ.

Quantifier Elimination and QBF Conversion

Two formulas are called model-equivalent if there is a bijection between the models of the two formulas. That is, a model of one formula uniquely maps to a model of the other formula, and vice versa. A formula-rewriting transformation is model-preserving if the formulas before and after the transformation are model-equivalent. An SOQBF can be converted to a model-equivalent QBF via ground instantiation, where every function variable is instantiated with respect to a full assignment over its support set. The conversion can be done by iteratively eliminating the innermost atomic variable through formula expansion until no more atomic variable is left. Specifically, for the SOQBF

Q1F1, . . . , Qn Fn, QX, y.ϕ, (5)

by eliminating variable y, it can be rewritten into a modelequivalent SOQBF as

Q1F y 1 F y 1 , . . . , Qn F y n F y n , QX.ϕ|y ϕ| y, (6)

where F y i = {f α y | f α Fi, y S(f α)} {f α | f α Fi, y S(f α)} and F y i = {f α y | f α Fi, y S(f α)} {f α | f α Fi, y S(f α)}. Note that without instantiation, a function variable f is considered as f α for α = 1. Also, for Q1F1, . . . , Qn Fn, QX, y.ϕ, (7) by eliminating variable y, it can be rewritten as Q1F y 1 F y 1 , . . . , Qn F y n F y n , QX.ϕ|y ϕ| y. (8) Note that after all atomic variables are eliminated, any instantiated function variable, say f α, is of an empty support set. That is, its valuation corresponds to a 0-ary function that represents a truth-table entry under assignment α of function [[f]]. As a 0-ary function variable can be seen as an effective atomic variable, the final formula is effectively a QBF. Example 1. Consider the SOQBF g, f, x1, x2, x3.ϕ, with the support sets S(g) = {x1, x2} and S(f) = {x1, x3}, and the matrix ϕ = (g f x1 x2 x3)(g f). Expanding on x3 yields the SOQBF g, F, x1, x2.ϕ , where F = {f x3, f x3} with S(f x3) = S(f x3) = {x1}, and ϕ = (g f x3 x1 x2)(g f x3)(g f x3). Expanding further on x2 yields the SOQBF G, F, x1.ϕ , where G = {gx2, g x2} with S(gx2) = S(g x2) = {x1}, and ϕ = (gx2 f x3 x1)(gx2 f x3)(gx2 f x3) (g x2 f x3)(g x2 f x3). Finally, expanding on x1 yields the SOQBF, G , F .ϕ , where G = {gx1x2, gx1 x2, g x1x2, g x1 x2} with S(gx1x2) = S(gx1 x2) = S(g x1x2) = S(g x1 x2) = {}, F = {f x1x3, f x1 x3, f x1x3, f x1 x3} with S(f x1x3) = S(f x1 x3) = S(f x1x3) = S(f x1 x3) = {}, and ϕ = ((gx1x2 f x1 x3)(gx1x2 f x1 x3) (gx1x2 f x1x3) (gx1 x2 f x1 x3)(gx1 x2 f x1x3)) ((g x1x2 f x1 x3)(g x1x2 f x1x3) (g x1 x2 f x1 x3)(g x1 x2 f x1x3)). After x1, x2, x3 are expanded, the final SOQBF is effectively a QBF as all the function variables are of zero arity. The model-equivalence between Eq. (5) and Eq. (6) and that between Eq. (7) and Eq. (8) can be verified by the semantics of SOQBF as defined in Section 3. Proposition 1. The SOQBFs of Eq. (5) and Eq. (6) are model-equivalent. Proposition 2. The SOQBFs of Eq. (7) and Eq. (8) are model-equivalent.

Normal Form Conversion We note that any totally-quantified SOQBF can be converted to the normal form of Eq. (3) through a sequence of modelpreserving transformation steps. Specifically, a non-prenex SOQBF can be converted to a prenex SOQBF by variable renaming; the second-order quantifiers can be placed on the left of the first-order quantifiers because the support-set information is explicitly specified for all function variables; the first-order quantifiers can be homogenized to all universal with a modified Skolemization procedure detailed in the following. Without loss of generality, the SOQBF

Q1F1, . . . , Qn Fn, X1, y, X2.ϕ, (9)

with S(f) X1 {y} X2 for f Fi, can be converted to

Q1F1, . . . , Qn Fn, fy, X1, y, X2.(y fy) ϕ, (10)

where fy is a fresh new function variable with S(fy) = X1. Proposition 3. The SOQBFs of Eq. (9) and Eq. (10) are equisatisfiable, and are model-equivalent with respect to the models of function variables F1 . . . Fn.

Proof. Their relation can be shown by QBF conversion.

When the variable y is not in any support set of the function variables of Eq. (9), then the standard Skolemization applies, and Eq. (10) reduces to

Q1F1, . . . , Qn Fn, fy, X1, X2.ϕ , (11)

where ϕ is obtained from ϕ by replacing every appearance of variable y in ϕ with variable fy. In Eq. (3), when Qn = , it can be simplified to an equisatisfiable SOQBF of n 1 levels of second-order quantifiers as the following proposition states. Proposition 4. The SOQBF of Eq. (3) with Qn = is equisatisfiable to

Q1F1, Q2F2, . . . , Qn 1Fn 1, X , X.ϕ , (12)

where X is derived from Fn with |X | = |Fn| by creating a fresh atomic variable xf X for every function variable f Fn, and ϕ is derived from ϕ by replacing function variable f with its corresponding atomic variable xf in ϕ. Furthermore, the SOQBF of Eq. (3) with Qn = and ϕ in CNF can be simplified to an equisatisfiable formula with all appearances of variables Fn being removed from the prefix and matrix of Eq. (3).

Proof. Expanding variables X in Eq. (3) yields a QBF formula with its matrix being a conjunction of formulas. Because universal quantification and conjunction commute, we can reuse the same name for the instantiated variables of f Fn in the universal quantification. Further when ϕ is in CNF, the variables of Fn can be removed by QBF - reduction.

That is, the SOQBF of Eq. (3) with Qn = is equisatisfiable to the same formula but changing the arity of every function f Fn to zero. In this case, the number of effective second-order quantification levels is reduced by one. Similarly, the SOQBF of Eq. (4) with Qn = is equisatisfiable

to the same formula but changing the arity of every function f Fn to zero, thus reducing one second-order quantification level. We note that an SOQBF with one function variable depending on another function variable can be converted to the normal form where function variables depend only on atomic variables. Specifically, let f be a function variable with support set S(f) containing a function variable g. The SOQBF ..., Qif, ..., Qjg, ..., X.ϕ

can be re-expressed as

..., Qif, ..., Qjg, ..., X, y.(y g) ϕ

for g S(f) being replaced with a fresh atomic variable y. We note that the above rewriting also works if the quantification level of g is smaller than f. A similar discussion is made in (Hannula et al. 2016).

Complexity The exponential-time hierarchy (EXPH) is to the computational complexity of checking SOQBF satisfiability (SOQSAT) as the polynomial-time hierarchy (PH) is to that of checking QBF satisfiability. Recall the complexity classes ΣEXP k , for ΣEXP k = NEXPΣP k 1. For k = 1, ΣEXP 1 = NEXP, which is the complexity of satisfiability checking for the Sform DQBF (Balabanov, Chiang, and Jiang 2014). By duality, complexity classes ΠEXP k , for ΠEXP k = co NEXPΣP k 1. For k = 1, ΠEXP 1 = co NEXP, which is the complexity of satisfiability checking for the H-form DQBF (Balabanov, Chiang, and Jiang 2014). Let SOQSATk be the satisfiability of SOQBFs with k levels of second-order quantifiers and Q1 = . The following statement, also in (L uck 2016), can be established by directly encoding the execution of an alternating Turing machine (ATM) (Chandra, Kozen, and Stockmeyer 1981) with k 1 alternations in an SOQBF of k levels of second-order quantification. (We omit the proof due to the page limit.)

Theorem 1. For any k 1, SOQSATk is ΣEXP k -complete.

Consider SOQSAT without bounding the quantification levels of an SOQBF. We note that as long as the number of alternations of the ATM is polynomial in the input size, the computation table of an exponential-time execution of the ATM can be efficiently encoded in an SOQBF of polynomial size. Let AEXP(poly) be the class of problems that can be decided by an ATM with k alternations for k polynomial in the input size. Consequently, the following corollary, also in (L uck 2016), is immediate.

Corollary 1. SOQSAT is complete in AEXP(poly).

4 Refutation Proof System In the sequel, we assume that an SOQBF is in the prenex normal form with all atomic variables being universally quantified as in Eq. (3), and the matrix is in CNF. As shown previously, an SOQBF can be converted to a model-equivalent QBF by ground instantiation. The conversion ensures the matrix of the resultant QBF remains in CNF as all atomic

variables are universally quantified. Then QBF resolution, Q-res, a sound and complete refutation proof system for QBF, can be applied to decide the truth or falsity of a QBF (Kleine B uning, Karpinski, and Fl ogel 1995). Essentially, Q-res consists of two rules: 1) resolution of two clauses on an existential pivot variable and 2) reduction on universal variables in a clause whose quantification levels are greater than those of any other existential variables in the clause. However, the conversion from an SOQBF to a QBF by ground instantiation mostly suffers an immediate exponential growth of formula size. To alleviate this problem, we apply a lazy instantiation strategy similar to the resolution principle for the first-order logic (FOL) (Robinson 1965), as we detail below. For a clause C = W i ℓ(fi) W j ℓ(xj) in the matrix of an SOQBF, where ℓ(v) denotes the literal appearance of variable v in C, its function-form is derived by the rule:

W i ℓ(fi) W j ℓ(xj)

Functionize W i ℓ(f { ℓ(xj) | xj S(fi)} i )

where literal ℓ(f { ℓ(xj) | xj S(fi)} i ) inherits the polarity of literal ℓ(fi). That is, the function variables of C are replaced with their respective partially instantiated versions with respect to the literal set (i.e., assignment) { ℓ(xj)} whereas all literals of atomic variables are being removed from C. Thereby, the derived set of clauses is in a function-form, namely, having no literals of atomic variables. Essentially, a literal f α (resp. f α) asserts the condition that the function value of f under any full assignment β over variables S(f) consistent with α, i.e., β α = 0, is true (resp. false). Let Φ be the SOQBF obtained from Φ such that its matrix consists of clauses functionized from those of Φ and its prefix quantifies the new variables for the quantifier type and quantification level of f { ℓ(xj) | xj S(fi)} i being the same as those of fi in Φ. We remark that unlike ground instantiation, the valuations of two partially instantiated function variables may not be independent. E.g., for a function variable f with S(f) = {x1, x2}, its two instantiated versions f x1 and f x2 are not independent because their valuations have to agree on f x1 x2. For simplicity, we shall assume that all the partially instantiated versions of variable fi are bundled together in the prefix and referred to as a quantifier bundle. We sometimes write Qfi, for Q { , }, in the prefix to represent quantification over all instantiated versions of fi.

Lemma 1. An SOQBF Φ and its functionized version Φ are model-equivalent.

Proof. Let ϕ be the matrix of Φ . Expanding ϕ with V α ϕ |α for assignments α over all atomic variables X of Φ (recall that X are universally quantified) results in an effective QBF, which is the same as the QBF obtained through ground instantiation on Φ.

The following two rules form a refutation proof system SOQ-res for functionized SOQBFs.

C1 f α1 C2 f α2 qnt(f) = , α1 α2 = 0 F -Resolve DInst(C1, α2, α1) DInst(C2, α1, α2)

C ℓ(f α) qnt(f) = , lev(f) > lev(g) for any g in C, qnt(g) = F -Reduce C In rule F -resolve, given a clause C and two ordered assignments α and β, the differential instantiation DInst(C, α, β) operation produces a new clause C with _

ℓ(f γ i ) C ℓ(f γ {ℓ(xj) α\β | xj S(fi),xj / γ, xj / γ} i ),

where α \ β is in the set notation of assignments, denoting removing β literals from α. Note that the two differential instantiations in the resolvent effectively achieve unification in the resolution principle of FOL (Robinson 1965). We remark that the above rule provides a stronger unification than that of DQBF calculus D-IR-calc (Beyersdorff et al. 2016), where the resolvent generated effectively corresponds to DInst(C1, α1 α2, 1) DInst(C2, α1 α2, 1)1. Recall the assumption that a clause is non-tautological. We note that F -resolve on two non-tautological clauses may yield a partially tautological clause, e.g., (C f α f β) for α β = 0. In such occasions, we shall remove the tautological part of the clause. Before presenting the method for partial-tautology removal, we first generalize the notation f α of function variable f instantiated with respect to an assignment α over a subset of S(f) to f χ, where χ is a Boolean expression over variables S(f). A literal f χ (resp. f χ) indicates the condition that f must be true (resp. false) for any assignment α that satisfies χ. By this definition, the equality f α1 α2 = f α1 f α2 holds. E.g., for S(f) = {x1, x2}, the partial instantiation f x1 is equivalent to f x1x2 x1 x2 = f x1x2 f x1 x2. Also, the literal f x1, meaning ( f)x1, is equivalent to f x1x2 x1 x2 = f x1x2 f x1 x2, but not (f x1x2 f x1 x2). Note that, in special cases, literal f 1 indicates f being a constant-1 function, and literal f 0 equals 1 (a tautology), imposing no constraint on f. Now the partially tautological clause (C f α f β) with α β = 0 can be rewritten as (C f α (β β) f (α α) β), which in turn can be factored into four clauses (C f α β f α β) (C f α β f α β) (C f α β f α β) (C f α β f α β). By removing the first tautological clause, we obtain the nontautological part of (C f α f β) as (C f α β f α β) (C f α β f α β) (C f α β f α β). In the sequel, we assume that a partially tautological clause is rewritten with non-tautological ones by the following rule.

(C f α f β) α β = 0 Detautologize (C f α β f α β) (C f α β f α β) (C f α β f α β)

1Note that Boolean constant 1 here corresponds to an assignment whose literal set is empty.

Note that the expression deduced by detautologization is not in CNF and has to be further factored into |α| + |β| + |α||β| clauses. Note that without removing tautological clauses may result in unsound F -reduce operation. To see the problem, consider the SOQBF f.(f f), which equals f.1 and is true. However, without removing the tautological clause (f f), by F -reduction, the matrix reduces to an empty clause, making the SOQBF equal f.0, which is false. Therefore, it is crucial to make clauses non-tautological. For rule F -reduce, in the sequel we shall assume that a clause C is maximally reduced by iterative application of the rule until no more literals can be removed from C.

Lemma 2. The resolvent produced by the F -resolve rule is logically implied by the conjunction of the two parent clauses.

Proof. Note that DInst(C1 f α1, α2, α1) can be rewritten as DInst(C1, α2, α1) f α1 α2 and thus is implied by C1 f α1. Similarly, DInst(C2 f α2, α1, α2) equals DInst(C2, α1, α2) f α1 α2 and is implied by C2 f α2. In addition, we know that (DInst(C1, α2, α1) f α1 α2) (DInst(C2, α1, α2) f α1 α2) implies DInst(C1, α2, α1) DInst(C2, α1, α2). Hence the lemma follows.

Lemma 3. A functionized SOQBF with one existential quantification level is false if and only if an empty clause can be derived by a sequence of F -resolve operations.

Proof. A functionized SOQBF with one existential quantification level can be seen as a special case of Skolem normal form of an FOL formula. As the F -resolve rule is an analogy of the resolution principle of FOL (Robinson 1965), the lemma follows from the completeness of the FOL resolution principle using the semantic-tree argument (Chang and Lee 1973).

The soundness of F -reduction is stated in the following lemma.

Lemma 4. An SOQBF Φ with prefix π and matrix ϕ C (for C non-tautological) is true if and only if the SOQBF Φ = π.ϕ C is true, where C is a clause F -reduced from C.

Proof. ( ) If Φ is true, then we can find a model M of Skolem functionals for the existential function variables. The model M makes all the clauses of the matrix ϕ C be satisfied under all possible function assignments to the universal function variables. As C is F -reduced from C, the reduced universal function variable does not affect the Skolem functionals to satisfy C besides ϕ. Therefore, M is also a model for Φ . ( ) Observe that removing literals from C to get C makes Φ no easier to satisfy than Φ. Any model for Φ is also a model for Φ.

Theorem 2. An SOQBF Φ is false if and only if an empty clause can be derived by SOQ-res.

Proof. The proof can be done in a way similar to that of Qres for QBF (Kleine B uning, Karpinski, and Fl ogel 1995). ( ) We show by induction on k, the number of quantifier bundles. For the base case, when k = 1 and Φ = F1.ϕ with F1 = {f α1,1 1 , . . . , f α1,n1 1 }, the empty clause is derivable according to Lemma 3. When k = 1 and Φ = F1.ϕ with F1 = {f α1,1 1 , . . . , f α1,n1 1 }, the empty clause is clearly derivable by F -reduce. As the induction hypothesis, assume that the empty clause can be derived for any Φ with k < m. For the induction case, when k = m and Φ = F1, Q2F2, . .. , Qm Fm.ϕ with Fi = {f αi,1 i , . . . , f αi,ni i }, consider all possible valuations on the function variable f1, that is, all possible assignments to the 2|S(f1)| ground instantiated function variables of f1. The formula of Φ induced under a valuation [[f1]], i.e., an assignment to the 2|S(f1)| groundinstantiated function variables of f1, denoted Φ|[[f1]], is the

formula Q2F2, . . . , Qm Fm.ϕ|f1=[[f1]], where the cofactor

ϕ|f1=[[f1]] denotes the formula of ϕ with every appearance of F1-literals being valuated (to either 0 or 1) with respect to [[f1]].2 By the induction hypothesis, an empty clause is derivable via SOQ-res for the formula induced under every function valuation [[f1]]. Let Φ = F1, Q2F2, . . . , Qm Fm.ϕ for ϕ = {C ϕ | C not satisfied by [[f1]]}. Then, either an empty clause or a CNF formula of f1-instantiated literals falsified by [[f1]] can be deduced for Φ via SOQ-res. Note that because ϕ ϕ holds, the formulas deducible from Φ can also be deduced from Φ. Let ψ be the conjunction of these deduced CNF formulas (possibly including an empty clause) for all valuations of f1. It is effectively a formula after quantifier elimination of variables F2, . . . , Fm from Φ. Because Φ is false, so is ψ. An empty clause is derivable from ψ by F -resolve due to its correspondence to the base case. When k = m and Φ = F1, Q2F2, . . . , Qm Fm.ϕ, following the above reasoning, as ψ is a CNF formula and all its variables are universally quantified, an empty clause can be derived by F -reduce. Therefore, for a false SOQBF Φ with an arbitrary number of quantifier bundles, an empty clause can be derived by SOQ-res. ( ) By the soundness of F -resolution and F -reduction as stated in Lemmas 2 and 4, the derivation of an empty clause via SOQ-res ensures the falsity of the SOQBF.

5 Countermodel Extraction

Similar to the countermodel extraction of Herbrand functions from a Q-res-proof of a QBF (Balabanov and Jiang 2012), it is possible to extract a countermodel of Herbrand functionals from a SOQ-res-proof of an SOQBF. Let ite(a, b, c) be the if-then-else operation on Boolean expressions a, b, and c, denoting if a, then b, else c, which equals the expression ab ac. We represent a decision list

2Note that literal f α 1 (resp. f α 1 ) valuates to 1 under [[f1]] if and only if all ground instantiated variables {f β 1 | α β = 0} are assigned 1 (resp. 0) in [[f1]].

Algorithm 1: Countermodel Extraction Input: A false SOQBF Φ and an SOQ-res proof DAG GΠ(VΠ, EΠ) Output: A countermodel represented with decision lists 1: for all vertex v of GΠ in topological order do 2: if v.clause is F -reduced from u.clause, i.e., (u, v) EΠ then 3: for all universal ℓ(f α) in u.clause but not in v.clause do 4: γ := α; 5: for all non-empty DLf β of variable f do 6: if α β = 0 then 7: if ℓ(f α) = f α then 8: let DLf α β be DLf β added by ( v.clause, 0); 9: else if ℓ(f α) = f α then 10: let DLf α β be DLf β added by ( v.clause, 1); 11: rename DLf β to DLf α β; 12: γ := β γ; 13: if γ = 0 then 14: if ℓ(f α) = f α then 15: create DLf γ with entry ( v.clause, 0); 16: else if ℓ(f α) = f α then 17: create DLf γ with entry ( v.clause, 1); 18: if v.clause is an empty clause then 19: return DLs;

(Rivest 1987) as a sequence (e1, c1), (e2, c2), . . . , (ek, ck) of expression-constant pairs to mean function

ite(e1, c1, ite(e2, c2, ite(. . . , ite(ek, ck, ck) . . .))).

The Herbrand functionals are to be built with decision lists (DLs) in Algorithm 1 for countermodel extraction. The SOQ-res refutation proof of a false SOQBF can be represented as a directed acyclic graph (DAG) GΠ(VΠ, EΠ), where a vertex v VΠ represents a clause v.clause and an edge (u, v) EΠ signifies u.clause is derived from v.clause by either F -resove or F -reduce. Given a false SOQBF and its SOQ-res refutation DAG, Algorithm 1 computes a countermodel consisting of Herbrand functionals for the universally quantified function variables. It traverses GΠ in a topological order until a vertex of empty clause is reached (Line 1). For a vertex v with v.clause being F -reduced from u.clause (Line 2), it examines the F -reduced literals from u.clause (Line 3). For each such literal, say ℓ(f α), it updates all DLs of instantiated function variables f β of f for α β = 0 (Lines 5 11). Specifically, the DL of f α β is created to be the same as f β but appended with the pair ( v.clause, 0) if ℓ(f α) is of positive polarity (Lines 7, 8) and ( v.clause, 1) otherwise (Lines 9, 10). Also, the DL of f β becomes that of f α β (Line 11). If α is not completely covered by the β assignments (Line 13), a new DL is created for the remaining assignments of α with entry ( v.clause, 0) if ℓ(f α) is of positive polarity (Lines 14, 15) and ( v.clause, 1) otherwise (Lines 16, 17).

The DLs are returned when a vertex of empty clause is reached (Lines 18, 19). Note that any two distinct DLs, say, DLf α1 and DLf α2 , computed by Algorithm 1 satisfy the orthogonality that the instantiated assignments are mutually independent, i.e., α1 α2 = 0. To maintain this orthogonality, the number of DLs may grow exponentially in the number of atomic variables. Note also that a Herbrand functional returned by the algorithm may refer not only to existential function variables but also to universal function variables. To eliminate the dependencies on universal function variables, unwanted universal function variables can be substituted with their corresponding Herbrand functionals. By repeated substitutions in ascending order of quantification levels, all Herbrand functionals can be made to depend only on existential function variables. In the substitutions, an instantiated universal function variable may not have its corresponding DL returned by Algorithm 1. However, the Herbrand functional of an arbitrary instantiated function variable f α can be obtained by forming the conjunction of the Herbrand functionals of variables f β, for β α = 0, which are derivable from the DLs returned from Algorithm 1. The correctness of Algorithm 1 is stated as follows.

Theorem 3. Given a false SOQBF Φ = π.ϕ and a refutation proof, let the instantiated universal functional variables in ϕ be substituted with the Herbrand functionals extracted by Algorithm 1. Then ϕ after the substitution is unsatisfiable.

Proof. Observe that when the instantiated assignments of every universal function variable appearing in the resolution proof are all orthogonal, the constructed DLs form a countermodel, as can be shown in the same way as that of the QBF case (Balabanov and Jiang 2012). Furthermore, it can be verified that Algorithm 1 maintains the orthogonality of the partially instantiated universal function variables in constructing the DLs.

Example 2. Consider the SOQBF

g1, f1, g2, f2, x1, x2, x3.C1C2C3,

where the support sets S(g1) = {x1}, S(f1) = {x2, x3}, S(g2) = {x2, x3}, S(f2) = {x1, x3}, and

C1 = (gx1 1 f x2 x3 1 f x1 x3 2 ), C2 = (g2 f2), C3 = ( g x1 1 f x2 1 gx2 2 f x1 2 ).

Its falsity can be shown by the following refutation steps.

C4 = (gx1 1 f x2 x3 1 g x3 2 ) by F -resolve(C1, C2); C5 = (gx1 1 f x2 x3 1 ) by F -reduce(C4); C6 = (g2 g x1 1 f x2 1 gx2 2 ) by F -resolve(C2, C3);

C 6 = (g x2 2 g x1 1 f x2 1 gx2 2 ) by tautology removal; C7 = ( g x1 1 f x2 1 ) by F -reduce(C 6); C8 = (gx1 1 g x1 1 ) by F -resolve(C5, C7); C9 = () by F -reduce(C8).

Given the proof, Algorithm 1 derives the DLs:

DLg x2 x3 2 = ite( gx1 1 f x2 x3 1 , 0, ite(g x1 1 f x2 1 , 0, 1)),

DLg x2x3 2 = ite(g x1 1 f x2 1 , 0, 1),

DLgx2 x3 2 = ite( gx1 1 f x2 x3 1 , 0, ite(g x1 1 f x2 1 , 1, 0)),

DLgx2x3 2 = ite(g x1 1 f x2 1 , 1, 0),

DLgx1 1 = ite(1, 0, 1)

DLg x1 1 = ite(1, 1, 0).

They yield the following Herbrand functionals:

H[gx1 1 ] = 0, H[g x1 1 ] = 1, H[gx2x3 2 ] = f x2 1 , H[gx2 x3 2 ] = f x2 x3 1 f x2 1 = f x2 1 , H[g x2x3 2 ] = f x2 1 , H[g x2 x3 2 ] = f x2 x3 1 f x2 1 = 0.

By combining and substituting the Herbrand functionals to their corresponding function variables in the matrix, we get

(f x2 x3 1 f x1 x3 2 )( f2)( f x2 1 f x1 2 ),

which can deduce an empty clause via F -resolve.

6 Applications We briefly mention two potential applications of SOQBF, one in system synthesis and the other in AI planning. For the first application, consider the system block diagram shown in Fig. 2, where an unknown component F (with inputs Y ) is to be synthesized within a known context circuit C (with inputs X), which is to be composed with some third-party design G (with inputs Z). We are asked to design F such that the entire composite system satisfies some desired safety property P regardless of any function G for composition. For simplicity, assume the systems are combinational, i.e., memoryless. Then the synthesis problem can be expressed in an SOQBF of the form

F, G, H, X, Y, Z, W.ϕ,

where function variables F, G, H are with support sets S(F) = Y, S(G) = Z, S(H) = X Y Z W, for W being extra atomic variables for CNF encoding of the matrix constraint ϕ and H being extra function variables for normal form conversion. For the second application, consider a planning problem of two opposing agents A1 and A2. Assume the two agents take actions by turns sequentially. We are interested in knowing whether, under a bounded planning horizon, for any action strategy of A1, agent A2 has a strategy to enforce the environment transition from the initial state to a goal state. Assume for simplicity that the planning horizon is one. Then the planning problem can be expressed in an SOQBF of the form

F1, F2, E, S, S , S , X. (I(S) T1(S, S , F1) T2(S , S , F2) G(S )) ψ,

Figure 2: Circuit synthesis for compositional safety.

where function variables F1 with S(F1) = S and F2 with S(F2) = S correspond to the state updates due to the action choices of A1 and A2, respectively; function variables E are extra ones for normal form conversion; atomic variables S, S , and S are the state variables of the environment in the beginning, after A1 taking action, and after A2 taking action, respectively; atomic variables X are extra ones for CNF encoding; predicates I, T1, T2, and G correspond to formulas that constrain the initial states, state-action relation of A1, state-action relation of A2, and goal states, respectively; quantifier-free formula ψ is induced from normal form conversion.

7 Conclusions and Future Work

This paper studied the second-order quantified Boolean logic from the aspects of representation and interpretation, complexity, refutation proof system, and countermodel extraction. Specifically, we established the connection between SOQBF and QBF. We extended the FOL resolution principle and QBF resolution calculus to a sound and complete refutation proof system for SOQBF, and extended the countermodel extraction algorithm of QBF to SOQBF. Potential applications of SOQBF were also discussed. For future work, we plan to identify more applications. In particular, checking memory consistency models (Cooksey et al. 2019) could be an interesting direction. Also, we intend to develop SOQBF solvers for potential practical applications.

Acknowledgements

The author is grateful to Christoph Scholl and Tony Tan for their valuable comments on the manuscript. This work was partly supported by the National Science and Technology Council of Taiwan under Grant 111-2221-E-002-182 and Grant 111-2923-E-002-013-MY3.

References Ackermann, W. 1954. Solvable cases of the decision problem. North-Holland Publishing Company. Balabanov, V.; Chiang, H.-J. K.; and Jiang, J.-H. R. 2014. Henkin quantifiers and Boolean formulae: A certification perspective of DQBF. Theoretical Computer Science, 523: 86 100. Balabanov, V.; and Jiang, J.-H. R. 2012. Unified QBF Certification and Its Applications. Formal Methods in System Design, 41: 45 65.

Beyersdorff, O.; Chew, L.; Schmidt, R. A.; and Suda, M. 2016. Lifting QBF Resolution Calculi to DQBF. In Proceedings of International Conference on Theory and Applications of Satisfiability Testing, 490 499. Biere, A.; Heule, M.; van Maaren, H.; and Walsh, T., eds. 2021. Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press. Chandra, A. K.; Kozen, D. C.; and Stockmeyer, L. J. 1981. Alternation. J. ACM, 28(1): 114 133. Chang, C.-L.; and Lee, R. C.-T. 1973. Symbolic Logic and Mechanical Theorem Proving. Academic Press. Cook, S. A. 1971. The Complexity of Theorem-Proving Procedures. In Proceedings of ACM Symposium on Theory of Computing, 151 158. Cooksey, S.; Harris, S.; Batty, M.; Grigore, R.; and Janota, M. 2019. Pride MM: Second Order Model Checking for Memory Consistency Models. In Formal Methods. FM 2019 International Workshops, 507 525. Dawar, A.; Gottlob, G.; and Hella, L. 1998. Capturing Relativized Complexity Classes without Order. Mathematical Logic Quarterly, 44(1): 109 122. Hannula, M.; Kontinen, J.; L uck, M.; and Virtema, J. 2016. On quantified propositional logics and the exponential time hierarchy. In Proceedings of International Symposium on Games, Automata, Logics and Formal Verification, 198 212. Hannula, M.; Kontinen, J.; L uck, M.; and Virtema, J. 2020. On the Complexity of Horn and Krom Fragments of Second Order Boolean Logic. Co RR, abs/2007.03867. Henkin, L. 1961. Some Remarks on Infinitely Long Formulas. In Journal of Symbolic Logic, 167 183. Kleine B uning, H.; Karpinski, M.; and Fl ogel, A. 1995. Resolution for Quantified Boolean Formulas. Information and Computation, 117(1): 12 18. Lohrey, M. 2012. Model-checking hierarchical structures. Journal of Computer and System Sciences, 78(2): 461 490. L uck, M. 2016. Complete Problems of Propositional Logic for the Exponential Hierarchy. Co RR, abs/1602.03050. Peterson, G. L.; and Reif, J. H. 1979. Multiple-person alternation. In Proceedings of IEEE Symposium on Foundations of Computer Science, 348 363. Rivest, R. L. 1987. Learning decision lists. Machine Learning, 2(3): 229 246. Robinson, J. A. 1965. A Machine-Oriented Logic Based on the Resolution Principle. J. ACM, 12(1): 23 41. Scholl, C.; and Wimmer, R. 2018. Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications - Extended Abstract. In Proceedings of International Conference on Theory and Applications of Satisfiability Testing, 3 16. Stockmeyer, L. J. 1976. The polynomial-time hierarchy. Theoretical Computer Science, 3(1): 1 22. Stockmeyer, L. J.; and Meyer, A. R. 1973. Word Problems Requiring Exponential Time(Preliminary Report). In Proceedings of the ACM Symposium on Theory of Computing, 1 9.