On the Enumeration of Signatures of XOR-CNF’s

Propositional formulas are ubiquitous in computer science. The complexity of the satisfiability problem has been extensively studied from the point of view of several algorithmic tasks such as decidability, counting, or enumeration to mention but a few. Given a CNF formula $\phi$ with clauses $C_1,\mathrm{\dots },C_m$ over a set of variables $V=\{v_1,\mathrm{\dots },v_n\}$, a truth assignment $𝐚:V\to \{0,1\}$ leads to a binary sequence ${\sigma }_{\phi }(𝐚)$, called a signature of $\phi$, defined by ${\sigma }_{\phi }(𝐚)=(C_1(𝐚),\mathrm{\dots },C_m(𝐚))$ where $C_i(𝐚)=1$ if clause $C_i$ evaluates to 1 under assignment $𝐚$, and $C_i(𝐚)=0$ otherwise. Deciding the satisfiability of $\phi$ boils down to deciding whether the all-one sequence is a signature of $\phi$.

In this paper, we investigate the problems of listing all, minimal, and maximal signatures of a CNF, where minimal and maximal are meant bitwise. The task of finding all signatures of a CNF originates from well-designed pattern trees and has first been posed during the Dagstuhl Seminar on enumeration in data management [5]. However, enumerating the signatures of a given CNF – may it be all, minimal, or maximal ones – will generally produce an exponential number of solutions. Therefore, input sensitive complexity is not a suitable yardstick of efficiency when analyzing enumeration algorithms performance. Instead, output-sensitive complexity estimates the running time of an enumeration algorithm using both input and output sizes. In that framework, an algorithm is considered tractable when it runs in total-polynomial time (or output-polynomial time), that is, if its execution time is bounded by a polynomial in the combined size of the input and the output. Still, further constraining this notion to guarantee some regularity in the enumeration is sometimes desirable. For this reason, polynomial delay and incremental-polynomial time are customarily regarded as better notions of tractability for enumeration complexity. On the one hand, polynomial delay means that the delay between consecutive outputs is polynomial in the input size. Incremental-polynomial time, on the other hand, means that the time to produce the $i^{\text{th}}$ solution is bounded by a polynomial in the input size plus $i$ (see e.g., [17, 22]).

Generating all the signatures of a CNF turns out to be of great fundamental interest, for it is an example of enumeration problem which can be solved in total-polynomial time even though solutions cannot be recognized in polynomial time.¹¹1These problems thus lie outside of the class EnumP which is commonly studied in algorithmic enumeration; see e.g. [22]. In a recent contribution [2], Bérczi et al. investigate this problem. They give an incremental-polynomial time algorithm for listing all the signatures of a $k$-CNF for fixed $k$, and show that for tractable CNF’s, signatures can be enumerated with polynomial delay. On the other hand, they show that generating maximal signatures is hard, while minimal signatures can be listed with polynomial delay, regardless of the CNF under consideration. Their positive result relies on the equivalence with maximal independent sets enumeration in graphs, known to be tractable [23]. As of their hardness result, it relies on the fact that the existence of at least two solutions would imply the non-satisfiability of the CNF at hand. Thus, the difficulty of the enumeration heavily relies on the intractability of the satisfiability of CNF’s in general. This observation naturally leads to the following open question, where by tractable CNF’s we mean families of CNF’s for which the satisfiability of a formula $\phi$ in the family (as well as its sub-formulas) can be decided in polynomial time.

Among tractable formulas, Horn and 2-CNF’s are two natural candidates for approaching Question 1. These two cases however proved to be very challenging, and the question of their tractability was explicitly stated as an open problem in the 2022’s edition of the Workshop on Enumeration Problems and Applications (WEPA’22).

Another natural step toward answering Question 1 is to consider XOR-CNF formulas, being conjunctions of clauses using the “exclusive-or” connective instead of the usual “or” connective. XOR-clauses were revealed in Schaefer’s famous complexity classification as a tractable case for deciding the satisfiability of a set of generalized clauses [21]. Interestingly, XOR-clauses are the only ones that lead to a tractable case when it comes to counting the number of satisfying assignments [11]. They subsequently appeared in many Schaefer-like classifications for a variety of algorithmic tasks, including enumeration [10, 14]. The success of XOR-clauses is due to their algebraic properties. Indeed, a set of such clauses can be seen as a system of linear equations over the 2-element field. As a result, the sets of satisfying assignments of such subsets are affine subspaces, and they allow for algebraic tools such as Gaussian elimination and matroid algorithms. Also in the special case of 2-XOR clauses, subsets of clauses can be interpreted as graphs with 0/1-labeled edges and benefit from several efficient graph algorithms, e.g., for computing connected components or identifying cycles [14]. This ability to capture XOR clauses using algebraic, matroid, and graph concepts and methods provides efficient tools for analyzing their behavior with respect to our enumeration problem.

Note that these formulas do not fall in the framework of CNF’s though. Indeed, rewritting an XOR-CNF as a CNF may result in a blowup on the number of clauses and signatures, as discussed in Section 2. Hence, we remark that the positive results from [2] do not directly apply to XOR-CNF. Yet, we show that signatures enumeration remains tractable using flashlight search as it is done in [2]. Namely, we prove the following.

Concerning the enumeration of minimal signatures, we show that the problem is in fact equivalent to the case of listing maximal signatures.

This leaves us with the study of maximal signatures enumeration for XOR-CNF’s. Quite surprisingly, we prove this problem to relate well with other problems from graph theory and matroid theory. Specifically, we show the case of 2-XOR-CNF to generalize maximal bipartite subgraphs enumeration, a problem which was recently shown to admit a polynomial-delay algorithm [6]. As of the general case of XOR-CNF’s, it can be seen as listing all maximal satisfiable subsystems of a linear system of equations, which is related to the enumeration of circuits passing through a given element in a matroid [4]; see also [18, 19]. Relying on these results, we derive that maximal signatures enumeration for XOR-CNF’s is tractable. Namely, we obtain the following.

Concerning the case of 2-XOR-CNF, we show it to be even more tractable, that is, we show that it can be solved with polynomial delay using proximity search.

To prove Theorem 4, we represent the input 2-XOR-CNF as an edge-bicolored multigraph where each color codes the parity of the XOR clause. Then, the enumeration amounts to list maximal bipartite subgraphs with additional constraints on colored edges.

A caveat of Theorems 3 and 4 is that a queue of solutions has to be maintained in the generation. More precisely, in [4] the queue is needed to generate a new solution as the algorithm uses the saturation technique where new solutions are derived from obtained ones. In [6], the queue has the other purpose of preventing repetitions. In both cases, getting rid of a potentially exponential space use is a natural enhancement one may seek. It should however be noted that improving the algorithm from [4] to get polynomial space is open for two decades now. As of improving Theorem 4 to use polynomial space, it would imply such a result for maximal bipartite subgraphs enumeration, another open question [6]. Toward such directions, we prove that the folklore technique of flashlight search used to obtain Theorem 1 may probably not be of great use as deciding whether a subsequence of clauses can be extended into a signature is NP-complete.

All the objects considered in this paper are finite. If $V$ is a set, ${\mathrm{𝟐}}^V$ is its powerset. Let $m\in \mathbb{N}$ and let $\sigma \in {\{0,1\}}^m$ be a binary sequence. We write $\sigma [i]$ to denote the value of the $i^{\text{th}}$ element of $\sigma$. It will be furthermore convenient to note $\mathrm{𝟏}(\sigma )$ the set of indices $I\subseteq \{1,\mathrm{\dots },m\}$ whose corresponding values in $\sigma$ is 1; $\mathrm{𝟎}(\sigma )$ is defined analogously. The complementary of $\sigma$ is the binary sequence $\overline{\sigma }$ obtained from $\sigma$ by flipping all the bits, i.e., $\overline{\sigma }[i]=1+\sigma [i]$ (mod $2$) for $1\le i\le m$. If $\sigma ,\tau \in {\{0,1\}}^m$, we write $\sigma \le \tau$ if $\sigma [i]\le \tau [i]$ for all $1\le i\le m$. In other words, $\le$ corresponds to the bitwise order, and we write if $\sigma \le \tau$ and $\sigma \ne \tau$.

We prove that testing whether a binary sequence is a signature (resp. minimal signature, maximal signature) of an XOR-CNF can be done in polynomial time in the size of the CNF at hand, and use it to show that listing all signatures of an XOR-CNF is tractable. For the rest of the section, let us fix some XOR-CNF $\phi =C_1\wedge \mathrm{\cdots }\wedge C_m$ on variable set $V=\{x_1,\mathrm{\dots },x_n\}$. A preliminary step is the following.

From Proposition 5 we already derive Proposition 2.

Given two disjoint subsets $A,B\subseteq \{1,\mathrm{\dots },m\}$, we define

to be the formula obtained from $\phi$ by taking the clauses with index in $A$ and the negation of clauses with index in $B$. We furthermore set this formula to be defined on variable set $V(\phi )$ even though some variables in $V(\phi )$ may not appear in any of the clauses of $\phi (A,B)$ – we want this to ensure that assignments of $\phi (A,B)$ are well-defined for $\phi$. Remark that the size of $\phi (A,B)$ is at most that of $\phi$, and that it is defined on precisely $m$ clauses whenever $A,B$ is a bipartition of $\{1,\mathrm{\dots },m\}$. In the next proposition, we show that testing whether a binary sequence is a signature of an XOR-CNF can be reduced to satisfiability testing.

Note that signatures are neither closed by subset or superset, i.e., they may exist binary words such that $\sigma ,\rho$ are signatures but not $\tau$. We nevertheless show that testing the minimality (or maximality) of a signature can be done locally in polynomial time.

To conclude this section, we argue that enumerating all the signatures of an XOR-CNF is tractable using the above properties and flashlight search. We recall that the main idea of this technique is to conduct binary search over the space of solutions. In order for flashlight search to run with polynomial delay and polynomial space, it is sufficient to solve the so-called “extension problem” in polynomial time: given two disjoint subsets $A,B$ of the ground set, decide whether there exists a solution including $A$ and avoiding $B$. We refer to e.g. [3, 20] for a more detailed description of this folklore technique.

In the case of XOR-CNF signatures, $A$ will consist of indices of clauses to be satisfied in the signature – the 1’s in the sequence – while $B$ will consist of indices of clauses not to be satisfied – the 0’s in the sequence. Then, it follows from the discussion above that $\phi$ admits a signature $\sigma$ satisfying $\sigma [i]=1$ and $\sigma [j]=0$ for all $i\in A$ and $j\in B$ if and only if $\phi (A,B)$ is satisfiable. Indeed, a satisfying assignment $𝐚$ of $\phi (A,B)$ satisfies the clauses of $\phi$ with index in $A$, and not those with index in $B$. Thus the signature of $\phi$ produced by $𝐚$ meets the requirements. As for the converse direction, it follows directly from the definition of a signature. We conclude by Proposition 7 that the extension problem can be solved in polynomial time for XOR-CNF signatures, hence proving Theorem 1 that we recall here.

We point out that Theorem 1 is not a direct consequence of [2, Theorem 1]. Indeed, in the latter theorem the authors consider families of tractable CNF’s which do not contain XOR-CNF’s in general. The arguments, however, follow the same line.

We investigate the complexity of enumerating the maximal signatures of a given XOR-CNF. More precisely, we prove the general case to be solvable in incremental-polynomial time by a result of Boros et al. [4], and the 2-XOR-CNF case to be solvable with polynomial delay using proximity search.

In Section 2 we have mentioned that the clauses of a given XOR-CNF $\phi$ may be seen as linear equations $x_1+\mathrm{\cdots }+x_k=\epsilon$, $\epsilon \in \{0,1\}$ over the two-elements field ${𝐅}_2$. Hence $\phi$ can be seen as a system of linear equations whose maximal feasible subsystems correspond to its maximal signatures. In [4], the authors present an incremental polynomial-time algorithm for enumerating all circuits of a matroid containing an element, and more generally, one for enumerating all maximal subsets not spanning an element. Using Farkas’ lemma (more precisely the Fredholm alternative) we can derive an algorithm which, given an infeasible system of linear equations, enumerates all its maximal feasible (or minimal infeasible) subsystems within the same time; see also [19, 18] on the use of this characterization of infeasible systems. This immediately yields Theorem 3.

We now focus on 2-XOR-CNF’s. Recall from Section 2 that we can consider these formulas as a set of 2-clauses of the form $x=y$ or $x\ne y$ for positive literals $x,y$ only, together with a set of 1-clauses $(z)$ with $z$ a positive or negative literal. Furthermore we may assume that no clause is repeated in the formula, as far as signatures enumeration is concerned. We shall call graphic a 2-XOR-CNF with clauses of the first type only – that is, without 1-clauses – and will assume for now on that our XOR-CNF’s are graphic. Later, we will show how to deal with 1-clauses with small modifications on the instance.

We start by defining an underlying multigraph structure of graphic 2-XOR-CNF that will be convenient for applying the framework of proximity search. Given such an XOR-CNF $\phi$ we define $G(\phi )$ (or simply $G$ when it is clear from the context) as the edge-bicolored multigraph defined on vertex set $V(\phi )$ and where there is a blue edge $xy$ whenever $x\ne y$ is a clause of $\phi$, and a red edge $xy$ whenever $x=y$ is a clause of $\phi$. A same pair of variables $x,y$ can produce both a red and a blue edge: this corresponds to having clauses $x=y$ and $x\ne y$ in $\phi$ which typically makes it unsatisfiable. However as no clause is repeated in $\phi$, no two edges of a same color share the same endpoints. In other words, our multigraph has edge multiplicity at most two, and two edges between a same pair of endpoints means that one is blue and the other is red; see Figure 1 for an example of such a multigraph. In the following, we will label edges of $G$ as $e_1,\mathrm{\dots },e_m$ so that the edge $e_j$ corresponds to the clause $C_j$ in $\phi$. We denote by $R(G)$ the set of red edges of $G$, and $B(G)$ the set of its blue edges. Observe that by definition, $R(G)$ and $B(G)$ define a bipartition of the edge multiset of $G$. In other words, it is convenient to see $R(G)$ and $B(G)$ as partitioning the set of indices of the edges $e_1,\mathrm{\dots },e_m$ of $G$. In the following, when noting $E\subseteq F$ for two edge multisets of $G$, we mean inclusion of the indices of their edges, that is, by $E\subseteq F$ we mean $I(E)\subseteq I(F)$ for $I(F)\subseteq \{1,\mathrm{\dots },m\}$ denoting the set of indices of the edges in $F$.

In the rest of the section, by subgraph of an edge-bicolored multigraph $G$ we mean a graph $H$ with $E(H)\subseteq E(G)$ and $V(H)\subseteq V(G)$ where $V(H)$ contains at least the vertices involved in the edges of $E(H)$. For convenience, we may as well refer to a subgraph by its edge set, in which case we assume its vertex set to be the one induced by the endpoints of its edges. Finally, given two disjoint subsets $X,Y$ of a graph $G$, by ${\delta }_G(X,Y)$ we mean the set of edges having an endpoint in $X$ and the other in $Y$, and may drop $G$ from the subscript if no ambiguity arises.

Note that an arbitrary (simple, uncolored) graph $H$ is bipartite whenever it admits a bipartition $(X,Y)$ of its vertex set with $E(H)=\delta (X,Y)$. In the next lemma, we relate the satisfiability of a graphic 2-XOR-CNF to a property of its underlying edge-bicolored multigraph which generalizes bipartiteness. Observe that this property is only stated on blue edges, which is still reasonable as blue and red edges partition the edges of the multigraph.

We derive the following analogue for signatures, where by maximal subgraph we refer to edge inclusion.

In the following, given an edge-bicolored multigraph $G$, we call red-blue bipartite any of its subgraph $H$ admitting a bipartition $(X,Y)$ of its vertex set such that $\delta (X,Y)=B(H)$. In Figure 2, we give an example of a maximal red-blue bipartite subgraph $H$ of the multigraph $G$ of Figure 1. Note that red-blue bipartite subgraphs do not contain both a red edge and a blue edge between a same pair of vertices, i.e., they define edge-bicolored graphs.

A consequence of Theorem 10 is that the enumeration of maximal signatures of a 2-XOR-CNF only consisting of disequalities $x\ne y$ is equivalent to the enumeration of maximal (edge) bipartite subgraphs of a given graph. Indeed in that case, $R(G)$ is empty – hence $G$ is a graph – and we only require $E(G)=\delta (X,Y)$. We derive the following using a recent result by Conte and Uno [6] on maximal bipartite subgraphs enumeration by proximity search.

We end the section showing that the result from [6] can be extended into our context using proximity search, and arguing how to capture clauses of size one.

In the following, we say that an edge-bicolored multigraph $G$ is connected if its underlying graph (where colors are ignored and multi-edges are considered as a single edge) is connected. Note that we can assume without loss of generality that $G(\phi )$ is connected, as far as signatures enumeration is concerned. Indeed, if it was not the case we could enumerate the signature of each subformula of $\phi$ corresponding to connected components of $G(\phi )$ and combine the results by doing their Cartesian product. Hence, we may further assume that $G(\phi )$ is connected, and shall call connected a formula such that its underlying multigraph is. We first show that if $G$ is connected then its maximal red-blue bipartite subgraphs are as well, yielding a canonical bipartition.

Proximity search has been introduced in [7] as a special case of solution graph traversal in which the proof that the solution graph is strongly connected relies on a notion of proximity between solutions that is more involved than their intersection. More precisely, the proximity between two solutions $S,S^{\ast }$ is defined as the length of the longest prefix of $S^{\ast }$ (according to a carefully chosen ordering of its elements) that is subset of $S$, and needs not to be symmetric. We refer to [6] for more details on the technique. In [6], the authors extract the necessary conditions that make an enumeration problem “proximity searchable” and thus to be solvable with polynomial delay. We restate these conditions here in the context of XOR-CNF for self-containment and better readability.

In the reformulation below, let $G$ be an edge-bicolored multigraph and $\mathscr{H}(G)$ denote the set of maximal (connected) red-blue bipartite subgraphs of $G$ we shall call maximal solutions. We further call solutions the connected red-blue bipartite subgraphs of $G$.

The rest of the section is dedicated to proving that the conditions of Theorem 14 are fulfilled for well-chosen $\mu$ and set $𝒦$. The fact that $\mathrm{COMP}$ can be computed in polynomial time follows from the fact that the red-blue bipartiteness is a hereditary property which can be tested in polynomial time, hence that we can greedily obtain a maximal solution.

We start with the definition of $\mu$. Given a maximal red-blue bipartite graph $H$ of $G$ we denote by $(H_0,H_1)$ the unique bipartition given by Lemma 13 where $H_0$ is the side containing the vertex $v_0$ of smallest index in $G$. Consider a BFS ordering of the vertices of $G$ initiated at $v_0$: we start with $v_0$ which is unmarked, and at each step, we iteratively consider unmarked vertices ordered so far, and, in order, we mark them and append the unmarked vertices of their neighborhoods in ascending order of their label. Clearly, each prefix of such an ordering defines a connected (vertex) induced subgraph. We define $\mu (H)$ as the increasing ordering of the edges of $H$ with respect to their endpoint occurring later in the BFS ordering launched at $v_0$, and break the tie by increasing order of their earlier endpoint in the BFS; see Figure 3 for an example of such an edge-ordering. This choice of an edge-ordering of a maximal solution yields the following property which will be crucial in the rest of the proof, and from which, intuitively, we will obtain that pairs of solutions $H,H^{\ast }$ must agree on their respective bipartition of the elements in $H\tilde{\cap }{H}^{\ast }$.

Let us now consider arbitrary $H,H^{\ast }\in \mathscr{H}(G)$ and put $H^{\prime }:=H\tilde{\cap }{H}^{\ast }$ as defined in Theorem 14. Note that if $H^{\prime }$ is empty then the trivial removable $K=E(G)$ satisfies the above conditions. Hence we may assume for convenience (in the rest of the analysis) that $|H\tilde{\cap }{H}^{\ast }|\ne 0$, while it will appear clear later that this assumption is in fact not needed. By Observation 15 since the first edge in $\mu (H^{\ast })$ belongs to both $H^{\prime }$, $H$ and $H^{\ast }$ we derive that $v_0$ belongs to all three graphs. Again by Observation 15, $H^{\prime }$ is a connected red-blue bipartite subgraph of $G$. Thus by Lemma 13 it admits a unique bipartition $(H_0^{\prime },H_1^{\prime })$ with blue edges lying between $H_0^{\prime }$ and $H_1^{\prime }$, and such that $v_0\in H_0^{\prime }$. Now since $H$ and $H^{\ast }$ contain $H^{\prime }$ they must agree with that bipartition, meaning that $H_0^{\prime }\subseteq H_0\cap H_0^{\ast }$ and $H_1^{\prime }\subseteq H_1\cap H_1^{\ast }$, where $(H_0^{\ast },H_1^{\ast })$ denote the unique bipartition of $H^{\ast }$ such that $v_0\in H_0^{\ast }$ as provided by Lemma 13. In the following, for each edge $e=ab$ in $E(G)\setminus E(H)$, we use the edges incident to the vertices of $e$ to build the removables. More precisely, we define $K_1:=\{av:av\in E(G)\}$ and $K_2:=\{bv:bv\in E(G)\}$ to be the two removables of $(H,e)$ and argue that $𝒦:=\{K_1,K_2\}$ meets the requirements of the theorem. We stress the fact that in $K_1$ or $K_2$ we may find edges lying in both $H$ and $H^{\ast }$, which is not a problem; rather, we will argue that, when choosing $e$ as the minimal element of $\mu (H^{\ast })$ not in $H$, one of $K_1$ or $K_2$ will be disjoint from $H\tilde{\cap }{H}^{\ast }$, hence that $𝒦$ defines a valid set of removables.

Consider the first edge $e=ab$ in $\mu (H^{\ast })$ that is not an edge of $H$. We distinguish two symmetric cases depending on whether $e$ is red or blue, and only detail the blue case here. This situation is depicted in Figure 4.

We assume without loss of generality that the endpoint $a$ belongs to $H_0^{\ast }$ and that the other endpoint $b$ lies in $H_1^{\ast }$. Recall that $e\notin H$. Since $H$ is maximal, it is connected by Lemma 12, so that $a,b$ lie in $V(H)$. Hence since $e$ is blue, either the two endpoints $a,b$ belong to $H_0$, or they both belong to $H_1$. Two symmetric cases arise. Let us assume $\{a,b\}\subseteq H_0$, as depicted in Figure 4. Note that in $H^{\ast }$ we have no blue edge between $b$ and $H_1^{\prime }$, and no red edge between $b$ and $H_0^{\prime }$. In $H$ this is the opposite: we have no blue edge between $b$ and $H_0^{\prime }$, and no red edge between $b$ and $H_1^{\prime }$. Now as $E(H^{\prime })\subseteq E(H^{\ast })\cap E(H)$ we conclude that $b$ is not incident to blue or red edges in $H^{\prime }$, that is, $E(H^{\prime })\cap K_2=\mathrm{\varnothing }$. This concludes the case and the other situation of $\{a,b\}\subseteq H_1$ yields the symmetric situation of $E(H^{\prime })\cap K_1=\mathrm{\varnothing }$ by the same arguments. The other situation of $e$ being red follows the exact same arguments, swapping red for blue. Hence, for one of $K_1$ or $K_2$ we have that $(H\tilde{\cap }{H}^{\ast })\cap K=\mathrm{\varnothing }$, as required by the last condition of Theorem 14.

We finish the proof observing that the graphic conditions of 2-XOR-CNF’s can be relaxed. As a preliminary step, note that 1-clauses containing variables that do not appear in 2-clauses can be removed from the instance as they will be set to true in any maximal signature. Thus we may assume that $\phi$ does not contain such isolated 1-clauses. We code every other 1-clauses $(x)$ and $(\overline{y})$ – which can also be seen as clauses $x=1$ and $y=0$ – by a blue edge $xu$ and a red edge $yu$ in the edge-bicolored multigraph $G$ we have defined above, for some special additional vertex $u$ that will be connecting all such 1-clauses. Note that $G$ stays connected by the above assumption that $\phi$ has no isolated 1-clause. Then we set $u$ to be the vertex of smallest label in $G$, followed by $v_0$. Then by the definition of $\mu (H)$ the vertex $u$ will be placed in $H_0$ which can be seen as forcing the gadget to false, satisfying the clause $y=0$ if the red edge $uy$ is selected, and satisfying the clause $x=1$ if the blue edge $ux$ is selected. We conclude with Theorem 4 as a consequence of Theorem 14 and the above discussion.

In this work we have showed that enumerating all (resp. minimal, maximal) signatures of an XOR-CNF formula is tractable, namely, Theorems 1, 3 and 4. Observe that the algorithm of Theorem 3 runs in incremental-polynomial time while the other two run with polynomial delay. Hence it is natural to ask whether Theorem 3 can be improved to polynomial delay.

The algorithm by Boros et al. [4] underlying Theorem 3 relies on the enumeration of the circuits of a matroid, for which the same question seems open since two decades. Hence, answering Question 2 would either require new techniques, or would need to answer the open question from [4] in the Boolean case. A natural first step is to handle the case of $k$-XOR-CNF’s for fixed values of $k\ge 3$.

Furthermore, except for Theorems 1 and 3 that run with polynomial space, the algorithm of Theorem 4 requires a space that is potentially exponential as solutions must be stored into a queue. A natural question is the following.

We however stress the fact that a positive answer to Question 3 would improve the algorithm by Conte et al. for maximal bipartite subgraphs enumeration for which the questions of achieving polynomial delay and space is open [6].

Toward this direction, we now argue that flashlight search may not be adapted in order to give a positive answer to Question 3, as the extension problem is hard in that case. Moreover, this result even holds when restricted to 2-XOR-CNF’s consisting of disequalities, that is, in the context of maximal bipartite subgraph enumeration, which may be of independent interest.

Concerning prospective research directions, let us restate here the implicit question from [2] that motivated this work, which additionally was posed at the WEPA’19 open problem session, and that is still open to date. Recall that a family of CNF’s is tractable if there exists a polynomial-time algorithm to decide the satisfiability of any formula (and its subformulas) in the family.

Natural examples of tractable CNF’s include 2-CNF’s and Horn CNF’s for which, to the best of our knowledge, no progress has been made. Toward this direction, the case of Horn 2-CNF also seems open.

Another question left open by the work of Bérczi et al. deals with the dimension of the formula, defined as the maximum size of a clause it contains. Namely, the algorithm of [2, Theorem 4] only performs in incremental-polynomial time for fixed dimension, and it is open whether the same result can be obtained for formulas of arbitrary dimension.

Finally, another promising direction is the parameterized study of signatures enumeration. More particularly, it can be seen that the algorithm of [2, Theorem 4] is XP-incremental parameterized by the dimension $k$, that is, it generates the $i^{\text{th}}$ solution in time ${(\Vert \phi \Vert +i)}^{f(k)}$ for some computable function $f$. It would be interesting to know whether this algorithm can be improved to run with FPT-delay, that is, to run with $f(k)\cdot {\Vert \phi \Vert }^{O(1)}$ delay; see e.g. [15, 13, 12, 16, 1] for more details on the parameterized aspects of enumeration problems. A preliminary step in that direction would be to get such running times for a double parameterization. Among parameters, the maximum occurrence $\omega$ of a variable in the formula is natural. This parameter is relevant as in [2, Theorem 3] the authors give a simpler algorithm for signatures enumeration when both $k$ and $\omega$ are bounded. Improving this XP-incremental algorithm into one that run with FPT-delay parameterized by $k$ plus $\omega$ seems open.