Solving a PSPACE-complete problem with cP systems

Abstract

There have been a few NP-hard problems solved using cP systems including the travelling salesman problem. However, these problems are typically in NP rather than higher in the polynomial time hierarchy. In this paper, we solve QSAT (also known as TQBF), which is a well-known PSPACE-complete problem. Compared to other extant confluent P systems solutions, our deterministic cP solution only uses a small constant number of custom alphabet symbols (19), a small constant number of rules (10) and a small constant upper limit of membrane nesting depth (6), independent of the problem size.

1 Introduction

There are many computational complexity classes from log space to exponential and beyond. Many of these classes are not known to be equal or not. One of the millennial prize problems is dedicated to knowing whether P equals NP. The class NP has many complete problems such as the maximum independence set, the travelling salesman, and satisfiability problems. NP is one of the lowest levels of the polynomial-time hierarchy which characterises many different classes within PSPACE. One of the most famous PSPACE-complete problems is the Quantified Boolean Satisfiability (QSAT) problem, also known as the True Quantified Boolean Formula (TQBF) problem.

P systems proposed in [1] are a parallel and distributed model of computation based on a membrane structure. Following this work, many different variants of P systems were proposed including P systems with active membranes [2], spiking neural P systems [3], tissue P systems [4] and P systems with compound terms (cP systems). A large number of hard problems have been shown to be able to be solved in polynomial time with P systems. For example, in [2], it was shown how P systems with active membranes are able to solve NP complete problems in linear time.

cP systems are a variant of P systems that use high-level rewriting rules, based on one-way first-order syntactic unification (which is similar to pattern matching in functional programming). cP systems usually have smaller alphabets and rulesets than other P systems; however, the rules are more complex. cP systems have been used: to solve NP-hard problems such as the travelling salesman problem [5], to model distributed problems [6], and with recent research focused on verification [7]. In this paper, we demonstrate that cP systems can not only solve NP-hard problems in linear time, but also PSPACE-complete problems in polynomial time, with QSAT (i.e. TQBF) being solvable in linear time.

Our solution is—as far as we know—the first using cP systems; it uses ten rules and a constant custom alphabet of size 19. Our solution is deterministic, so we do not compare it here with nonconfluent solutions, such as [8]. (This could be the topic of further investigations.) We note that our solution is not the first confluent solution to PSPACE-complete problems using P systems. Previous solutions exist that follow similar ideas, such as [9,10,11,12]. Our solution utilises partial evaluation when generating the possible candidate solutions to the problem, allowing our solution to minimise the number of clauses being used. As shown in Table 1, our solution substantially improves the extant results, on several criteria: alphabet size, number of rules and membrane nesting depth—all small constants, independent of the problem size.

Table 1 Comparison of our solution with pre-existing confluent P system solutions, where n is the number of variables and m the number of clauses

Rule templates are groupings of similar rules, only differing by symbol indices. When counting rule templates and rules, we did not consider the numbers of repeated copies placed in different membranes/neurons. If we were to include such occurrence counts, the number of rules would increase drastically, for the other extant solutions. For example, the solution to QSAT in [9] would have ${\mathcal {O}}(2^{2n})$ rules, if we count the rules in every neuron. cP systems do not have such a exponential blow-up, and all these characteristics are small constants.

In Sect.  2, we discuss the background of this specific problem and how cP systems work. In Sect.  3, we present and discuss our ruleset to solve the QSAT problem.

2 Background

In this section, we cover cP systems and a brief explanation of the QSAT problem. For a more thorough introduction to cP systems, see [13].

2.1 QSAT

A Boolean formula is an expression involving Boolean variables and Boolean operations. For more information on Boolean formulae, see [14]. An NP-complete problem is the Boolean satisfiability problem (SAT), which determines if the variables of a given Boolean formula can be assigned Boolean values that evaluate the formula to true.

A Boolean formula is in conjunctive normal form (CNF) if it is expressed as a conjunction ($\wedge$) of clauses. A clause is a disjunction ($\vee$) of literals. A literal is a variable or its negation (here indicated by overbars). For example, the following Boolean formula is in CNF:

$$\begin{aligned} (x_{1} \vee x_{2}) \wedge (x_{1} \vee {\bar{x}}_{2}). \end{aligned}$$

The SAT formulae assume implicit existential quantifiers on all variables. The existential quantifier ($\exists$) results are true if one of the possible assignments of the variables allows the formula to be true. Thus, the above formula is interpreted as:

$$\begin{aligned} \exists x_1 ~\exists x_2 ~(x_{1} \vee x_{2}) \wedge (x_{1} \vee {\bar{x}}_{2}). \end{aligned}$$

A quantified Boolean formula is a Boolean formula where variables can be explicitly and independently quantified, with existential or universal quantifiers. The universal quantifier ($\forall$) results true if every possible assignment of the variables results in the formula being true.

Without loss of generality, we use a restricted version of quantified Boolean formulae that are assumed to be in fully quantified prenex normal form. Prenex normal form (PNF) means that the quantified variables are all factored out before the Boolean formula. Fully quantified means that every variable in the Boolean formula has a quantifier. This leads to the problem TQBF, as presented in [14]:

$$\begin{aligned}&\mathrm {TQBF} \\&\quad = \{\phi \mid \phi ~\text {is a }{} \mathbf{true} \text { fully quantified Boolean formula in PNF}\}. \end{aligned}$$

As shown in [15], TQBF is a PSPACE-complete problem. Without loss of generality, here we only use Boolean formulae which are also in CNF form, a further restricted version which is still PSPACE-complete. This problem is usually referred to as QSAT, where [9,10,11,12] also make the same assumptions.

For example, the following two formulae are fully quantified Boolean formulae in CNF and PNF:

$$\begin{aligned} \forall x_{1} ~\exists&x_{2} ~(x_{1} \vee x_{2}) \wedge (x_{1} \vee {\bar{x}}_{2}). \end{aligned}$$

(1)

$$\begin{aligned} \exists x_{1} ~\forall&x_{2} ~(x_{1} \vee x_{2}) \wedge (x_{1} \vee {\bar{x}}_{2}). \end{aligned}$$

(2)

Solving QSAT for a given formula $\phi$ can be done, as shown in [14], with the recursive algorithm (pseudocode) presented here in Table 2, slightly adapted, where we separate $\phi$ in three components: q—the stack of quantifiers; p—the stack of variables; and f the Boolean expression itself (the unquantified matrix).

The given algorithm systematically explores all possible combinations of variable assignments and evaluates the formula according to the given quantifiers. In the top-down pass, expressions $f[x:=0]$, $f[x:=1]$ indicate substitutions in f of x by 0 (i.e. false), respectively, by 1 (i.e. true). In the bottom-up pass, ($\exists$) is associated with ($\vee$), and ($\forall$) with ($\wedge$), as straightforward arguments indicate.

Table 2 Recursive algorithm for QSAT: $q = \hbox {quantifiers}$; $p = \hbox {variables}$; $f = \hbox {unquantified Boolean expression}$

The candidate solutions of Formulae (1, 2) can be visualised on the trees shown in Figures 1, 2: (a) lists the quantified variables, top–down, one per tree layer; (b) is the top–down construction of the tree, showing variable assignments; and (c) is the bottom–up evaluation of the tree, applying $\vee$ for $\exists$ and $\wedge$ for $\forall$.

A sequential execution of the recursive solution makes a preorder traversal of the complete tree, using ${\mathcal {O}}(n)$ space and ${\mathcal {O}}(2^n)$ runtime steps, where n is the number of quantifiers (or variables) in the prefix, and also the number of tree levels below the root.

Fig. 1

QSAT tree for Formula (1): $\forall x_1 ~\exists x_2 ~(x_{1} \vee x_{2}) \wedge (x_{1} \vee {\bar{x}}_{2})$

Fig. 2

QSAT tree for Formula (2): $\exists x_1 ~\forall x_2 ~(x_{1} \vee x_{2}) \wedge (x_{1} \vee {\bar{x}}_{2})$

Note that Formulae (1, 2) only differ in quantifiers. Thus, Figs. 1, 2 differ only in their quantifiers lists (a) and evaluation results in otherwise isomorphic tress (c), while trees (b) are identical.

The recursion of the algorithm in Table 2 can be unrolled by straightforward techniques. The nonrecursive solution in Table 3 creates each layer of the tree successively, while implicitly discarding the previous layer. Variables in p are processed during the top–down pass, so p is simply successively popped. Quantifiers in q are required during the bottom–up pass, so, during the top–down pass, q is successively reversed into $q'$.

F is an ordered list of Boolean expressions, corresponding to the nodes of the corresponding layer in the underlying virtual tree. Initially, $F = (f)$, a singleton list containing the formula given by the problem. F changes $2n+1$ times, by way of the higher-order function map: (i) during the n top-down steps, each expression $f \in F$ is replaced by the substitutions pair $f[x:=0], f[x:=1]$; (ii) at the leaves level, when all variables have been assigned, each f is replaced by its evaluated Boolean value; and (iii) during the n bottom–up steps, each consecutive pair of Boolean values is replaced by either an $\wedge$ or $\vee$ result, depending on the corresponding quantifier, $\forall$ or $\exists$. (This quantifier was saved in $q'$ during the top-down pass.)

Assuming that enough processing elements are available, a parallel execution of this nonrecursive solution trades space for time, running in ${\mathcal {O}}(n)$ time and using ${\mathcal {O}}(2^n)$ space. Our cP solution follows the same process as the nonrecursive solution in Table 3.

Table 3 Nonrecursive pseudocode—layer by layer in both sequential and parallel modes: $q = \hbox {quantifiers}$; $p = \hbox {variables}$; $F = \hbox {list of unquantified Boolean expressions}$

2.2 cP systems

P systems, also known as membrane computing, is a generic framework for designing computational models inspired by biology. Similar to many other P systems variants, cP systems (i) assume access to unbounded resources, such as space and computing power; (ii) organise top-level cells into digraph-like structures (Fig. 3); and (iii) evolve by applying formal multiset rewriting rules, with additional messaging primitives between top cells.

Fig. 3

High-level view of our top-level cell, as initialised for Formula (1) (Cf. Table 8)

cP top cells contain multisets of atoms and labelled sub-cells, which are compound objects similar to ground terms used in logic programming (Prolog). However, unlike Prolog terms, cP terms are strictly multiset based, thus totally unordered and allowing repetitions. Collectively, cP cells (top cells and sub-cells) correspond to cells or membranes used by other P system variants.

cP rules are high level, supporting one-way first-order syntactic unification (which is similar to pattern matching in functional programming). Unlike other P systems variants, only cP top cells have rewriting rules. Sub-cells in cP systems do NOT have own rules and are only used to represent local data.

We now present a brief overview of cP systems, only focusing on the details needed here, specifically ignoring the inter-top-cell relations and messaging rules, as our solution here consists of one single top-cell.

Using a BNF-like notation, Tables 4 and 5 describe basic structures of cP systems, as used in this paper. The grammar presented in Table 4 describes the contents for top cells and sub-cells, i.e., how data are stored in cP multisets. The grammar presented in Table 5 describes the high-level rewriting rules for cP systems.

We use standard conventions: the symbol $\lambda$ denotes the empty multiset; dots (‘$\ldots$’) represent zero or more repetitions; atoms are denoted by lower case characters (letters or other symbols); and variables are denoted by uppercase letters, except the special discard variable, denoted by an underscore (${\underline{\ \ }}$).

Top cells have states and contain multisets of literal atoms and recursively nested compound terms called sub-cells. Functors are sub-cell labels, and their multiset arguments are enclosed in parentheses “()” Top-cell contents are all ground, i.e. cannot contain variables.

Rules are applied in state-based weak priority order (see example 5 in Sect. 2.3) and contain compound terms called vterms, which are similar to the sub-cell terms, but with one critical distinction: vterms may also include variables. State-based weak priority order enables simple but powerful application flow control, specifically branching (if then else) and various looping constructs.

As already mentioned, rules are applied using pattern matching unification between terms, and specifically unification between variables and other terms (atom or compound). Rules can be applied in two modes: in exactly-once (1) or max-parallel mode (+).

As usually, before a rule can be applied, it must match, by way of unification, all conditions specified by its left-hand side, and its promoter and inhibitor constraints. There are two cases: (i) vterm arguments enclosed in round parentheses ’()’ require complete match and (i) vterm arguments enclosed in curly braces ’{}’ require partial match, of only the specified contents. The second feature is not frequently needed, but enables partial sub-cell transformations similar to those of other P system variants, without locking the whole sub-cell; this is further described under the title microsurgery.

We emphasise that cP terms and vterms are strictly based on multisets. However, we can straightforwardly emulate other structures, such as numbers and even ordered lists. Essentially, numbers can be represented as multisets solely consisting of repeated occurrences of a designated unary digit, typically 1. We do not use lists here, so this topic is not discussed.

Terms with repeated arguments seem to require an order concept. However, we consider that these are just convenient shorthands to nested multiset-based labelled terms. For example, the term a(bc)(de) is actually a shorthand for $a(b c ~\cdot (d e))$, where the dot functor ($\cdot$) is system provided. Thus, if a is a sub-cell at nesting depth 1, then b and d are at nesting depths 2 and 3, respectively.

We conclude this subsection by noting that, unlike most other P system variants, cP terms and rules allow crisp algorithm descriptions, with constant-size alphabets, constant-size rulesets and bounded membrane nesting, independent of the size of the problem and number of cells in the system. The cP semantics will be further clarified in the following subsection, by way of examples.

Table 4 BNF grammar for cP top cells

Table 5 Restricted BNF grammar for cP rules, omitting inter-cell messaging and other features not used here

2.3 Examples of cP rules

We now present a few simple but typical rules for cP systems.

• 1. Change state from $s_0$ to $s_1$ and rewrite one pair of a and b into one c, provided that at least one p is present (and will stay unchanged in the cell):

  $s_0$ a b $\rightarrow _{1}$ $s_1$ c $\mid$ p

• 2. Change state from $s_0$ to $s_1$ and rewrite all a, b pairs into c’s, in the max-parallel mode, provided that at least one p is present:

  $s_0$ a b $\rightarrow _{+}$ $s_1$ c $\mid$ p

• 3. Change state from $s_0$ to $s_1$, rewrite one compound term a() by adding one 1 to its contents; variable X is unified to the actual contents of a.

  $s_0$ a(X) $\rightarrow _{1}$ $s_1$ $a(X\textit{1})$

  If the current a already has two copies of 1, i.e. $a({1}{1})$, then the result will be an updated copy with three 1’s, i.e. $a({1}{1}{1})$—thereby incrementing its base 1 contents.

• 4. Conditionally change state from $s_0$ to $s_1$, rewrite one compound term a() by removing one 1 from its contents, if there is at least one 1 among its contents.

  $s_0$ $a(Y1)$ $\rightarrow _{1}$ $s_1$ a(Y)

  For example, if the current a already has three copies of ${1}$, i.e. $a({1}{1}{1})$, the result will be an updated copy with two ${1}$’s, i.e. $a({1}{1})$—thereby decrementing its base 1 contents. The rule does NOT apply if the cell does not contain at least one 1.

• 5. A complex operation, highlighting the weak priority order, with resulting state depending on the current cell contents.

  $s_0$ a $\rightarrow _{1}$ $s_1$ e     (1)

  $s_0$ b $\rightarrow _{1}$ $s_2$ f     (2)

  $s_0$ c $\rightarrow _{1}$ $s_1$ g     (3)

  • (a) If the cell contains a and c, then rules (1) and (3) apply; new state: $s_1$, new contents: e and g.

  • (b) If the cell contains b and c, then only rule (2) applies; new state: $s_2$, new contents: f and c. Rule (3) is NOT applicable, because rule (2) has already set the target state to $s_2$.

  • (c) If the cell contains a, b and c, then only rules (1) and (3) apply; new state: $s_1$, new contents: e, b and g. Rule (2) is NOT applicable, because rule (1) has already set the target state to $s_1$.

• 6. Microsurgery is denoted by curly braces { } instead of round parentheses ( ) and enables processing of parts of the inner contents, without locking the rest [16]. Microsurgery allows us to use sub-cells in the same style as we use our own top cells, and also independent cells in other P systems variants. Without microsurgery, this will NOT be possible, because sub-cells do NOT have own rules—instead, their contents need to be manipulated solely by rules of their containing top cells.

  For example, the rules:

  $s_{0}$ $x\{ a \}$ $\rightarrow _{+}$ $x\{ b \}$

  $s_{0}$ $x\{ c \}$ $\rightarrow _{+}$ $x\{ d \}$

  applied to the term x(a a c c c e) will in one single step result in x(b b d d d e). Without microsurgery, this requires more steps and more complex rules.

  Note that microsurgical applications are already the default for top cells, where we do apply partial matching, without locking all the contents. However, for simplicity, we do not use explicit curly braces for the outermost top-cell. For example, these two rules would in fact be equivalent:

  $s_{0}$ a $\rightarrow$ $s_{0}$ b $\equiv$ $s_{0}$ a $\rightarrow$ $s_{0}$ b,

3 cP Solution and examples

In this section, we discuss our cP system for solving QSAT for $n \ge 1$, and we illustrate its evolution on Formulae (1, 2), recalled here:

$\forall x_{1} ~\exists ~x_{2} ~(x_{1} \vee x_{2}) \wedge (x_{1} \vee {\bar{x}}_{2})~~~~~~~~$ (1)

$\exists x_{1} ~\forall ~x_{2} ~(x_{1} \vee x_{2}) \wedge (x_{1} \vee {\bar{x}}_{2})~~~~~~~~$ (2)

We only use one single top-level cell, and we closely follow the parallel pseudocode algorithm listed in Table 3: a layer-by-layer sweep over a virtual tree, in two passes—first top-down and then bottom-up.

We use six states, $\{s_1, s_2, ..., s_6\}$, where $s_1$ is the initial state, and $s_6$ is the final. The ruleset is shown in two listings: the top-down pass in Table 9 and the bottom-up pass in Table 11. The evolution corresponding to Formula (1) is illustrated in the following tables: Table 8 shows the initial cell contents and state; then, Table 10 traces the top–down evolution, and Table 12 traces the bottom–up evolution. Table 13 traces the bottom–up evolution of the slightly different Formula (2).

3.1 Lookup tables

For efficiency, our cP solution uses two read-only “tables”. Four sub-cells y()()() form a lookup table for Boolean identity and negation operations. Table 6 shows their contents and their interpretation.

Eight sub-cells w()()()() form a lookup table for Boolean $\wedge$ and $\vee$ operations, the actual operation being selected on the corresponding quantifier. Table 7 shows their contents and their interpretation.

Table 6 Cells y form a lookup table for Boolean identity and negation operations: $V = \mathbf{if }$ $S=+ \mathbf{then }$ $K \mathbf{else }$ ${\bar{K}}$

Table 7 Cells w form a lookup table for Boolean $\vee$ and $\wedge$ operations: V = if $Q=\forall$ then $V'$ $\wedge$ $V''$ else $V'$ $\vee$ $V''$

3.2 Prefixes and tree levels

During the top-down pass, sub-cell $\nu ()$ is a counter that indicates the tree-level depth, initially $\nu (n)$, where n is the actual number of quantifiers (or variables).

Sub-cells p()(), q()() form 1-based associative arrays that encode the given prefix: p()() contains variables, q()() contains quantifiers. These sub-cells are used as “horizontal” (not nested) stacks, where the top is indicated by the current value of counter $\nu ()$. During the top-down pass, the top elements of p()() are temporarily popped into h(), and q()() is reversed into a similar “horizontal” stack, $q'()()$, whose top is indicated by counter $\mu ()$—stack $q'()()$ will be used in the bottom-up pass.

Stacks $p()(), q()(), q'()()$ closely match their namesake variables used in Table 3. Together with their associated counters, $\nu ()$ and $\mu ()$, these play the role of global variables controlling the two passes.

3.3 Literals encoding and formula sub-cells

Formula literals, i.e. variables and their negations, are given via sub-cells x()(). We use shorthand notations that closely match the mathematical expression and keep our expression crisp:

$x_{1} \equiv x({1})(+)$

${\bar{x}}_{2} \equiv x({1}{1})(-)$

This is just a notation convenience, and our rules actually assume the longer version when being matched.

Clauses are given via sub-cells c(), having literals as contents, with implicitly assumed Boolean or’s. For example:

$(x_{1} \vee {\bar{x}}_{2}) \equiv c(x_{1} {\bar{x}}_{2}) \equiv c( x({1})(+) ~x({1}{1})(-) )$

The contents of c()’s are multisets; thus, the order of literals is irrelevant, but we usually keep it in our listings, for more readability.

Unquantified formulae are given via sub-cells f(). Initially, sub-cells f() contain just multisets of clauses. For example, at the root of the virtual tree, the unquantified part of Formula (1) is encoded as:

$f(c(x_{1}~ x_{2}) ~ c(x_{1} ~{\bar{x}}_{2}))$

The contained clauses are partially evaluated during the top-down pass, and new contents appear in f() that indicate the path to the root and the final value.

Sub-cells a()() form a 1-based associative array that indicates a complete path to the root and are used as “horizontal” (not-nested) stacks, with the top indicated by the contents of counter $\nu ()$—similar to the above-mentioned global $q'()()$ sub-cells. For example, ignoring its other contents, a formula associated with the node on leftmost path 01 looks like this:

$f(... ~ a({1}{1})({1}) ~ a({1})(\textit{0}))$

The contents inside the first parentheses indicate the depths (here 2 and 1), while the content inside the second parentheses indicates the assigned values (here 1 and 0).

Note that the layers are processed in the order of variables given by the prefix—this will be discussed shortly. This need not be in increasing order, but usually is. Thus, the above a()’s may indicate the tree node for $x_1=0, x_2=1$, (Cf. Figures 1, 2).

The a()()’s are created during the top-down pass and effectively used during the bottom-up pass, to properly match sibling nodes.

At the tree leaves level, the formulae are completely evaluated and their values are stored in v() sub-cells. For example, under the above-mentioned sample assumptions:

$f(v(0) ... ~ a({1}{1})({1}) ~ a({1})(\textit{0}))$

$\Longleftrightarrow (x_1 \vee x_2) \wedge (x_1 \vee {\bar{x}}_2)[x_1:=0, x_2:=1] \equiv (0 \vee 1) \wedge (0 \vee {\bar{1}}) \equiv 0$

To help an efficient top-down formula substitution split, such as $[x_i=0]$ vs. $[x_i:=1]$, we also use temporary variants of f with two distinct arguments, f()().

Cells f() closely match their namesake variables used in Table 3.

Table 8 Contents of our top-level cell, as initialised for Formula (1): $\forall x_{1} ~\exists x_{2} ~(x_{1} \vee x_{2}) \wedge (x_{1} \vee {\bar{x}}_{2})$

3.4 Top–down pass

The rules for the top–down pass are listed in Table 9. Essentially, we have a loop consisting of three steps ($s_1 \rightarrow s_2 \rightarrow s_3 \rightarrow s_1$) that is repeated n times and a subsequent one-step evaluation ($s_{1} \rightarrow s_4$). These steps closely follow the top-down pass of the parallel algorithm presented in Table 3.

Rules (1, 2, 3) form an if then else construct. If we have not yet processed all quantifiers and variables, condition detected by a nonempty $\nu ()$ counter, then rule (1) applies, resetting our global control variables and starting one more loop iteration ($s_1 \rightarrow s_2$). Sub-cell h() is updated to the current variable to be substituted, say $h(x_i)$, and its associated quantifier is popped into stack $q'()()$, to be used in the bottom–up pass.

Otherwise, if the quantifiers and variables stacks are empty, we exit the loop via rules (2,3), applied in max-parallel mode. Formulae f() that after partial evaluations are false, detected by at least one empty c() clause are tagged by one $v(\textit{0}$) sub-cell. The other formulae, which are true, are tagged by one $v({1}$) sub-cell.

Together, rules (4,5,6) form the main body of the top–down loop ($s_2 \rightarrow s_3 \rightarrow s_1$). They run in max-parallel mode and create the next level down the tree, discarding the current level. Each formula f() is split into two children formulae, by two substitutions, $x_i := 0, x_i := 1$, and new a()() sub-cells are created, to record the corresponding tree paths. These paths tags a()() will be essentially used during the bottom–up pass, when these two children will be recognised as siblings and merged together (despite being here thrown into an unordered multiset).

Using the lookup table y()()(), rules (5,6) also perform straightforward partial evaluations, based on the values that are assigned to variable $x_i$.

Table 10 illustrates this top–down pass by traces for Formula (1), starting from the initial state shown in Table 8.

Table 9 Top–down rules. The three-step loop $s_1 \rightarrow s_2 \rightarrow s_3 \rightarrow s_1$ is repeated n times, followed by the exit $s_1 \rightarrow s_4$

Table 10 Top–down traces for Formula (1, $\forall ~\exists$). Continued from Table 8. (Cf. tree (b) in Figure 1)

3.5 Bottom–up evaluation

The rules for the top–down traversal pass are listed in Table 11. Essentially, we have a one-step transition from the top–down pass ($s_4 \rightarrow s_5$), followed by a one-step loop ($s_5 \rightarrow s_5$) that is repeated n times, and a one-step exit to the final state ($s_5 \rightarrow s_6$). These steps closely follow the bottom–up pass of the parallel algorithm presented in Table 3.

Rule (7) runs in max-parallel mode and performs a clean-up step ($s_{4} \rightarrow s_{5}$), removing unwanted material from all sub-cells f().

Rules (8,9,10) form a repeat until bottom–up loop, with the exit condition checked by rules (9,10). This works, as we assume that $n \ge 1$.

Rule (8) forms the main body of this bottom–up loop, $s_5 \rightarrow s_5$, that is repeated n times and runs in max parallel mode. This rule creates the next level up the tree, discarding the current level.

Each pair of sibling formulae f() is merged and evaluated, using the corresponding quantifier from stack $q'()()$ (which was saved during the top–down pass). Because we use multisets, we cannot a sequence-based pairing, as in Table 3. From all f()()’s in the current multiset content, siblings are grouped together according to their path to root records, given by their contained a()()’s. The evaluation is performed with the help from the look-up table w()()()().

Rules (9,10) form an if then else loop end check. If we are not yet at the root level, condition detected by a nonempty counter $\mu$, then rule (9) resumes the loop, $s_5 \rightarrow s_5$. Otherwise, rule (10) applies and exits, cleaning all remaining stuff and recording the final value in v().

Table 12 illustrates this bottom–up pass by traces for Formula (1, $\forall ~\exists$), starting from the end state shown in Table 12. The evolution for the related Formula (2, $\exists ~\forall$) is only marginally different, but still significantly in the bottom-up pass, when we actually use quantifiers; its bottom-up traces are shown in Table 13.

Table 11 Bottom–up rules. One-step loop $s_5 \rightarrow s_5$ repeated n times

Table 12 Bottom–up traces for Formula (1, $\forall ~\exists$). Continued from Table 10. Final result is false. (Cf. tree (c) in Figure 1)

Table 13 Bottom–up traces for Formula (2, $\exists ~\forall$). Continued from Table 10, with different $q'()()$’s. Final result is true. (Cf. tree (c) in Figure 2)

3.6 Analysis

Proposition 1

Our solution uses a custom alphabet size of 19.

The state alphabet is $\{ s_1, s_2, s_3, s_4, s_5, s_6 \}$.

Our custom alphabet is $\{ \exists , \forall , +, -, \textit{0}, {1}, f, c, q, q', p, x, h, y, w, \nu , \mu , a, v \}.$ $\square$

Proposition 2

Our solution uses a ruleset containing ten rules.

Top–down pass uses six rules (Table 9), and bottom–up pass uses four (Table 11), making a total of ten rules. $\square$

Proposition 3

Total runtime is $4n+3$.

Top–down runtime (Table 9): The top–down loop $s_1 \rightarrow s_2 \rightarrow s_3 \rightarrow s_1$ runs n times. The transition $s_{1} \rightarrow s_4$ runs once, making this pass take $3n+1$ steps.

Bottom–up runtime (Table 11): The transitions $s_{4} \rightarrow s_{5}$ and $s_{5} \rightarrow s_{6}$ run once. The bottom–up loop $s_{5} \rightarrow s_{5}$ runs n times, making this pass take $n+2$ steps.

Thus, the total runtime is ${\mathcal {O}}(n)$ = $4n+3$. $\square$

Proposition 4

The evolution of our ruleset is totally deterministic.

Rules that are applicable exactly once ($\rightarrow _1$) use singleton terms and do not allow any possible choice. Rules that are applicable in the max-parallel mode ($\rightarrow _+$) make the same multiset transformations, regardless of any hypothetical application order. $\square$

Proposition 5

Maximum membrane nesting depth is 6.

The largest nesting depth in Table 10 occurs in:

$$\begin{aligned}&f(\textit{0})(c(x_{2}) ~ c({\bar{x}}_{2}) ~ a({1}{1})(0) ~ a({1})(\textit{0})) \\&\quad \equiv f(\textit{0})(c(x({1}{1})(+)) ~ c(x({1}{1})(-)) ~ a({1}{1})(0) ~ a({1})(\textit{0})) \end{aligned}$$

and other similar cells. Denoting nesting depth by $\delta$, we have: $\delta (f)=1$, $\delta (c)=3$, $\delta (x)=4$, $\delta (+)=6$. This example is for $n=2$; however, for larger n, the nesting depth will NOT increase, but rather the “horizontal” number of cells at existing levels. $\square$

4 Conclusion and future work

We have presented an efficient deterministic cP solution to QSAT that runs in $4n+3 = {\mathcal {O}}(n)$ steps, at same order of magnitude as the other P system solutions. However, in contrast to other confluent P system solutions, our cP solution uses a small constant alphabet size (19), a small constant number of rules (10) and very small constant membrane nesting depth (6), independent on the problem size.

We conclude by noting the following open problems, which may need further investigations: Is it possible to design an equivalent cP system, still deterministic, “with an even smaller nesting depth bound, e.g. three or even two?

How would non-confluent designs affect the power of cP systems? Are cP system inhibitors really needed? We note that our solution does not use any, and the presence of inhibitors will likely negatively affect the simulation runtime on existing hardware and software platforms.

Is a sub-linear runtime solution possible, using cP systems and/or another P systems variant? We note this can be viewed as seeing whether cP systems agree with the parallel computation thesis [15]. This also leads to the question on whether or not cP systems are polynomial equivalent to the other P system variants.