1 Introduction↩︎

The Boolean satisfiability problem (Sat) is a central decision problem in theoretical computer science. Given a Boolean formula in conjunctive normal form (CNF), the problem asks whether there exists an assignment that satisfies all clauses. Cook’s seminal result established that Sat is NP-complete [1], and the problem has since served as a benchmark for studying computational hardness.

A common approach to gaining a finer understanding of the complexity of Sat is to study restricted subclasses of CNF formulas. By imposing syntactic or structural constraints, the resulting satisfiability problem may become tractable.

A well-known example for such a jump is the restriction to clauses of size two: While 3-Sat is NP-complete, 2-Sat is solvable in polynomial time [2]. Further restrictions, such as bounding the number of variable occurrences, can render the problem trivial in the sense that every restricted formula is either always satisfiable or always unsatisfiable. Tovey showed that any CNF formula with clause size \(r\) in which each variable occurs at most \(r\) times is always satisfiable [3]. More recent work in this direction—aimed at identifying tractable or in particular trivial subclasses—has explored restrictions on the graph representation of formulas [4] and on the number of potential conflicts arising from truth value assignments [5].

Among the restricted variants of Sat, monotone formulas—formulas in which each clause contains either only positive or only negative literals—have received considerable attention. Since Monotone 3-Sat is NP-complete [6], [7], monotonicity alone does not suffice to render satisfiability easy. Consequently, additional restrictions are required to identify subclasses where satisfiability is guaranteed.

In the monotone setting, particular attention has also been paid to formulas where the number of occurrences of each variable is explicitly bounded. Darmann, Döcker, and Dorn [8] show that Monotone 3-Sat remains hard if each variable appears exactly four times. Darmann and Döcker [9] distinguish positive and negative occurrences of the variables. They study the class Monotone 3-Sat-\((p,q)\), consisting of monotone 3-CNF formulas in which each variable occurs exactly \(p\) times positively and \(q\) times negatively, and obtain hardness results for every fixed pair \((p, q)\) with \(p \geq 2\) and \(q \geq 2\), as well as for the case that each variable appears exactly three times positively and once negatively, or three times negatively and once positively.

They also show that Monotone 3-Sat-\((k,1)\) is NP-complete for \(k \geq 5\), and pose the question of the complexity of Monotone 3-Sat-\((k,1)\) with \(k < 5\). By a result of Tovey [3], the problem is trivial for \(k\leq 2\), but the cases \(k\in \{3,4\}\) remained open. This question is particularly intriguing as it probes the precise threshold between hardness and guaranteed satisfiability within a structurally simple class of formulas.

In this paper, we resolve the open question of Darmann and Döcker by proving that all instances of Monotone 3-Sat-\((k,1)\) with \(k \leq 4\) are satisfiable, establishing that the satisfiability problem for this class is trivial. Our proof introduces a new combinatorial framework, called a color structure, which captures the interaction between positive and negative clauses under bounded variable occurrences. We present an algorithm that iteratively builds such a color structure from a given monotone formula with bounded occurrences running in \(\mathcal{O}(n \cdot m)\) time, where \(n\) and \(m\) denote the number of negative and positive clauses of the input formula, respectively. We prove correctness of the algorithm and show that a satisfying assignment can be extracted directly from the resulting color structure.

2 Definitions and Notation↩︎

Let \(x_1, x_2 , \dots\) be Boolean variables taking values in \(\{{\texttt{true},\texttt{false}}\}\). A literal is either a variable \(x_i\) or its negation \(\overline{x_i}\). A clause is a disjunction of literals, and a formula is in conjunctive normal form (CNF) if it is a conjunction of clauses. If every clause in a CNF formula contains exactly \(k\) literals, the formula is called a \(k\)-Sat formula. A variable occurrence is a specific appearance of a variable in a clause of the formula, possibly negated, and possibly appearing multiple times. A CNF formula is monotone if every clause consists entirely of positive literals or entirely of negative literals. Accordingly, the clauses of a monotone CNF-formula partition into positive clauses, containing only unnegated variables, and negative clauses, containing only negated variables.

We further bound the number of variable occurrences. The class Monotone 3-Sat-\((p,q)\) consists of all monotone 3-Sat formulas in which each variable occurs exactly \(p\) times positively and exactly \(q\) times negatively. Analogously, Monotone 3-Sat-\((\leq p,\leq q)\) consists of all monotone 3-Sat formulas in which each variable occurs at most \(p\) times positively and at most \(q\) times negatively. Throughout this paper, we consider instances of Monotone 3-Sat-\((\leq k,1)\) or Monotone 3-Sat-\((k,1)\) for \(k \in \{3,4\}\).

To simplify such formulas, we encode the information carried by negative clauses by a color (denoted by a letter) and say that variables in the same negative clause have the same color. If two (unnegated) variables have the same color, we call them relatives. A variable is not its own relative. Since the negated literals occur exactly once, we omit them and carry this information into the positive clauses via their respective colors. The simplified formula consisting of positive (and colored) clauses only is called a colored formula. Note that coloring a formula imposes an order on the variables that appear in the formula. We say that a variable is smaller than another variable if the letter corresponding to its color appears earlier in the alphabet or, if both variables have the same color, if the index of the variable is smaller. If we want to explicitly highlight that the order and letter is not relevant, we use \(u_i, v_j\) and \(l_s\) as variable names.

Central to our approach is the notion of guards. A guard is a variable that is explicitly chosen to be assigned to the value false. Intuitively, the set of guards represents the choices we make in constructing the assignment. A negative clause is satisfied if and only if at least one of its variables is assigned the value false. We may therefore assume, without loss of generality, that any satisfying assignment sets exactly one variable per negative clause to false: if more than one variable in some negative clause was set to false, the assignment of the excess false variables could be flipped to true without harming satisfiability. Therefore, the negative clauses of a formula are satisfied if there is exactly one guard for each color. We say that a variable is unguarded if it is not a guard and there is no relative of the variable that is a guard. To reason about a formula and a variable assignment simultaneously, we introduce a combined representation called a color structure. A colored monotone 3-Sat-\((\leq k, 1)\) formula and a corresponding assignment can be translated into a color structure and the other way around.

Note that not all variables of the formula need to occur in \(G \cup N\) and that for a clause containing two variables that are both not guards, we may freely choose which one to place as an edge label and which as a non-guard node, since the disjunction \(\lor\) of the formula is commutative.

Example 2. Given the (colored) formula \((a_1 \lor a_3 \lor c_2) \land (a_1 \lor b_1 \lor c_1) \land (c_1 \lor c_2 \lor c_3) \land (b_1 \lor c_1 \lor c_3)\), we construct the color structure \((G=\{a_1, c_1\} \cup N=\{c_2,c_3\},E=\{\{a_1,c_2\}^{a_3}, \{a_1,c_1\}^{b_1}, \{c_1,c_3\}^{c_2}, \{c_1,c_3\}^{b_1} \})\) (see Figure 1). Since there is no guard that of color \(b\), the variable \(b_1\) is unguarded. The induced assignment of the color structure sets \(a_1\) and \(c_1\), corresponding to the guard variables \(x_1\) and \(x_7\), to false and all remaining variables to true.

In the following, we want to formalize how to build a color structure. We do so by formalizing how to add variables to \(G\) without violating a property of the color structure. If two variables of a clause are contained in \(G\) and we add the third variable to \(G\), no variable of the clause is an edge label and the color structure yields an assignment where there is a clause where all variables are assigned to false. We say that a variable is locked if it appears in a positive clause whose two remaining variables are both guards. A color is locked if all variables of the color are locked.

If only one variable of a clause is a guard and we want to choose a variable of the remaining two to become a guard, we choose the variable that is placed at the end point of the edge and hence contained in \(N\) in order to comply the first property of the color structure. Otherwise, we need to swap the edge variable and the variable in \(N\). Further, we can make sure that \(G\) and \(N \cup E\) are disjoint after we added a variable \(x\) to \(G\) if we add all variables from the clauses that contain \(x\) to the sets \(G,N\) and \(E\). We abbreviate the process of swapping and adding variables by the term expansion.

Expansion of a variable can be seen as an update of the color structure that increases the number of guards. Conversely, we say that we unexpand a variable if we remove the respective variable from the set \(G\) and add it to \(N\). We refrain from unexpanding variables that have just been expanded or the other way around. Note that the process of expanding a variable modifies the current color structure in a unique way.

Further, we define a measure of how close a color is to being locked. We call the lock number of a variable of a color structure the number of relatives that have at least one locked occurrence or that are contained in a clause where one variable is a guard. By construction and the variable occurrence bound of four, the lock number ranges between zero and three. In Example 2, the lock number of variable \(b_1\) is zero, while the lock number of \(b_2\) and \(b_3\) is one, since \(b_1\) is locked between \(a_1\) and \(c_1\) and on top \(b_1\) labels the edge \(\{c_1,c_3\}^{b_3}\). Intuitively, a high lock number indicates that the color of a variable is close to being locked. We therefore prioritize expanding variables with a high lock number. Similarly, we define the expand number of a variable of a color structure as the number of locked colors that are gained if we expand the variable.

3 A Color Structure Algorithm↩︎

Our first algorithmic approach for constructing a color structure is to greedily expand variables color by color. The lock number serves as a heuristic to avoid locking a color: if four variables of a color are locked, no satisfying assignment can be derived. If three variables of a color are locked, the only way to obtain a satisfying assignment is to expand the one remaining unlocked variable. The lock number ensures that this variable is prioritized for expansion. Nevertheless, this greedy approach may still produce a locked color, and thus an unsatisfying assignment. In that case, we need to modify the current color structure to eliminate locked colors. If this fails, no satisfying assignment can be derived from the color structure. In particular, a color structure is satisfying if each color has exactly one guard. The color structure depicted in Figure 2 (belonging to Example 3 below) is not satisfying, since no variable of color \(g\) is a guard. The following lemma formalizes the correspondence between satisfying assignments and satisfying color structures.

In the following, we present the algorithm (Listing [lst:color-structure]) that takes a colored variant of a monotone 3-Sat formula \(F\) where each variable occurs once negated and up to four times unnegated together as input and returns a color structure. The following example illustrates the individual steps of the algorithm. We resolve ties in line 3 of the algorithm by taking the smallest variable and ties in line 5 by taking the variable that occurs the least often and then, the highest variable in order to aim for a connected color structure. Other tie breaks are also possible.

Set $Q = \{a_1\}$
WHILE $Q$ is not empty DO
    Expand unguarded variable in $Q$ with highest lock number
    WHILE there exists a locked color $u$ DO
        Choose variable $u_i$ with the lowest expand number 
        FOR each occurrence of $u_i$ DO
            Let $c=(u_i \lor v_j \lor l_s)$ be the clause containing $u_i$
            Among $v_j$ and $l_s$, unexpand the one with lower lock number
            Expand $u_i$
        END FOR
    END WHILE
    Add all variables in the color structure that are not locked to $Q$ 
    IF $Q$ is empty DO
        Pick a new unguarded variable $q_i$ that is not locked
        $Q = \{q_i\}$
    END IF  
    Remove variables $G$ and all their relatives from $Q$ 
END WHILE
RETURN Color structure constructed from the set of expanded variables

Example 3. Consider the formula \[\begin{align} &(a_1 \lor b_1 \lor f_1) \land (a_1 \lor b_1 \lor f_2) \land (a_1 \lor b_3 \lor c_1) \land (a_2 \lor b_1 \lor c_3) \land (a_3 \lor d_3 \lor g_3)\\ &\land (b_2 \lor c_1 \lor d_2) \land (b_2 \lor f_2 \lor g_1) \land (c_1 \lor d_1 \lor e_1) \land (d_1 \lor e_2 \lor g_1) \land (d_1 \lor e_2 \lor g_2)\\ &\land (c_2 \lor e_3 \lor g_3) \land (e_2 \lor f_3 \lor g_3). \end{align}\] First, we expand \(a_1\) since the lock number of each variable is zero. Then, we have the following queue annotated with the current lock number in the second coordinate: \((b_1,1),(b_3,1),(c_1,0), (f_1,1)\) and \((f_2,1)\). Subsequently, we expand \(b_1\) since it has the highest lock number and is the smallest variable. In the course of the algorithm, we expand the variables \(a_1,\; b_1,\; c_1,\; d_1,\; e_2,\; f_3\) in this order.

This results in the color structure depicted in Figure 2, locking the color \(g\) and hence, the variables \(g_1,\, g_2\), and \(g_3\). Since all variables \(g_1,\, g_2\), and \(g_3\) occur exactly once, we expand \(g_3\). The variable \(g_3\) is locked between \(e_2\) and \(f_3\). Since the lock number of \(e_2\) is one and the lock number of \(f_3\) is two, we unexpand \(e_2\) and then expand \(g_3\). The outer while loop then terminates since we expanded the variable \(e_3\) and with it the last color. This results in the color structure depicted in Figure [figure:finalstructure]. Now, we can extract the satisfying assignment: We set the guard variables \(a_1,\; b_1,\; c_1,\; d_1,\; e_3,\; f_3,\; g_3\) to false and all remaining ones to true. Since there are exactly as many negative clauses as guards, we have that \(Q\) is empty and the formula is satisfiable by Lemma 1.

The outer while loop greedily expands a variable for each color. Since the inner while loop may create new locked colors, we record its operations in a state diagram. An operation is depicted as rectangle and connected with the operation that is subsequent in the inner while loop. The inner while loop contains the operations expand or unexpand. The minimal size consists of six operations since we have that unexpansions are always followed by expansions and by definition, we do not immediately unexpand a variable that was just expanded or the other way around. The number of states in the state diagram depends on the input formula. In order to facilitate a later counting argument, we section an arbitrary state diagram into the base cycle and the \(\ell\)-block. The base cycle consists of the minimal size state diagram. We rename the variables such that the minimal size of a state diagram consists of the operations ‘expand \(a_1\)’, ‘unexpand \(b_1\)’, ‘expand \(c_1\)’, ‘unexpand \(a_1\)’, ‘expand \(d_1\)’, ‘unexpand \(e_1\)’. The remaining part of the state diagram consisting of the remaining \(\ell\) expand operations and \(\ell\) unexpand operations is called \(\ell\)-block. We rename the variables of the \(\ell\)-block that are expanded as \(y_1^1, \dots, y_1^\ell\) and the variables \(x_1^1, \dots, x_1^\ell\) that are unexpanded. Hence, the state diagram is labeled with variables of the colors \(a,b,c,d,e,y^1, \dots, y^\ell, x^1, \dots, x^\ell\). This naming convention helps us to overview the states of the inner while loop (see Figure 3).

In order to prove correctness, we want to abstract from a concrete color structure given an input formula to the algorithm. Instead, we look at a hypothetical color structure that is constructed at a certain time in the algorithm. We specify this via the states of the state diagram. The state diagram fixes parts of the color structure due to the naming which variable is expanded or unexpanded when. We know that the variables that were expanded are guards and the variables that were unexpanded are edge labels connected to the guards. In particular, if ‘expand \(a_1\)’ and ‘unexpand \(b_1\)’ are consecutive, some clause must contain both \(a_1\) and \(b_1\). We call clauses connectors that contain two variables from consecutive operations ‘expand’ and ‘unexpand’ because they connect the states in the state diagram. For each subsequent operation pair, we choose one specific connector if more than one clause contains both variables. In addition to connectors, there are clauses where we cannot specify its guards due to the naming of the state diagram but that contain variables that need to be locked somewhere in the current color structure. Throughout the algorithm, we only unexpand a variable if the corresponding color is locked in the first place. A color is locked if all (at most) four variables of the color have at least one occurrence that is locked. If we unexpand \(b_1\) in order to expand \(c_1\), we can assume two relatives \(c_2\) and \(c_3\) to be locked in the first place. For each unexpansion followed by an expansion of a variable, we call the relative variables of the variable detainee relatives.

So far, we have reasoned about the parts of the color structure at a certain state of the state diagram with fixed naming. In contrast, we can look at the parts of the color structure where we have not yet named the variables or fixed the location of the clauses. To illustrate the hypothetical color structure, imagine a color structure that consists of placeholders for the guards, edge labels and node labels were some are filled with variables and some are blank. The blank spots arise because no variable names have been assigned/specified in the inner while loop yet. We call edges whose labels have not yet been specified in the inner while loop prisoner spots. A variable is locked if it is contained in a clause with two other guards and hence, prisoner spots are the locations where variables can be locked if the edge label is contained in a clause with two guards.

In the following, we use the counting arguments to prove correctness of the Color Structure Construction Algorithm.

As a result, we obtain an algorithm that iteratively builds a color structure from a given colored formula and thereby derives a satisfying assignment. Together with the equivalence proved by Darmann and Döcker [9] and the aforementioned hardness result showing that Monotone 3-Sat-\((k, 1)\) is NP-complete for all \(k \geq 5\) [9], we obtain the following dichotomy:

4 Conclusion↩︎

In sum, we introduced the concept of a color structure for encoding assignments for formulas of the type Monotone 3-Sat-\((\leq k,1)\) with \(k\geq 1\). We presented a polynomial-time algorithm that translates a formula of this type into a color structure and used it to establish the existence and construction of a satisfying assignment for \(k\leq 4\). The correctness proof of the algorithm relies on a counting argument: For \(k \leq 4\), as shown in the proof of Theorem 1, each color has variables that are not locked and can therefore be expanded, which guarantees that the algorithm terminates with a satisfying assignment. For \(k\geq 5\), this argument no longer applies, since there are enough prisoner spots for all detainee relatives, so that the loop may not be left. This breakdown is not incidental: Monotone 3-Sat-\((\leq k,1)\) is NP-hard for \(k\geq 5\), which in particular implies the existence of unsatisfiable instances. If the counting argument still held, it would show that every instance is satisfiable, contradicting this hardness result. In this sense, the color structure allows us to pinpoint exactly where the argument breaks down as \(k\) increases from 4 to 5, matching the transition in complexity. This suggests that color structures capture relevant structural information about such formulas beyond the specific algorithm presented here, and we believe the concept may prove fruitful for other Sat-solving approaches as well.

References↩︎