Linear Satisfiability Preserving Assignments (Extended Abstract)

1 Introduction

The constraint satisfaction problem (CSP, in short) is given as a triple (V,D, C), where V is a set of variables, D is a finite variable domain, and C is a set of constraints on the variables that specify the permitted combinations of value assignments to variables. A solution to a CSP instance is an assignment to all the variables that satisfies all the constraints. The CSP is the problem of finding a solution to a given instance (V, D, C). The CSP can express a number of problems in diverse fields, and is recognized as one of the most fundamental problems in computer science (e.g., [Tsang, 1993; Creignou et al., 2001; Dechter, 2003; Rossi et al., 2006]). It is known that the Boolean satisfiability problem (SAT) can be regarded as a Boolean CSP, in which each constraint is represented by a clause (i.e., disjunction of literals). Moreover, integer linear systems are also formulated as a CSP. The problem is, given a matrix G ∈ Zm×n , a vector h ∈ Zm, and a positive integer d, where Z denotes the set of all integers, to compute an integer vector x ∈ {0, 1, . . . , d}n such that Gx ≥ h. It is a well-studied topic, especially in the field of mathematical programming.

∗This paper is an extended abstract of an article in the Journal of Artificial Intelligence Research [Kimura and Makino, 2018].

Many practical algorithms have been proposed to solve CSPs (including SAT and integer linear systems). One of the important methods is based on reducing the problem size by partial variable assignments. For example, satisfiability preserving assignments are used to reduce the problem size, where a partial assignment is called satisfiability preserving if the satisfiability of the problem does not change after substituting it to the corresponding variables. Once a satisfiability preserving assignment is available, instead of solving the original problem instance, we may solve the problem instance obtained from the original one by the partial assignment. Here we note that the size of the resulting problem instance is smaller than the original one.

Satisfiability preserving assignments have been considered in many fields such as artificial intelligence and optimization. An important example is forced assignments, which are essentially the same concepts as back bones [Monasson et al., 1999], frozen variables [Jonsson and Krokhin, 2004], and implied values [Bordeaux et al., 2008]. An assignment of a ∈ D to variable x is called forced if x has to be set to a in all satisfying assignments. Unit clause propagation in SAT is a prominent example of forced assignments. Pure literals in SAT can also be seen as another example of satisfiability preserving assignments, where a literal ℓ is called pure if a given CNF contains no ℓ (i.e., negation of ℓ). By definition, for a pure literal ℓ, an assignment ℓ = 1 is satisfiability preserving. Pure literals, together with unit clause propagation, are used by the Davis-Putnam-Logemann-Loveland (DPLL) algorithm [Davis and Putnam, 1960; Davis et al., 1962] to reduce the search space. We note that the DPLL algorithm is a basis of many current SAT solvers. Also in practice, various types of satisfiability preserving assignments are used, especially in branch-and-bound algorithms. Among them, we consider three fundamental satisfiability preserving assignments, namely, satisfying, fixable, and autark partial assignments. A satisfying partial assignment is a straightforward example of satisfiability preserving assignments. A partial assignment is satisfying if it satisfies all the constraints no matter what values are assigned to the unassigned variables. Clearly, satisfying partial assignments are satisfiability preserving. An assignment A to variable set X ⊆ V is called fixable ([Bordeaux et al., 2008]; also called safe in, e.g., [Kleine B¨uning and Kullmann, 2009]) if every satisfying total assignment stays satisfying, even if the assignment to X is replaced by A, where the assignment to V \ X remains unchanged. By definition, a fixable assignment is satisfiability preserving. For the SAT problem, autark assignments were introduced by Monien and Speckenmeyer [1985] to provide a fast exponential time algorithm. A partial assignment is called autark if it satisfies all the clauses that contain variables assigned by it.

Although it is preferable to obtain these satisfiability preserving assignments, it is in general NP-hard to find these assignments. Thus, linear and local types are studied by Kullmann [2000] and Bordeaux et al. [2008], for example, where linear types are discussed in the next paragraph. Local types are defined in terms of constraints. More precisely, they require a partial assignment to be satisfiability preserving for each constraint, when each constraint itself is regarded as a problem instance.

Since it is NP-hard to find an autark assignment, Kullmann [2000] introduced linear autark assignments to efficiently find an autark assignment. Linear autark assignments can be seen as polyhedral conic inner approximations of autark assignments in the sense that they correspond to polyhedral cones, which are defined by systems of linear inequalities, contained in the set of vectors corresponding to the set of autark assignments. This implies that they can be computed in polynomial time via solving linear programming problems [Kullmann, 2000]. Linear autark assignments provide a unifying algorithm to solve wellknown tractable subclasses of the SAT problem. For example, 2- [Even et al., 1976], Horn [Henschen and Wos, 1974], renamable Horn [Lewis, 1978], and q-Horn [Boros et al., 1990] SAT problems are polynomially solvable by iteratively finding linear autark assignments [Kullmann, 2000; van Maaren, 2000].

Despite its importance, the field of linear autark assignments appears largely unexplored as pointed out by, e.g., Kleine B¨uning and Kullmann [2009, Section 11.11]. These motivate us to study convex inner approximations of autark assignments and especially general linear types, i.e., satisfiability preserving assignments that can be represented by general linear programming problems.

In this paper, we mainly deal with the Boolean CSP and investigate linear fixable, autark and satisfying partial assignments, i.e., those satisfiability preserving assignments corresponding to polyhedral cones in the associated vector space. Kullmann introduced linear autark assignments, namely, satisfiability preserving assignments that can be obtained efficiently via solving linear programming problems. These linear autark assignments correspond to specific cones, i.e., cones defined by clause-variable matrices (see Section 2). It is important to consider more general cones and convex sets dominating (namely, containing) these specific cones, since they might be more useful in practice. We hence consider general convex inner approximations of satisfying preserving assignments. We show that, even if viewed from the generalized framework, Kullmann's framework offers good approximations of satisfiability preserving assignments.

Due to the space limitation, we omit all the proofs of the results, where the proofs can be found in [Kimura and Makino, 2018].

2 Preliminaries

Let V denote a set of variables with size n = |V |. Let D denote the finite domain of the variables in V , where |D| ≥ 2. For a subset X ⊆ V , a mapping A : X → D is called a partial assignment on X. We denote by DX the set of partial assignments on X. For convenience, we identify the variables and the indices in this paper. For a partial assignment A : X → D, X is denoted by var(A). A partial assignment A is called a total assignment if var(A) = V holds, and called a trivial assignment if var(A) = ∅ holds. For notational simplicity, we identify a partial assignment A with a vector a ∈ (D∪{∗})n such that aj = A(xj) if xj ∈ var(A), and aj = ∗ otherwise (i.e., xj ̸∈ var(A)). For example, if n = 3 and A : {x1, x3} → {0, 1, 2} such that A(x1) = 2 and A(x3) = 0, then we have a = (2, ∗, 0). For an integer k ≥ 1, a k-ary relation on D is a subset of Dk . A constraint C is a pair C = 〈(xC1 , . . . , xCk ), R〉, where xC1 , . . . , xCk ∈ V are variables and R is a k-ary relation on D. (xC1 , . . . , xCk ) is called a scope of the constraint and {xC1 , . . . , xCk } is written as V (C). We denote by SC the set of the total assignments satisfying the constraint C = 〈(xC1 , . . . , xCk ),R〉, that is, SC = {a ∈ Dn | (aC1 , . . . , aCk ) ∈ R}. An instance of the constraint satisfaction problem (CSP) is defined by a triplet (V,D, C) such that C denotes a set of constraints with m = |C|. A total assignment A ∈ DV is called a solution (or a satisfying total assignment) to a CSP instance (V, D, C) if it satisfies every constraint, i.e., (aC1 , . . . , aCk ) ∈ R holds for every constraint 〈(xC1 , . . . , xCk ),R〉 ∈ C. Hence, A ∈ DV is a solution if and only if A ∈ ⋂C∈C SC holds. The CSP is the problem of finding a solution to a given instance (V, D, C).

The Boolean satisfiability problem (SAT) is regarded as a special case of the CSP, in which V = {x1, . . . , xn} denotes the set of propositional variables, i.e., D = {0, 1}, and C is given by a conjunctive normal form (CNF) ϕ = ∧mi=1 (∨j∈J (i) + xj ∨ ∨j∈J (i) - xj), where J (i) + , J (i) - ⊆ {1, . . . , n} and J (i) + ∩J (i) - = ∅ for all i = 1, . . . ,m. Namely, the constraints in C correspond to the clauses in ϕ. The problem of solving an integer linear system (with finite domain) is also contained in CSPs, where each constraint is given as a

linear inequality.

A CNF ϕ is prime if replacing a clause c ∈ ϕ by a proper subclause of c produces a CNF which is not equivalent to ϕ.

For a partial assignment A and X ⊆ var(A), the restriction of A to X, denoted by A|X, is defined as a partial assignment in DX such that A|X(v) = A(v) for all v ∈ X. Let S be a subset of DV . For a partial assignment A, let S[A] be the restriction to V \ var(A) of those elements in S that are compatible with A, i.e., S[A] = {B|V \var(A) | B ∈ S,B|var(A) = A}. For a CSP instance (V,D, C) with the solution set S ⊆ DV , a partial assignment A is called satisfiability preserving if the satisfiability of the problem does not change after substituting it to the corresponding variables, i.e., S[A] ̸= ∅ if and only if S ̸= ∅. In other words, a satisfiability preserving assignment is a partial assignment which can be extended to a total assignment in S, if S is not empty. For a CSP instance with S = ∅, any partial assignment is satisfiability preserving.

We now introduce several (globally and locally) satisfiability preserving assignments.

Definition 1 (Globally satisfiability preserving assignment). Let (V,D, C) be a CSP instance, and let A be a partial assignment.

• (i) A is called globally satisfying for (V,D, C) if any extension of A to a total assignment is a solution.
• (ii) A is called globally fixable for (V,D, C) if any solution to (V,D, C) produces a solution by replacing those assignments to var(A) by A.

Let S be a solution set to (V, D, C). By definition, a partial assignment A is globally satisfying if and only if S[A] = DV \var(A) holds. Moreover, A is globally fixable if and only if S[A] ⊇ S[B] holds for any partial assignment B such that var(B) = var(A).

Definition 2 (Locally satisfiability preserving assignment). Let (V,D, C) be a CSP instance, and let A be a partial assignment.

• (i) A is called locally satisfying for (V,D, C) if for any constraint C ∈ C, it is globally satisfying for (V,D, {C}).
• (ii) A is called autark for (V,D, C) if for any constraint C ∈ C with a variable in var(A), it is globally satisfying for (V, D, {C}).
• (iii) A is called locally fixable for (V,D, C) if for any constraint C, it is globally fixable for (V,D, {C}).

Definition 3. For a CSP instance I, we define Pg-sat(I), Pℓ-sat(I), Pautark(I), Pg-fix(I), Pℓ-fix(I) and Ppresv(I) as the set of all the globally satisfying, locally satisfying, autark, globally fixable, locally fixable and satisfiability preserving partial assignments of I, respectively.

We then define linear satisfiability preserving assignments. In order to define linear satisfiability preserving assignments for Boolean CSPs with V = {x1, . . . , xn} and D = {0, 1}, we identify a vector y ∈ Rn with a partial assignment ay ∈ {0, 1, ∗}n such that

We note that the jth coordinate of Rn corresponds to Boolean variable xj . We also note that this identification is introduced by Kullmann [2000]. For Z ⊆ Rn , let P(Z) be the set of partial assignments corresponding to the vectors in Z, i.e., P(Z) = {ay | y ∈ Z}. Conversely, for a set of partial assignments P , we define the set of vectors corresponding to P by Y (P) = {y ∈ Rn | ay ∈ P}. Note that Y (P) is a (not necessarily convex) cone.

For two vectors y and z ∈ Rn , we write y ≥ z, if yj ≥ zj holds for all j = 1, . . . , n, and y ≫ z, if yj > zj holds for all j = 1, . . . , n. For a matrix M, let K≥(M) = {y ∈ Rn | My ≥ 0} and K≫(M) = {y ∈ Rn | My ≫ 0}. A subset Z ⊆ Rn is called a (closed) polyhedral cone if Z = K≥(M) holds for some matrix M and open polyhedral cone if Z = K≫(M) holds for some matrix M.

Definition 4. Let (V,D = {0, 1}, C) be a Boolean CSP instance. A subset P of globally satisfying (resp., globally fixable, locally satisfying, autark, locally fixable, and satisfiability preserving) partial assignments of (V,D, C) is called linear if it corresponds to some polyhedral cone K in Rn , i.e., P = P(K), and such a partial assignment in P is called K-linear.

Kullmann [2000] introduced unweighted linear autark assignments for the SAT problem 1 . Namely, for a CNF ϕ = ∧mi=1 ci, let Mϕ be a clause-variable matrix of ϕ, i.e., an m × n matrix such that (i, j) entry is 1 if xj ∈ ci, -1 if xj ∈ ci, and 0 otherwise (i.e., xj ̸∈ V (ci)). Then an unweighted linear autark assignment is exactly a K≥(Mϕ)- linear autark assignment. We note that any partial assignment in P(K≥(Mϕ)) is autark. Kullmann [2003] implicitly studied unweighted linear globally satisfying partial assignments, which are K≫(Mϕ)-linear globally satisfying partial assignments. We again note that any partial assignment in P(K≫(Mϕ)) is globally satisfying.

Kullmann [2003] then introduced weighted linear autark and globally satisfying partial assignments. For a real matrix M, let Q(M) denote the set of matrices N with its sign pattern identical to M, i.e., Nij < 0 (resp., = 0, > 0) if and only if Mij < 0 (resp., = 0, > 0). Q(M) is known as the qualitative class of matrix M [Brualdi and Shader, 1995]. Then a set P of partial assignments is called weighted linear autark if we have P = P (K≥(M)) for an M ∈ Q(Mϕ), and weighted linear globally satisfying if we have P = P(K≫(M)) for an M ∈ Q(Mϕ). Kullmann characterizes autark and globally satisfying partial assignments in terms of the qualitative class of the clause-variable matrix of a CNF. Namely, it is shown that Pautark = ⋃M∈Q(Mϕ) P(K≥(M)) and Pg-sat = ⋃M∈Q(Mϕ) P(K≫(M)). We give more detailed analyses in the next section.

3 Main Results of the Paper

3.1 Maximality of Weighted Linear Satisfiability Preserving Assignments for CNFs

We here describe our extensions of Kullmann's work to general convex sets and cones. The results stated below in this paragraph are for SAT instances, i.e., CNFs.

As mentioned in Section 2, for a Boolean CSP instance of n variables, we identify a vector y ∈ Rn with a partial assignment x. Then, to compute satisfiability preserving assignments efficiently, we consider polyhedral conic inner approximations of them, i.e., polyhedral cones that are contained in the set of vectors corresponding to satisfiability preserving assignments. We note that linear autark assignments defined by Kullmann [2000] are indeed polyhedral conic inner approximations of a special type. We investigate which polyhedral cone well approximates satisfiability preserving assignments.

1 More precisely, Kullmann referred to unweighted linear autark assignments as simple linear autark assignments, and partial assignments defined by iteratively applying simple linear autark assignments as linear autark assignments.

We first show that the weighted linear autark assignments introduced by Kullmann [2003] dominate general polyhedral cones in term of the set of vectors for autark assignments. Namely, no matter how complex a polyhedral cone is, it is contained in a polyhedral cone defined by a matrix in the qualitative class of the clause-variable matrix. Note that similar results to the ones for autark assignments also hold for satisfying partial assignments from Theorems 1 to 3. Let Q0(M) denote the set of matrices N such that 1) Nij < 0 (resp., Nij > 0), only if Mij < 0 (resp., Mij > 0), and 2) each row contains at least one nonzero entry.

Theorem 1. Let I = (V, D, C) be a SAT instance, where C is given by a CNF ϕ.

• (i) Let N be a matrix that represents linear autark assignments, i.e., K≥(N) is contained in Y (Pautark(I)). Then there exists a matrix M in Q(Mϕ) such that K≥(N) ⊆ K≥(M).
• (ii) Let N be a matrix that represents linear satisfying partial assignments, i.e., K≫(N) is contained in Y (Psat(I)). Then there exists a matrix M in Q0(Mϕ) such that K≫(N) ⊆ K≫(M).

This extends the result that any autark assignment can be obtained as a weighted linear autark assignment [Kullmann, 2003, Lemma 3.5], since there always exists a polyhedral cone containing a vector corresponding to the autark assignment. Moreover, we show that the weighted linear autark assignments dominate general convex sets in terms of the set of partial assignments. Namely, for any convex set contained in the set of vectors corresponding to the autark assignments, there exists a matrix in the qualitative class of the clausevariable matrix such that the set of the partial assignments corresponding to the polyhedral cone defined by the matrix subsumes the set of the partial assignments corresponding to the convex set.

Theorem 2. Let I = (V, D, C) be a SAT instance, where C is given by a CNF ϕ.

• (i) For any convex set C contained in Y (Pautark(I)), there exists a matrix M ∈ Q(Mϕ) such that P(C) ⊆ P (K≥(M)).
• (ii) For any convex set C contained in Y (Psat(I)), there exists a matrix M ∈ Q0(Mϕ) such that P(C) ⊆ P (K≫(M)).

Furthermore, if the input is monotone, i.e., if the input CNF contains no negative literal, then any matrix in the qualitative class of the clause-variable matrix defines a polyhedral cone that contains all the autark assignments, which shows the strength of linear autark assignments.

Theorem 3. Let I = (V,D, C) be a monotone SAT instance, i.e., a SAT instance where C is given by a monotone CNF ϕ. Then for any matrix M ∈ Q(Mϕ), we have P(K≥(M)) = Pautark(I) and P (K≫(M)) = Psat(I).

Finally, if the input is monotone and prime, then any matrix in the qualitative class of the clause-variable matrix defines a polyhedral cone that is maximal as a convex set. Here a convex subset Z ⊆ Y (P) is called a maximal convex subset of Y (P) if there exists no distinct convex set Z ′ ⊆ Y (P) that contains Z.

Theorem 4. Let I = (V, D, C) be a prime monotone SAT instance, i.e., a SAT instance with C given by a prime monotone CNF ϕ. Then any M ∈ Q(Mϕ) defines a maximal convex subset K≥(M) of Y (Pautark(I)).

3.2 Algorithms of Finding Linear Satisfiability Preserving Assignments for Integer Linear Systems

In this subsection, we discuss computing a linear satisfiability preserving assignment of CSPs given by integer linear systems. Using the ellipsoid method [Gr¨otschel et al., 1993], we first provide a pseudo-polynomial time algorithm to find a linear locally-fixable assignment for the 0-1 integer linear system. Here, a 0-1 integer linear system is an integer linear system such that D = {0, 1}. An algorithm is called a pseudo-polynomial time algorithm if it runs in polynomial in the length of the input and the magnitude of the largest integer occurring in the input (e.g., [Garey and Johnson, 1979]). We also show that the problem can be solved in polynomial time if every entry of the input matrix is contained in {0, -1, +1}.

Theorem 5. We can find in pseudo-polynomial time a nontrivial linear locally fixable assignment for the 0-1 integer linear system, if it exists. Moreover, it is possible in polynomial time, for the unit integer linear system, i.e., the input matrix G is given by G ∈ {0, -1, +1}m×n .

We can also obtain a similar result for general integer linear systems by making use of the following encoding called the order encoding [Tamura et al., 2009; Petke and Jeavons, 2011] that transform CSP instances with D = {0, 1, . . . , d} to Boolean CSP instances. For each variable xj, we take d Boolean variables xj1, . . . , xjd which guarantee that xj = p if and only if xj1 = · · · = xjp = 1 and xj,p+1 = · · · = xjd = 0. We then obtain the following theorem.

Theorem 6. We can find in pseudo-polynomial time a nontrivial linear locally fixable assignment for the general integer linear system, if it exists.

Similar to the results for SAT by Kullmann [2000] and van Maaren [2000], we can solve TVPI [Hochbaum et al., 1993; Bar-Yehuda and Rawitz, 2001], Horn [Glover, 1964; van Maaren and Dang, 2002], and q-Horn [Kimura and Makino, 2016] integer linear systems by repeatedly obtaining a linear locally-fixable assignment.

Theorem 7. If an integer linear system is TVPI, Horn or qHorn, then it can be solved in pseudo-polynomial time by repeatedly finding linear locally fixable assignments.

Acknowledgments

The authors thank Dr. Yasushi Kawase for fruitful discussion on Theorem 5. The first author is supported by JSPS KAKENHI Grant Number JP15H06286. The second author is supported by JSPS KAKENHI Grant Number JP24106002, JP25280004, JP26280001, and JST CREST Grant Number JPMJCR1402, Japan.