# linear_satisfiability_preserving_assignments__1bc94775.pdf

Journal of Artiﬁcial Intelligence Research 61 (2018) 291-321 Submitted 08/17; published 02/18

Linear Satisﬁability Preserving Assignments

Kei Kimura kimura@cs.tut.ac.jp Toyohashi University of Technology Toyohashi, 441-8580, Japan

Kazuhisa Makino makino@kurims.kyoto-u.ac.jp Kyoto University Kyoto, 606-8502, Japan

In this paper, we study several classes of satisﬁability preserving assignments to the constraint satisfaction problem (CSP). In particular, we consider ﬁxable, autark and satisfying assignments. Since it is in general NP-hard to ﬁnd a nontrivial (i.e., nonempty) satisﬁability preserving assignment, we introduce linear satisﬁability preserving assignments, which are deﬁned by polyhedral cones in an associated vector space. The vector space is obtained by the identiﬁcation, introduced by Kullmann, of assignments with real vectors. We consider arbitrary polyhedral cones, where only restricted classes of cones for autark assignments are considered in the literature. We reveal that cones in certain classes are maximal as a convex subset of the set of the associated vectors, which can be regarded as extensions of Kullmann s results for autark assignments of CNFs. As algorithmic results, we present a pseudo-polynomial time algorithm that computes a linear ﬁxable assignment for a given integer linear system, which implies the well known pseudo-polynomial solvability for integer linear systems such as two-variable-per-inequality (TVPI), Horn and q-Horn systems.

1. Introduction

We in this section introduce central concepts in the study and summarize our results.

1.1 Constraint Satisfaction Problem

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 ﬁnite 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 satisﬁes all the constraints. The CSP is the problem of ﬁnding a solution to a given instance (V, D, C). The CSP can express a number of problems in diverse ﬁelds, and is recognized as one of the most fundamental problems in computer science (e.g., Tsang, 1993; Creignou, Khanna, & Sudan, 2001; Dechter, 2003; Rossi, van Beek, & Walsh, 2006). The CSP has been studied extensively from both theoretical and practical points of view. For example, it is known that the CSP of a ﬁxed ﬁnite constraint language has a dichotomy property (Schaefer, 1978; Bulatov, 2006, 2017; Zhuk, 2017). Namely, it is polynomially solvable if all the constraints satisfy a certain property, or otherwise NP-hard. Moreover, due to practical importance, many heuristic algorithms have been proposed (Tsang, 1993; Dechter, 2003; Rossi et al., 2006). In this paper, each constraint might involve a non-ﬁxed number of variables, as is often assumed in the literature (van Hoeve & Katriel, 2006).

c 2018 AI Access Foundation. All rights reserved.

Kimura & Makino

The Boolean satisﬁability problem (SAT) can be regarded as a Boolean CSP, in which each constraint is represented by a clause (i.e., disjunction of literals). SAT itself is an important problem in computer science. It is well-known that SAT is NP-hard (Cook, 1971), but several restricted classes such as 2-SAT (Even, Itai, & Shamir, 1976), Horn SAT (Henschen & Wos, 1974), renamable Horn SAT (Lewis, 1978), q-Horn SAT (Boros, Crama, & Hammer, 1990), and Lin Aut SAT (Kullmann, 2000; van Maaren, 2000) are solvable in polynomial time.

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 ﬁeld of mathematical programming. The problem is strongly NP-hard, but several (semi-)tractable subclasses are known to exist. For example, the problem can be solved in polynomial time, if n is bounded by some constant (Lenstra, Jr., 1983), or if G is totally unimodular (Hoﬀman & Kruskal, 1956). Moreover, it can be solved in pseudo-polynomial time if (1) m is bounded by some constant (Papadimitriou, 1981), (2) G corresponds to a two-variable-per-inequality (TVPI) system (i.e., each row of G contains at most two nonzero elements) (Hochbaum, Megiddo, Naor, & Tamir, 1993; Bar-Yehuda & Rawitz, 2001), (3) G is Horn (i.e., each row of G contains at most one positive element) (Glover, 1964; van Maaren & Dang, 2002), or (4) G is q-Horn (Kimura & Makino, 2016). It is also known that the problem is weakly NP-hard, even if m is bounded by some constant or the system is TVPI and Horn (also called monotone quadratic) (Lagarias, 1985).

1.2 Satisﬁability Preserving Assignments

As mentioned above, 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, satisﬁability preserving assignments are used to reduce the problem size, where a partial assignment is called satisﬁability preserving if the satisﬁability of the problem does not change after substituting it to the corresponding variables. Once a satisﬁability 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.

Satisﬁability preserving assignments have been considered in many ﬁelds such as artiﬁcial intelligence and optimization. An important example is forced assignments, which are essentially the same concepts as back bones (Monasson, Zecchina, Kirkpatrick, Selman, & Troyansky, 1999), frozen variables (Jonsson & Krokhin, 2004), and implied values (Bordeaux, Cadoli, & Mancini, 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 satisﬁability preserving assignments, where a literal ℓis called pure if a given CNF contains no ℓ(i.e., negation of ℓ). By deﬁnition, for a pure literal ℓ, an assignment ℓ= 1 is satisﬁability preserving. Pure literals, together with unit clause propagation, are used by the Davis-Putnam-Logemann-Loveland (DPLL) algorithm (Davis & Putnam, 1960; Davis, Logemann, & Loveland, 1962) to reduce the search space. We note that the

Linear Satisfiability Preserving Assignments

DPLL algorithm is a basis of many current SAT solvers. Also in practice, various types of satisﬁability preserving assignments are used, especially in branch-and-bound algorithms. Among them, we consider three fundamental satisﬁability preserving assignments, namely, satisfying, ﬁxable, and autark partial assignments. A satisfying partial assignment is a straightforward example of satisﬁability preserving assignments. A partial assignment is satisfying if it satisﬁes all the constraints no matter what values are assigned to the unassigned variables. Clearly, satisfying partial assignments are satisﬁability preserving. An assignment A to variable set X V is called ﬁxable (Bordeaux et al., 2008; also called safe by, e.g., Kleine B uning & 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 deﬁnition, a ﬁxable assignment is satisﬁability preserving. Another example is autark assignments, which play an important role in this paper and thus will be stated in depth in the next paragraph. 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 satisﬁes all the clauses that contain variables assigned by it. Later, Kullmann (2000) investigated autark assignments in terms of resolution refutation. A CNF is lean if it does not have a nontrivial autark assignment. Kullmann showed that a CNF is lean if and only if every clause can be used by some resolution refutation. Moreover, it is shown that a CNF, seen as a set of clauses, can be uniquely decomposed into two subsets of clauses: the maximal autark subset and the maximal lean subset. Although it is preferable to obtain these satisﬁability preserving assignments, it is in general NP-hard to ﬁnd these partial assignments. Thus, local and linear types are studied by Kullmann (2000) and Bordeaux et al. (2008), for example, where linear types are discussed in the next subsection. Local types are deﬁned in terms of constraints. More precisely, they require a partial assignment to be satisﬁability preserving for each constraint, when each constraint itself is regarded as a problem instance. We note that an autark assignment is in fact a local type, since it is deﬁned in terms of constraints. A partial assignment is called locally satisfying if it is satisfying for each constraint, and locally ﬁxable if it is ﬁxable for each constraint. As seen in Section 3, the strength of locality depends on the constraint classes. Before discussing linear autark assignments, we state two concepts related to satisﬁability preserving assignments: symmetric breaking and backdoor sets. Symmetry breaking, which can be regarded as a generalization of satisﬁability preserving assignments, is also widely used to reduce the search space in artiﬁcial intelligence (Freuder, 1991; Jeavons, Cohen, & Cooper, 1994; Prestwich, 2004). A backdoor set is a subset of variables whose instantiation leads a given formula to the one which is computationally easy to solve (Crama, Ekin, & Hammer, 1997; Williams, Gomes, & Selman, 2003; Gaspers & Szeider, 2012).

1.3 Linear Autark Assignments

Since it is NP-hard to ﬁnd an autark assignment, Kullmann (2000) introduced linear autark assignments to eﬃciently ﬁnd 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 deﬁned by systems of linear inequalities, contained

Kimura & Makino

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). We note that the correspondence of partial assignments and vectors is also introduced by Kullmann. Although autark assignments are not always linear, linearity can be used to eﬃciently ﬁnd autark assignments and have a possible application to speed up heuristic SAT algorithms. Moreover, linear autark assignments provide a unifying algorithm to solve well-known tractable subclasses of the SAT problem. For example, 2-, Horn and q-Horn SAT problems are polynomially solvable by iteratively ﬁnding linear autark assignments (Kullmann, 2000; van Maaren, 2000).

At ﬁrst, Kullmann (2000) introduced unweighted linear autark assignments, namely, those assignments that correspond to polyhedral cones deﬁned by so-called clause-variable matrices of CNFs. Later, Kullmann (2003) used qualitative matrix analysis (e.g., Brualdi & Shader, 1995) to analyze autark assignments. For example, Kullmann (2003, Lemma 3.5) shows that any matrix in the qualitative class of the clause-variable matrix, i.e., matrix that has the same sign pattern as the clause-variable matrix, deﬁnes polyhedral cones that derive autark assignments (and such an assignment is sometimes called a weighted linear autark assignment). Namely, it is shown that polyhedral cones deﬁned by such matrices are included in the set of vectors corresponding to the autark assignments. Kullmann (2003, Lemma 3.5) also shows that any autark assignment can be obtained by linear inequalities deﬁned by some matrix in the qualitative class. However, it is not investigated which matrices deﬁne a good polyhedral conic approximation nor can we do better if we consider general convex inner approximation, i.e., convex sets contained in the set of vectors corresponding to the autark assignments. In fact, the ﬁeld 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., satisﬁability preserving assignments that can be represented by general linear programming problems.

We note that connection between linear programmings and SAT is explored by Chandru and Hooker (1999). They investigate the power of a linear programming relaxation of an integer programming formulation of SAT. Their work can be seen as an investigation of a convex outer approximation of integral solutions in the sense that the feasible solution of the relaxed problem subsume that of the original one. On the other hand, we investigate a convex inner approximation of integral solutions (and satisﬁability preserving assignments) in the sense that the convex sets we consider are contained in the (transformed) feasible solutions of the original problem.

1.4 The Results in this Paper

In this paper, we mainly deal with the Boolean CSP and investigate linear ﬁxable, autark and satisfying partial assignments, i.e., those satisﬁability preserving assignments corresponding to polyhedral cones in the associated vector space. Kullmann introduced linear autark assignments, namely, satisﬁability preserving assignments that can be obtained eﬃciently via solving linear programming problems. These linear autark assignments correspond to speciﬁc cones, i.e., cones deﬁned by clause-variable matrices. It is important to consider more general cones and convex sets dominating (namely, containing) these speciﬁc cones,

Linear Satisfiability Preserving Assignments

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 oﬀers good approximations of satisﬁability preserving assignments.

1.4.1 Linear Satisﬁability Preserving Assignments

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. We ﬁrst 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 (see Theorem 3 in Section 3). Namely, no matter how complex a polyhedral cone is, it is contained in a polyhedral cone deﬁned by a matrix in the qualitative class of the clause-variable matrix. 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 (see Theorem 4). 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 clause-variable matrix such that the set of the partial assignments corresponding to the polyhedral cone deﬁned by the matrix subsumes the set of the partial assignments corresponding to the convex set. 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 clausevariable matrix deﬁnes a polyhedral cone that contains all the autark assignments, which shows the strength of linear autark assignments (see Theorem 5). Similar results hold for satisfying partial assignments (see Theorems 3-5). Finally, if the input is monotone and prime, then any matrix in the qualitative class of the clause-variable matrix deﬁnes a polyhedral cone that is maximal as a convex set (see Theorem 6). Here, a CNF φ is called prime if replacing a clause c φ by a proper subclause of c produces a CNF which is not equivalent to φ. We note that such matrices were considered in relation with autark and satisfying partial assignment (Kullmann, 2003), however, it is not investigated in the literature how good the polyhedral cones that these matrices deﬁne are. We also note that any Boolean CSP instance can be transformed to a (possibly exponential size) CNF, and hence these results indicate how to ﬁnd a good convex set for any Boolean CSP.

1.4.2 Algorithms of Finding Linear Satisﬁability Preserving Assignments for Integer Linear Systems

We consider computing linear satisﬁability preserving assignments, especially linear locally ﬁxable assignments, of a given integer linear system. If each constraint is represented by a prime CNF, then we can compute a linear locally ﬁxable assignment by considering a linear autark assignment, which can be easily formulated from given linear inequalities (Kullmann, 2000). Moreover, since each constraint of an integer linear system is monotone (unate, more precisely), this ensures its dominance property by Theorems 5 and 6. However, it can be seen that a prime CNF expression is in general exponentially larger than the input. Therefore, instead of explicitly constructing the system of linear inequalities corresponding to a prime

Kimura & Makino

CNF expression φ, we solve it by using the ellipsoid method, where the separation problem is solved by using a dynamic programming similar to the one for the Knapsack Problem. Note that linear globally ﬁxable or more general satisﬁability preserving assignments cannot be easily formulated as a linear programming problem from given linear inequalities. In this paper, we obtain the following algorithmic results. First, we provide a pseudopolynomial time algorithm to ﬁnd a linear locally-ﬁxable 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 & Johnson, 1979, Section 4). 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} (see Theorem 7 in Section 4). By extending the ﬁrst result, we provide a pseudo-polynomial time algorithm to ﬁnd a linear locally-ﬁxable assignment for the (general) integer linear system (see Theorem 8 in Section 4). This is obtained by making use of the following encoding known as order encoding (Tamura, Taga, Kitagawa, & Banbara, 2009) that transforms 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 note that the number of clauses in the order encoding might be exponential in d in general and hence we cannot construct the encoded CNF explicitly. Here, the ellipsoid method again copes with this diﬃculty. Similar to the results for SAT by Kullmann (2000) and van Maaren (2000), we show that TVPI, Horn and q-Horn integer linear systems can be solved by repeatedly obtaining a linear locally-ﬁxable assignment (see Theorem 9). The rest of the paper is organized as follows. In Section 2, we formally deﬁne the CSP and introduce several (linear) satisﬁability preserving assignments considered in the paper. In Section 3, we investigate the maximality of linear satisﬁability preserving assignments in terms of the set of vectors and the set of partial assignments. Section 4 presents the application of linear satisﬁability preserving assignments to integer linear systems.

2. Preliminaries

In this section, we ﬁrst ﬁx the notation to represent the constraint satisfaction problem (CSP), and deﬁne several satisﬁability preserving assignments. We then introduce linear satisﬁability preserving assignments, and ﬁnally recall the equivalence of optimization and separation on well-described polytopes.

2.1 Constraint Satisfaction Problem and Satisﬁability Preserving Assignments

Let V denote a set of variables with size n = |V |. Let D denote the ﬁnite 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

Linear Satisfiability Preserving Assignments

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 = (x C1, . . . , x Ck), R , where x C1, . . . , x Ck V are variables and R is a kary relation on D. (x C1, . . . , x Ck) is called a scope of the constraint and {x C1, . . . , x Ck} is written as V (C). We denote by SC the set of the total assignments satisfying the constraint C = (x C1, . . . , x Ck), R , that is, SC = {a Dn : (a C1, . . . , a Ck) R}. An instance of the constraint satisfaction problem (CSP) is deﬁned 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 satisﬁes every constraint, i.e., (a C1, . . . , a Ck) R holds for every constraint (x C1, . . . , x Ck), R C. Hence, A DV is a solution if and only if A C C SC holds. The CSP is the problem of ﬁnding a solution to a given instance (V, D, C). The Boolean satisﬁability 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) φ = m i=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 ﬁnite domain) is also contained in CSPs, where each constraint is given as a linear inequality. For a partial assignment A and X var(A), the restriction of A to X, denoted by A|X, is deﬁned 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 satisﬁability preserving if the satisﬁability 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 satisﬁability 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 satisﬁability preserving. We now introduce several (globally and locally) satisﬁability preserving assignments.

Deﬁnition 1 (Globally satisﬁability 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 ﬁxable 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 deﬁnition, a partial assignment A is globally satisfying if and only if S[A] = DV \var(A) holds. Moreover, A is globally ﬁxable if and only if S[A] S[B] holds for any partial assignment B such that var(B) = var(A).

Deﬁnition 2 (Locally satisﬁability preserving assignment). Let (V, D, C) be a CSP instance, and let A be a partial assignment.

Kimura & Makino

(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 ﬁxable for (V, D, C) if for any constraint C, it is globally ﬁxable for (V, D, {C}).

By deﬁnition, local ﬁxability and autarky coincide for CNFs. See also the proof of Theorem 2 in Section 3.

Example 1. Let (V = {x1, x2, x3}, D = {0, 1, 2}, C) be a CSP instance whose solution set S is given as S = {(0, 1, 1), (0, 2, 1), (1, 1, 0), (1, 1, 1), (1, 1, 2)}.

Then a partial assignment (1, 1, ) is globally satisfying for (V, D, C), since S[(1, 1, )] = D{x3} holds. Moreover, (0, , 1) is globally ﬁxable for (V, D, C), since for a partial assignment A with var(A) = {x1, x3}, we have S[A] = {(1), (2)} if A = (0, , 1), {(1)} if A = (1, , 0), (1, , 1) or (1, , 2), and otherwise. We also see that (0, , 1) is not globally satisfying for (V, D, C) and that (1, , 0) is not globally ﬁxable for (V, D, C).

Example 2. Let (V = {x1, x2, x3}, D = {0, 1, 2, 3}, C) be a CSP instance, where C is given by a linear system 2x1 + 3x2 x3 3 3x1 4x3 2 x2 x3 5. (1)

As mentioned, each inequality corresponds to a constraint. We can see that the three partial assignments ( , 1, 0), ( , 2, ), and (3, , ) are respectively locally satisfying, autark, and locally ﬁxable for (V, D, C). To see that ( , 1, 0) is locally satisfying for (V, D, C), we substitute it to the linear system: 2x1 0 3x1 2 0 4. (2)

Note that all inequalities in (2) are satisﬁed for any assignment to x1, which implies that ( , 1, 0) is locally satisfying. We next show that ( , 2, ) is autark for (V, D, C). Note that x2 is contained in the ﬁrst and third constraints. We substitute it into those constraints to obtain 2x1 x3 3 x3 3. (3)

Both the constraints are satisﬁed for any assignment to x1 and x3, which implies that ( , 1, 0) is autark. Finally, (3, , ) is locally ﬁxable, since all the coeﬃcients of x1 are nonnegative in (1) and 3 is the maximum in D.

We remark that ﬁxable assignments were introduced by Bordeaux et al. (2008) for single variable assignments and are also known as safe assignments in the literature (e.g., Kleine B uning & Kullmann, 2009). The concept of autark assignments was introduced by

Linear Satisfiability Preserving Assignments

Monien and Speckenmeyer (1985) for the Boolean case D = {0, 1} to construct fast exact algorithms for SAT, and was investigated by Kullmann (2000). Autark assignments for general constraints were studied by Kleine B uning and Kullmann (2009) and Kullmann (2011).

Satisﬁability preserving assignments are hereditary, i.e., if a partial assignment A is satisﬁability preserving, then A|X is also satisﬁability preserving for any X var(A). However, no other concepts deﬁned above are hereditary. For example, consider a CNF φ = (x1 x2 x3)(x1 x2 x3). Then a partial assignment (1, 0, ) is globally satisfying for φ. On the other hand, neither (1, , ) nor ( , 0, ) is globally satisfying. Similarly, this example shows that none of the concepts such that globally ﬁxable, locally satisfying, autark, and locally ﬁxable assignments is hereditary.

Finally, we introduce notation to represent the sets of the satisﬁability preserving assignments.

Deﬁnition 3. For a CSP instance I, we deﬁne 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 ﬁxable, locally ﬁxable and satisﬁability preserving partial assignments of I, respectively.

2.2 Linear Satisﬁability Preserving Assignments

In this subsection, we introduce linear satisﬁability preserving assignments after reviewing several basic geometric concepts. In what follows 0 denotes the all-zero vector of appropriate size.

Let R denote the set of reals. A subset Z Rn is said to be convex if (1 λ)y + λz Z holds for any y, z Z and 0 < λ < 1. A subset Z Rn is a cone if λy Z holds for any y Z and λ > 0. For a subset Z Rn, its convex hull is the unique smallest convex set containing Z and denoted by conv(Z). For a subset Z Rn, its conic hull is deﬁned as {λy: λ > 0, y Z}. For a y Rn, let |y| denotes the Euclidean norm of y, i.e., |y| = (y2 1 + + y2 n)1/2. For a vector y Rn and a real ε > 0, let B(y, ε) R be the ball with the center y and the radius ε, i.e., B(y, ε) = {z Rn : |z y| ε}. For a subset Z Rn, its closure is deﬁned as cl(Z) = {y Rn : ε > 0, B(y, ε) Z = }, and its interior is deﬁned as int(Z) = {y Rn : ε > 0, B(y, ε) Z}.

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. A subset Z Rn is called a (closed) polyhedron if it is the solution set of a system of linear inequalities, i.e., Z = {y Rn : My b} holds for some m n matrix M and a vector b Rm, and is called an open polyhedron if Z = {y Rn : My b} holds for some matrix M and a vector b. A polyhedron Z that is bounded, i.e., Z B(0, γ) for some γ > 0, is called a polytope. 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.

In order to deﬁne linear satisﬁability preserving assignments for Boolean CSPs with V = {x1, . . . , xn} and D = {0, 1}, we identify a vector y Rn with a partial assignment

Kimura & Makino

ay {0, 1, }n such that

1 if yj > 0, 0 if yj < 0, otherwise.

We note that the jth coordinate of Rn corresponds to Boolean variable xj. We also note that this identiﬁcation 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 deﬁne the set of vectors corresponding to P by Y (P) = {y Rn : ay P}. Note that Y (P) is a (not necessarily convex) cone.

Deﬁnition 4. Let (V, D = {0, 1}, C) be a Boolean CSP instance. A subset P of globally satisfying (resp., globally ﬁxable, locally satisfying, autark, locally ﬁxable, and satisﬁability 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.

Example 3. Let I = (V = {x1, x2}, D = {0, 1}, C) be a SAT instance, where C is given by a CNF φ = x1 x2. Then we have

Ppresv(I) = {0, 1, }2 \ {(0, 0)}, Pautark(I) = Pℓ-fix(I) = Pg-fix(I) = {(0, 1), (1, 0), (1, 1), (1, ), ( , 1), ( , )}, Pℓ-sat(I) = Pg-sat(I) = {(0, 1), (1, 0), (1, 1), (1, ), ( , 1)}. (5)

Consider the three polyhedral cones deﬁned by linear systems:

K1 = {y R2 : y1 0, y1 y2 0}, K2 = {y R2 : y1 + y2 0}, K3 = {y R2 : y1 + y2 > 0}, (6)

where we note that the inequality in the third system is strict. Then we have

K1 Y (Ppresv(I)), K2 Y (Pautark(I)), and K3 Y (Pℓ-sat(I)). (7)

In fact, we have

P(K1) Ppresv(I), P(K2) = Pautark(I), and P(K3) = Pℓ-sat(I). (8)

Kullmann (2000) introduced unweighted linear autark assignments for the SAT problem1. Namely, for a CNF φ = m i=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

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

Linear Satisfiability Preserving Assignments

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 & 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 Section 3. We here emphasize that (un)weighted linear autark and globally satisfying partial assignments introduced by Kullmann are special cases of linear autark and globally satisfying partial assignments introduced in this paper. However, it turns out that they provide good convex inner approximations for autark and globally satisfying partial assignments; see Section 3 for more details. Linear satisﬁability preserving assignments for non-Boolean CSPs are deﬁned via transformations to Boolean CSPs, which can be found in Section 4.

2.3 Optimization and Separation

We here brieﬂy summarize the relationship between optimization and separation via the ellipsoid method (e.g., Gr otschel, Lov asz, & Schrijver, 1993), which will be used in Section 4. Let Q denote the set of rationals.

Problem 1 (Optimization Problem for Polytopes). Given a polytope Z Rn and a vector α Qn, either

(i) assert that Z is empty, or

(ii) ﬁnd a vector z Z that maximizes αy over Z.

Problem 2 (Separation Problem for Polytopes). Given a polytope Z Rn and a vector z Qn, decide whether z Z, and if not, ﬁnd a hyperplane that separates z from Z; more exactly, ﬁnd a vector α Qn such that αz > max{αy: y Z}.

For a polytope Z Rn and a positive integer ℓ, Z has facet-complexity at most ℓif there exists a system of inequalities with rational coeﬃcients that has solution set Z and such that the encoding length of each inequality of the system is at most ℓ. A well-described polytope is a triple (Z; n, ℓ) where Z Rn is a polytope with facet complexity at most ℓ.

Theorem 1 (Gr otschel et al., 1993, Thm. 6.4.9). Each of the strong optimization and separation problems can be solved in oracle-polynomial time for any well-described polytope given by an oracle for the other problem.

Kimura & Makino

3. Properties of Satisﬁability Preserving Assignments for the Boolean CSP

In this section, we restrict our attention to the Boolean CSP and discuss several fundamental properties of satisﬁability preserving assignments. The main results of the section are summarized as follows.

The inclusion relationships between satisﬁability preserving assignments including their local variants (Subsection 3.1).

Basic properties of the set of the vectors corresponding to satisﬁability preserving assignments (Subsection 3.2).

Maximality of weighted linear satisﬁability preserving assignments deﬁned by matrices in the qualitative classes of the clause-variable matrices (Subsections 3.3 and 3.4).

From these results we can deﬁne a large family of linear satisﬁability preserving assignments, from which we can compute in (pseudo-)polynomial time a satisﬁability preserving assignment for integer linear system; see Section 4.

3.1 Relationships between Satisﬁability Preserving Assignments

In this subsection, we summarize in Theorem 2 the inclusion relationships between several satisﬁability preserving assignments. Recall that a CNF φ is prime if replacing a clause c φ by a proper subclause of c produces a CNF which is not equivalent to φ.

Theorem 2. Let I be a CSP instance. Then the following relations hold.

Pℓ-sat(I) = Pg-sat(I) Pautark(I) Pℓ-fix(I) Pg-fix(I) Ppresv(I). (9)

Moreover, if the constraints are represented by a CNF, then we have

Pautark(I) = Pℓ-fix(I), (10)

and if the constraints are represented by a prime CNF, then we have

Pℓ-fix(I) = Pg-fix(I). (11)

By Theorem 2, in general, satisﬁability preserving assignments considered in this paper form a total preorder, where a binary relation is a preorder if it is reﬂexive and transitive, and in addition total if any two elements are comparable. In the preorder, global ﬁxability is the largest notion of satisﬁability preserving assignments and local satisﬁability (i.e., satisﬁability) is the smallest one. Moreover, autarky and local ﬁxability coincide if the constraints are given by a CNF, and local ﬁxability and global ﬁxability coincide if the constraints are given by a prime CNF. Hence, autarky, local ﬁxability, and global ﬁxability all coincide in a prime CNF. We note that a part of Theorem 2 is folklore in the CSP community and are obtained from basic observations. However, we cannot ﬁnd this from any textbook, and it is important to know it for the following reasons.

Linear Satisfiability Preserving Assignments

In order to reduce the problem size by using satisﬁability preserving assignment, it is desired to ﬁnd a satisﬁability preserving assignment in the largest class: a globally ﬁxable assignment in general or in CNFs, and a globally ﬁxable (i.e., locally ﬁxable and autark) assignment in prime CNFs. You might think that it is nonsense to deal with prime CNF instances, since we can easily see satisﬁability or unsatisﬁability of the instance if it is represented by a prime CNF. However, it will be used in Section 4 to compute a linear locally ﬁxable assignment of an integer linear system by implicitly constructing a prime CNF expression for each linear inequality. Before proving the theorem, we show by the following examples that no other relation than (9) in Theorem 2 holds for the general CSP.

Example 4. Consider the following four Boolean CSP instances Ii = (V, D, Ci) (i = 1, 2, 3, 4) with two variables, i.e., V = {x1, x2} and D = {0, 1}.

(i) Let C1 be given as a CNF φ = x1x2, namely, C1 = { (x1), {(1)} , (x2), {(1)} }. Then (1, ) is contained in Pautark(I1), but not in Pg-sat(I1). Indeed, (1, ) is satisfying for the ﬁrst constraint, and the second constraint does not contain variable x1 that is ﬁxed by (1, ). Hence, it is autark. On the other hand, it is not globally satisfying for I1, since (1, 0) is not a solution to I1. (ii) Let C2 be given as a single inequality x1 + x2 2, namely, C2 = { (x1, x2), {(1, 1)} }. Then (1, ) is contained in Pℓ-fix(I2), but not in Pautark(I2). Indeed, for the solution set S = {(1, 1)} to the unique constraint, we have S[(1, )] S[(0, )] and thus (1, ) is locally ﬁxable. However, it is not autark, since (1, 0) is not contained in S. (iii) Let C3 be given as a CNF φ = x1(x1 x2), namely, C3 = { (x1), {(1)} , (x1, x2), {(0, 1), (1, 0), (1, 1)} }. Then ( , 0) is contained in Pg-fix(I3), but not in Pℓ-fix(I3). Indeed, for the solution set S = {(1, 0), (1, 1)} to the instance, we have S[( , 0)] S[( , 1)] and thus ( , 0) is globally ﬁxable. However, it is not locally ﬁxable, since S [( , 0)] S [( , 1)] holds for the solution set S to the second constraint. (iv) Let C4 be given as a CNF φ = (x1 x2), namely, C4 = { (x1, x2), {(0, 1), (1, 0), (1, 1)} }. Then (0, ) is contained in Ppresv(I4), but not in Pg-fix(I4). Indeed, S[(0, )] = {(1)} = holds for the solution set S to the instance and hence it is satisﬁability preserving. However, it is not globally ﬁxable, since S[(0, )] S[(1, )] holds.

Proof of Theorem 2. We ﬁrst show (9). It is not diﬃcult from the deﬁnitions that

Pℓ-sat(I) = Pg-sat(I) Pautark(I) and Pg-fix(I) Ppresv(I). (12)

For Pautark(I) Pℓ-fix(I), let A be an autark assignment. If var(A) V (C) = for a constraint C, then SC[A](= DV \var(A)) includes SC[B] for any B Dvar(A). On the other hand, if var(A) V (C) = for a constraint C, then SC[A] = SC[B] for any B Dvar(A). Thus, A is locally ﬁxable and we have Pautark(I) Pℓ-fix(I). For Pℓ-fix(I) Pg-fix(I), let A be a locally ﬁxable assignment and S be the solution set of I. Recall that S = C C SC holds. Hence we have S[A] = C C SC[A]. Since for any B Dvar(A) we have SC[A] SC[B], it holds that S[A] = C C SC[A] C C SC[B] = S[B]. Hence A is globally ﬁxable. We then show (10). Let φ be a CNF and A be a locally ﬁxable assignment. For a clause c φ with V (c) var(A) = , there exists a partial assignment B such that c[B] = DV \var(A)

Kimura & Makino

holds. Since local ﬁxability of A implies that c[A] c[B] holds, we have c[A] = DV \var(A). Hence A is autark. We ﬁnally show (11). Let φ be a prime CNF that represents a Boolean CSP instance, and let A be a partial assignment. Assuming that A is not locally ﬁxable, we show that it is not globally ﬁxable. Let S be the set of the solutions of φ. Since A is not locally ﬁxable, there exists a clause c in φ such that Sc[A] Sc[B] for some partial assignment B. This implies that A is not a satisfying partial assignment for c, i.e., Sc[A] = {0, 1}V \var(A). Then, by primality of φ, there exists a globally satisfying total assignment A for φ that does not satisfy Sc[A], namely, A |V \var(A) Sc[A]. This implies that A |V \var(A) S[A]. Since A |V \var(A) S[A |var(A)], we have S[A] S[A |var(A)]. Hence A is not globally ﬁxable for S.

Since Pg-sat = Pℓ-sat holds for the general Boolean CSP in Theorem 2, we simply write Psat, and also write a satisfying partial assignment without having globally nor locally. Let us ﬁnally mention integer linear systems. Note that any CNF can be represented by a 0-1 integer linear system, where we recall that a 0-1 integer linear system is an integer linear system with D = {0, 1}. This is because a 0-1 assignment satisﬁes a clause c = ( j J+ xj j J xj) if and only if it satisﬁes j J+ xj + j J (1 xj) 1. Thus it follows from Example 4 that there exists a 0-1 integer linear system such that either (10) or (11) does not hold.

3.2 Characterizing Y (Ppresv(I)) and Y (Psat(I)) for Boolean CSP Instance I

Let I be an instance of the Boolean CSP, and let S be the solution set of I. We characterize Y (Ppresv(I)) and Y (Psat(I)) in terms of interior and closure of Y (S). We ﬁrst explain the relation between S and Y (S) where I is given by a CNF. Let us see Y (S), cl(Y (S)), and int(cl(Y (S))). Recall that n is the number of the variables. We write S(I) as the solution set of a CSP instance I.

Example 5. Consider the three Boolean CSP instances Ii = (V = {x1, x2}, D = {0, 1}, Ci) (i = 1, 2, 3), where I1 is given by a literal x1, I2 by a clause c = (x1 x2), and I3 by a CNF φ = x1 c. Let us see the diﬀerence between Y (S), cl(Y (S)), and int(cl(Y (S))).

Y (S(I1)) = {y R2 : (y1 > 0 and y2 > 0) or (y1 > 0 and y2 < 0)}, cl(Y (S(I1))) = {y R2 : y1 0}, and int(cl(Y (S(I1)))) = {y R2 : y1 > 0}.

From the above example, we can see that Y (S) only contains the vectors corresponding to the solutions and hence we do not have the vectors corresponding to partial assignments. By taking the closure of Y (S), we obtain the vector corresponding to partial assignments, and in fact we have cl(Y (S)) = Y (Ppresv). However, it also contains vectors not corresponding to satisfying partial assignments. By further taking the interior, we ﬁnally get the vectors that correspond to satisfying partial assignments. Namely, we have int(cl(Y (S))) = Y (Psat). We will show that these equations hold for the general Boolean CSP in the following.

Linear Satisfiability Preserving Assignments

We also have

Y (S(I2)) = {y R2 : (y1 < 0 and y2 > 0), (y1 < 0 and y2 < 0), or (y1 > 0 and y2 > 0)}, cl(Y (S(I2))) = {y R2 : y1 0 or y2 0}, and int(cl(Y (S(I2)))) = {y R2 : y1 < 0 or y2 > 0},

and Y (S(I3)) = {y R2 : y1 > 0 and y2 > 0}, cl(Y (S(I3))) = {y R2 : y1 0 and y2 0}, and int(cl(Y (S(I3)))) = {y R2 : y1 > 0 and y2 > 0}.

Note that these examples show that Y (S), cl(Y (S)) and/or int(cl(Y (S))) might not be convex in general.

In the above example, we have cl(Y (S(I1) S(I2))) = cl(Y (S(I1))) cl(Y (S(I2))). Therefore, we cannot compute cl(Y (S)) by simply taking the intersection of the closures of the solutions to each constraint. We now characterize satisﬁability preserving and satisfying partial assignments of the Boolean CSP.

Proposition 1. Let I = (V, D = {0, 1}, C) be a Boolean CSP instance with solution set S, i.e., the set of satisfying total assignments. Then we have the following statements.

(i) If S = , then Y (Ppresv(I)) = cl(Y (S)).

(ii) Y (Psat(I)) = int(cl(Y (S))).

Proof. (i): For Y (Ppresv(I)) cl(Y (S)), suppose that y is not contained in cl(Y (S)). We show that y Y (Ppresv), i.e., ay is not satisﬁability preserving. Since y cl(Y (S)), there exists an ε > 0 such that B(y, ε) cl(Y (S)) = . Thus, for suﬃciently small ε > 0, we have y + ε w Y (S) and ay+ε w j = ay j (j var(ay)) for all w { 1, 1}n. This implies that ay is not extendable to any satisfying total assignment. Hence, ay is not satisﬁability preserving. For Y (Ppresv(I)) cl(Y (S)), suppose that y is contained in cl(Y (S)). Then for suﬃciently small ε > 0, y + εz Y (S) and ay+εz j = ay j (j var(ay)) hold for some z B(0, 1). Thus, ay is extendable to a satisfying total assignment, implying that ay is satisﬁability preserving. (ii): If S = , then there exits no satisfying partial assignment. Thus, Y (Psat(I)) = . We also have Y (S) = and thus int(cl(Y (S))) = . Hence (ii) holds. We then assume that S = . For Y (Psat(I)) int(cl(Y (S))), assume that y Y (Psat(I)), i.e., ay is satisfying. Let ε be a positive real such that ε < |yj| for any yj = 0. We show that B(y, ε) cl(Y (S)), which implies that y int(cl(Y (S)). Let y B(y, ε) and let ε > 0. We have to show that B(y , ε ) Y (S) = holds. Deﬁne z B(0, 1) as |zj| < (|yj| ε)/ε

if yj = 0, zj/y j > 0 if yj = 0 and y j = 0, and zj > 0 otherwise (i.e., yj = y j = 0). Then

we have ay +ε z j = ay j (j var(A)) and var(ay +ε z) = V . Since ay is satisfying, ay +ε z is a satisfying total assignment, i.e., a solution. Hence we have B(y , ε ) Y (S) = . For Y (Psat(I)) int(cl(Y (S))), suppose that y is contained in the interior of the closure of Y (S). Then for any w { 1, 1}n, by taking suﬃciently small ε > 0, we have y + εw

Kimura & Makino

int(cl(Y (S))), ay+εw j = ay j (j var(A)) and var(ay+εw) = V (i.e., (y + εw)j = 0 for all j). Note that cl(Y (S)) Y ({0, 1}V \ S) = . Hence y + εw int(cl(Y (S))) and (y + εw)j = 0 for all j imply that y + εw Y (S). Therefore ay+εw is a satisfying total assignment. Thus, ay is arbitrarily extendable to a satisfying total assignment and hence it is satisfying.

If S = , then (i) does not hold, since every partial assignment is satisﬁability preserving, i.e., Y (Ppresv(I)) = Rn, and cl(Y (S)) = , implying that Y (Ppresv(I)) = cl(Y (S)). Proposition 1 shows that Y (Ppresv) and Y (Psat) can be characterized by Y (S). In this paper, we consider the vector space corresponding to partial assignments. Note that we can obtain a satisﬁability preserving or satisfying partial assignments by ﬁnding a point in Y (Ppresv) or Y (Psat). However, these sets are non-convex in general and it is hard to ﬁnd a point in these sets. We thus consider convex inner approximations of these sets, where convexity helps to ﬁnd a point in these sets. We want to deﬁne large convex inner approximations, and hence investigate maximal convex inner approximations in the following two subsections.

3.3 Maximality of Weighted Linear Satisﬁability Preserving Assignments for General CNFs

We here investigate convex inner approximation of satisﬁability preserving assignments for general CNFs. Before stating the main results of this subsection, we state several auxiliary results (Propositions 2-5). The following proposition shows that we have only to consider convex cones to ﬁnd large convex subsets in terms of the set of vectors.

Proposition 2. Let I = (V, D = {0, 1}, C) be a Boolean CSP instance. (i) For a closed subset Z Y (Ppresv(I)), there exists a closed cone Z such that Z Z Y (Ppresv(I)). If Z is in addition convex (resp., polyhedral), then Z can be taken from convex (resp., polyhedral) cones. (ii) For an open subset Z Y (Psat(I)), there exists an open cone Z such that Z Z Y (Psat(I)). If Z is in addition convex (resp., polyhedral), then Z can be taken from convex (resp., polyhedral) cones.

Proof. (i): Let Z be the closure of the conic hull of Z. Then we have Z Y (Ppresv(I)), since Y (Ppresv(I)) is a closed cone by Proposition 1. It is well known that convexity and polyhedrality are preserved by taking the closure of the conic hull (e.g., Rockafellar, 1970, Thm. 19.7). (ii): Let Z be the conic hull of Z. Then Z is open, and we have Z Y (Psat(I)), since Y (Psat(I)) is a cone. Since convexity and polyhedrality are preserved by taking the conic hull, the proof is completed.

By Proposition 1, Y (Ppresv(I)) and Y (Psat(I)) are closed and open, respectively. Hence, the proposition above restricts attention to closed and open subsets of Y (Ppresv(I)) and Y (Psat(I)), respectively. We note that the closedness condition of Z in (i) is not necessary. We then show the following proposition on the clause-variable matrix.

Proposition 3. Let I = (V, D = {0, 1}, C) be a SAT instance, where C is given by a CNF φ. Then we have

Linear Satisfiability Preserving Assignments

(i) cl(K (Mφ)) K (Mφ) Y (Pautark(I)) Y (Ppresv(I)), (ii) K (Mφ) Y (Psat(I)).

Proof. It is known by Kullmann that K (Mφ) is contained in Y (Pautark(I)) (Kullmann, 2000, Lemma 4.9) and K (Mφ) is contained in Y (Psat(I)) (Kullmann, 2003, Lemma 3.2). Moreover, we have K (Mφ) K (Mφ) by deﬁnition, and since taking the closure preserves the inclusion relation, we have cl(K (Mφ)) cl(K (Mφ)) = K (Mφ). The last equality holds since K (Mφ) is a closed set. Finally, by Theorem 2, we have Y (Pautark(I)) Y (Ppresv(I)).

We note that cl(K (Mφ)) Y (Psat(I)) and/or cl(K (Mφ)) = K (Mφ) might hold in general. Let I1 = (V1 = {x1}, D = {0, 1}, F1), where C1 is given by φ1 = x1, and I2 = (V2 = {x1, x2}, D = {0, 1}, F2), where C2 is given by φ2 = (x1 x2)(x1 x2). Then we have cl(K (Mφ1)) = {y1 R: y1 0} and Y (Psat(I1)) = {y1 R: y1 > 0}, which implies that cl(K (Mφ1)) Y (Psat(I1)) holds. Also, we have cl(K (Mφ2)) = and K (Mφ2) = {y R2 : y1 = y2}, implying that cl(K (Mφ2)) = K (Mφ2) holds. By Proposition 3, an autark assignment A is called unweighted linear if A P(K (M)) holds, and a satisfying partial assignment A is called unweighted linear if A P(K (M)) holds.

Example 6. Let (V = {x1, x2, x3}, D = {0, 1}, C) be a SAT instance, where C is given by a CNF φ = (x1 x2)(x1 x3)(x2 x3). Then an autark assignment ( , , 1) and a satisfying partial assignment (1, 1, ) are unweighted linear, since (0, 0, 1) K (Mφ) and (1, 2, 0) K (Mφ) hold.

We note that K (Mφ) = {0} and K (Mφ) = might hold in general as the next example shows.

Example 7. Let I = (V = {x1, x2, x3}, D = {0, 1}, C) be a SAT instance, where C is given by a CNF φ = (x1 x2 x3)(x1 x2 x3)(x1 x2 x3)(x1 x2 x3). It can be veriﬁed that

Ppresv(I) = {0, 1, }3 \ {(0, 0, 0), (0, 1, 1), (1, 0, 1), (1, 1, 0)}, Pautark(I) = {(0, 0, 1), (0, 1, 0), (1, 0, 0), (1, 1, 1), ( , , )}, Psat(I) = {(0, 0, 1), (0, 1, 0), (1, 0, 0), (1, 1, 1)}. (13)

On the other hand, there exists no nontrivial unweighted linear autark assignment nor unweighted linear satisfying partial assignment. We note that

1 1 1 1 1 1 1 1 1 1 1 1

and hence K (Mφ) = {0} and K (Mφ) = hold. Indeed, summing the inequalities y1 + y2 +y3 0 and y1 y2 y3 0 in Mφy 0 yields y1 0. Similarly, from y1 +y2 y3 0 and y1 y2 + y3 0, we obtain y1 0. This implies y1 = 0. We can obtain y2 = y3 = 0 in a similar way. Hence, we have K (Mφ) = {0}. By replacing the inequalities by strict inequalities in the above argument, we obtain y1 > 0 and y1 < 0. Hence, we have K (Mφ) = .

Kimura & Makino

We then consider weighted linear satisﬁability preserving assignments for a CNF φ, i.e., partial assignments deﬁned by some matrix M in Q(Mφ) or Q0(Mφ). Here, Q0(M) denotes 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. Recall that Q(M) is deﬁned in Subsection 2.2.

Proposition 4. Let I = (V, D = {0, 1}, C) be a SAT instance, where C is given by a CNF φ. Then we have the following 3 statements. (i) cl(K (M)) Y (Ppresv(I)) for all M Q0(Mφ). (ii) K (M) Y (Pautark(I)) for all M Q(Mφ). (iii) K (M) Y (Psat(I)) for all M Q0(Mφ).

Proof. Since (ii) is known by Kullmann (2003, Lemma 3.5), we show (i) and (iii) only. We ﬁrst show (iii). (iii): Let y be a vector in K (M). Then for each c φ, there exists an element j such that (xj c and yj > 0) or (xj c and yj < 0) hold. In either case, ay should satisfy c, implying that it satisﬁes φ. (i): We have K (M) Y (Psat(I)) for any M Q0(Mφ) by (iii). By taking the closure of K (M) and Y (Psat(I)), we obtain cl(K (M)) cl(Y (Psat(I))). Note that cl(Y (Psat(I))) cl(Y (Ppresv)) = Y (Ppresv(I)) holds, where the last equality follows from Proposition 1. Thus we have cl(K (M)) Y (Ppresv(I)).

We note that the proof of (iii) in Proposition 4 is similar to the one that K (M) Y (Psat(I)) for all M Q(Mφ) by Kullmann (2003, Lemma 3.2). By Proposition 4, 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 satisfying if we have P = P(K (M)) for an M Q0(Mφ). The next example shows that weighted linear satisﬁability preserving assignments dominate unweighted ones, which implies that weighed linear satisﬁability preserving assignments are more useful than unweighted ones.

Example 8. Consider again the CSP instance (V, D, C) given in Example 7, i.e., V = {x1, x2, x3}, D = {0, 1} and C is given by a CNF φ = (x1 x2 x3)(x1 x2 x3)(x1 x2 x3)(x1 x2 x3). Recall that there exists no nontrivial unweighted linear autark assignment nor unweighted linear satisfying partial assignment for φ. On the other hand, deﬁne matrices M1 Q0(Mφ) and M2 Q(Mφ) by

1 1 1 1 0 0 0 1 0 0 0 1

1 1 1 2 1 1 1 2 1 1 1 2

Then we have

P(cl(K (M1))) = {(1, 1, 1), (1, 1, ), (1, , 1), (1, , ), ( , 1, 1), ( , 1, ), ( , , 1), ( , , )}, P(K (M2)) = P(K (M1)) = {(1, 1, 1), ( , , )}. (16)

These provide weighted linear satisﬁability preserving assignments. For example, (1, 1, ) is a cl(K (M1))-linear satisﬁability preserving assignment.

Linear Satisfiability Preserving Assignments

We note that we cannot replace cl(K (M)) with K (M) in Proposition 4 (i). Namely, for a CNF φ and a matrix M Q0(Mφ), K (M) is not always contained in Y (Ppresv(I)). For example, consider φ = (x1 x2)(x1 x2) and

M = ( 0 1 0 1

) Q0(Mφ). (17)

( 1, 0) is clearly contained in K (M), while not in Ppresv(I), since (0, ) is not satisﬁability preserving. Therefore we have K (M) Ppresv(I). We also note that {cl(K (M)): M Q0(Mφ)} and {K (M): M Q(Mφ)} are incomparable in general. For example, for φ = (x1 x2) and

M = ( 1 0 ) Q0(Mφ), (18)

there exists no matrix M Q(Mφ) such that cl(K (M)) K (M ). Moreover, for φ = (x1 x2)(x1 x2) and

M = ( 1 1 1 1

) Q(Mφ), (19)

there exists no matrix M Q0(Mφ) such that K (M) cl(K (M )). The following proposition shows that the linear autark and satisfying partial assignments in Proposition 4 are enough to ﬁnd autark and satisfying partial assignments.

Proposition 5 (Kullmann, 2003, Lemmas 3.2 and 3.5). Let I = (V, D, C) be a SAT instance, where C is given by a CNF φ.

(i) For any A Pautark(I), there exists a matrix M Q(Mφ) such that A is K (M)-linear.

(ii) For any A Psat(I), there exists a matrix M Q(Mφ) such that A is K (M)-linear.

We next study the maximality of these linear satisﬁability preserving assignments, which can be used to heuristically ﬁnd a satisﬁability preserving assignment.

Theorem 3. 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).

Proof. (i): For a clause c = j J+ xj j J xj in φ with J+ J = , let Zc be a non-closed cone deﬁned by Zc = {y Rn : yj 0 (j J+), yj 0 (j J ), j J+ yj + j J yj > 0}. Then Zc contains no point in Y (Pautark(I)) and thus K (N) Zc = holds. Therefore, there exists a separating hyperplane between K (N) and Zc, i.e., there exists a vector α Rn such that K (N) {y Rn : αy 0} and Zc {y Rn : αy < 0} hold (e.g., Rockafellar, 1970, Thm. 11.7). We claim that αj > 0 for all j J+, αj < 0 for all j J , and αj = 0 for all j J+ J .

Kimura & Makino

Let ej denote the jth unit vector. Since ej and ej are respectively contained in Zc for j J+ and j J , we have α( ej) < 0 and αej < 0 respectively, which proves the claim for j J+ and j J . For j J+ J , deﬁne two vectors z and z by zj = 1, z j = 1, zk = z k = 0 if k J+ J {j}, zk = z k = ε if k J+, and zk = z k = +ε if k J for an ε > 0. Then z and z are contained in Zc and hence we have αz < 0 and αz < 0. This implies that ε( k J+ αk k J αk) < αj < ε( k J+ αk k J αk). Since ε > 0 is arbitrary, we have αj = 0. Since c is arbitrary, the claim implies (i) in the theorem. (ii): For a clause c = j J+ xj j J xj in φ with J+ J = , let Zc = {y Rn : yj 0 (j J+), yj 0 (j J )}. Then Zc is a closed cone which contains no point in Y (Psat(I)). This implies that K (N) Zc = holds. Since K (N) is open, there exists a vector α Rn such that K (N) {y Rn : αy > 0} and Zc {y Rn : αy 0}. We claim that αj 0 for all j J+, αj 0 for all j J , and αj = 0 for all j J+ J . Since ej, ej and ej are respectively contained in Zc for j J+, j J and j J+ J , we have α( ej) 0, αej 0 and α( ej) 0 respectively. This proves the claim. Since α = 0 and c is arbitrary, the claim implies (ii) in the theorem.

Note that (i) in Theorem 3 extends Kullmann s result (Proposition 5 (i)), since for any autark assignment, there exists a polyhedral cone containing a vector corresponding to the assignment. By Theorem 3, {K (M): M Q(Mφ)} and {K (M): M Q0(Mφ)} represent families of convex sets which are large in Y (Pautark(I)) and Y (Psat(I)). However, the polyhedral cones respectively might not be maximal convex subsets of Y (Pautark(I)) and Y (Psat(I)), as the next examples show. 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.

Example 9. Let I = (V = {x1, x2}, D = {0, 1}, C) be a SAT instance, where C is given by a CNF φ = x1(x1 x2). For any M Q(Mφ), K (M) is not a maximal convex subset of Y (Pautark(I)). Note that Y (Pautark(I)) = {y R2 : y1 > 0} {y R2 : y1 0, y2 0} holds. For any M Q(Mφ), let y = (M22, M21 1). Then y is contained in Y (Pautark(I)), but not in K (M), since it violates M21y1 + M22y2 0. Moreover, we can see that conv(K (M) {y}) is contained in Y (Pautark(I)). Hence, there exists a convex set contained in Y (Pautark(I)) that strictly contains K (M), implying that K (M) is not a maximal convex set in Y (Pautark(I)).

We recall that, by Proposition 2 (i), for any matrix N that represents linear satisﬁability preserving assignments, there exists a matrix M such that K (N) K (M) Y (Ppresv(I)). Example 9 shows that this M does not belong to Q(Mφ) in general.

Example 10. Let I = (V = {x1, x2}, D = {0, 1}, C) be a SAT instance, where C is given by a CNF φ = x1 x2. Then no M Q0(Mφ) produces a maximal convex set K (M) of Y (Psat(I)). This is because conv(K (M) {y}) Y (Psat(I)) holds for y = (M12, M11) K (M) if M12 = 0, and y = (0, 1) K (M) if M12 = 0.

Note that Example 10 does not contradict Proposition 2 (ii), since Example 10 deals with non-open convex sets.

Linear Satisfiability Preserving Assignments

The next theorem shows that there exist maximal elements in {K (M): M Q(Mφ)} and {K (M): M Q0(Mφ)} in terms of partial assignments, which contrasts with Examples 9 and 10.

Theorem 4. 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)).

Proof. Since we have 3n partial assignments, there exist ﬁnite points y(1), . . . , y(ℓ) C such that P({y(1), . . . , y(ℓ)}) = P(C). For (i), let Z denote the convex cone closure of y(i) (i = 1, . . . , ℓ). It follows that Z Y (Pautark(I)), since C is convex and Y (Pautark(I)) is a cone. By Theorem 3, there exists a matrix M Q(Mφ) such that Z K (M) holds. Then we have P(C) P(Z) P(K (M)). For (ii), let Z denote the convex hull of y(i) (i = 1, . . . , ℓ). It follows from convexity of C that Z C Y (Psat(I)). By applying a similar argument in the proof of Theorem 3, we have Z K (M) for some M Q0(Mφ).

We remark that K (Mφ) or K (Mφ) might not be maximal as seen in Examples 7 and 8.

3.4 Maximality of Weighted Linear Satisﬁability Preserving Assignments for Monotone CNFs

In this subsection we investigate convex inner approximation of satisﬁability preserving assignments for monotone and prime monotone CNFs. We show that several interesting properties hold for these CNFs, which are not satisﬁed for general CNFs. Recall that a CNF φ is called monotone if it contains no negative literal.

Theorem 5. 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).

Proof. We ﬁrst show the case of Psat(I). For a satisfying partial assignment A, let y be a vector in Rn deﬁned as yj = γ if aj = 1, yj = 1 if aj = 0, and yj = 0 otherwise (i.e., aj = ), where γ is a suﬃciently large real. Then it is clear that partial assignment ay is equal to A. Moreover, we have My 0. We can similarly show the case of autark assignments.

Theorem 5 does not hold if we replace Q(Mφ) by Q0(Mφ) for satisfying partial assignments. For example, for a monotone SAT instance I given by a monotone CNF φ = x1 x2, let M = (1 0) Q0(Mφ). Then we have P(K (M)) = {(1, 0), (1, 1), (1, )} Psat(I). We also remark that by Examples 9 and 10, even if φ is a monotone CNF, there does not always exist an M Q(Mφ) such that K (M) (resp., K (M)) is a maximal convex subset of Y (Pautark(I)) (resp., Y (Psat(I))). This contrasts with Theorem 5.

Kimura & Makino

We next consider prime monotone CNFs. Recall that a CNF φ is prime if replacing a clause c φ by a proper subclause of c produces a CNF which is not equivalent to φ. In this case, for autark assignments, maximality holds in terms of not only partial assignments but also convex sets in Y (Pautark(I)).

Theorem 6. Let I = (V, D, C) be a prime monotone SAT instance, i.e., a SAT instance, where C is given by a prime monotone CNF φ. Then any M Q(Mφ) deﬁnes a maximal convex subset K (M) of Y (Pautark(I)).

Proof. We claim that conv(K (M) {y}) Y (Pautark(I)) holds for any y K (M). Fix a vector y K (M). Then xj ci Mijyj + ε = 0 holds for some ci φ and ε > 0. If |ci| = 1, then Mijyj < 0 holds for the only xj ci, implying that yj < 0. Hence, ay does not satisfy ci and y is not contained in Y (Pautark(I)), which proves the claim. We therefore assume that |ci| 2. Let z be a vector in Rn deﬁned as zj = 1 Mij ( xk ci,k =j Mikyk + |ci| 1

|ci| ε) if xj ci, and zj = γ otherwise, where γ is suﬃciently large. We show that z K (M) and (y + z)/2 / Y (Pautark(I)) hold, which prove the claim since the former condition implies that (y + z)/2 conv(K (M) {y}) holds. In order to prove that z K (M) holds, we show that xj ci Mi jzj 0 holds for each ci φ. If ci = ci, we have

xj ci Mijzj = xj ci( xk ci,k =j Mikyk + |ci| 1

|ci| ε) = xj ci xk ci Mikyk xj ci Mijyj + (|ci| 1)ε = (|ci| 1)( xj ci Mijyj + ε) = 0.

On the other hand, if ci = ci, we have xj ci Mi jzj 0, since ci contains at least one variable not contained in V (ci) by primality of φ and γ is suﬃciently large. Next, we show that (y + z)/2 / Y (Pautark(I)) holds. For each xj ci,

yj + zj = yj + 1 Mij ( xk ci,k =j Mikyk + |ci| 1

= 1 Mij ( xj ci Mijyj + |ci| 1

= 1 Mij ( ε + |ci| 1

|ci| ε) < 0.

Hence, a partial assignment a(y+z)/2 does not satisfy ci, implying that (y + z)/2 is not contained in Y (Pautark(I)). This completes the proof.

Diﬀerent from Theorem 6, K (M) for M Q0(Mφ) is not always a maximal convex subset of Psat(I), which follows from Example 10. We also note that primality alone does not always yield maximality.

Example 11. Let I = (V = {x1, x2}, D = {0, 1}, C) be a SAT instance, where C is given by a prime CNF φ = (x1 x2)(x1 x2). Then no M Q(Mφ) \ {Mφ} produces a maximal convex subset K (M) of Y (Pautark(I)).

Linear Satisfiability Preserving Assignments

Indeed, let Z+ = {y R2 : y1 > 0, y2 > 0} and Z = {y R2 : y1 < 0, y2 < 0}. Then we have Y (Pautark(I)) = Z+ Z {0}. For any M Q(Mφ) \ {Mφ}, it holds that K (M) Z+ {0} or K (M) Z {0}. If K (M) Z+ {0}, then there exists a y Z+ which is not contained in K (M), since K (M) is closed and Z+ is open. It follows from convexity of Z+ {0} that conv(K (M) {y}) Z+ {0}. Hence, K (M) is not a maximal convex subset of Y (Pautark(I)). The case of K (M) Z {0} can be treated in a similar way.

We remark that maximality in Theorem 6 is used to heuristically compute a locally ﬁxable assignment, which can be found in the next section.

4. Computing a Satisﬁability Preserving Assignment for CSPs Given by Integer Linear Systems

In this section, we discuss how to compute a linear satisﬁability preserving assignment of CSPs given by integer linear systems. It is known that computing a nontrivial satisﬁability preserving assignment deﬁned in Section 2 is NP-hard, since we can solve the CSP by iteratively computing such partial assignments. We also note that it is still NP-hard to compute a partial assignment which is contained in some linear satisﬁability preserving assignments, by Proposition 5. Hence, we consider restricting linear satisﬁability preserving assignments. For CNFs φ, it is natural to consider linear autark assignments derived from matrices in Q(Mφ), in particular, unweighted linear autark assignments. For the 0-1 integer linear systems, we note that each constraint is unate (i.e., it can be represented by a monotone CNF by changing the polarity of variables appropriately). By Theorems 5 and 6, unweighted linear autark (i.e., globally ﬁxable) assignments for its prime CNF expression are maximal in terms of both the set of the corresponding vectors and partial assignments. We thus try to use the prime CNF expression of each inequality to obtain a maximal linear globally ﬁxable assignment of each inequality. However, we note that a prime CNF of an inequality might have exponentially many clauses with respect to the number of variables in the inequality. This implies that we cannot explicitly have linear inequalities that represent unweighted linear globally ﬁxable assignments. In this section, we study computing a linear locally ﬁxable assignment which is contained in the intersection of such unweighted linear globally ﬁxable assignments. We show that it can be computed in pseudo-polynomial time, even if some constraints have a non-ﬁxed number of variables. As a corollary, we show that TVPI, Horn, and q-Horn systems are solvable in pseudo-polynomial time by repeatedly computing such linear partial assignments, which is discussed in Subsection 4.2. We assume that d = |D| is a part of the input throughout the section. We ﬁrst consider the Boolean case, i.e., 0-1 integer linear systems, and then turn to the general case.

4.1 The Case of 0-1 Integer Linear Systems

In this subsection, we discuss the complexity of computing a satisﬁability preserving assignment of the Boolean CSP given by 0-1 integer linear systems.

Kimura & Makino

We consider a Boolean CSP instance I = (V, D = {0, 1}, C), where C is given by a linear system Gx h, (22)

where G is a matrix in Zm n and h is a vector in Zm. We note that each linear inequality in the system (22) is unate. To see this, consider a vector α 0 and a real β. Then a linear inequality αx β is monotone since αx β and x x clearly imply αx β. For a general α, by changing the polarity of the variables with αj < 0, we obtain a monotone linear inequality, implying that αx β is unate. It is known that every unate Boolean function has the unique prime CNF expression (e.g., Crama & Hammer, 2011). Let Ii denote the CSP instance that has a single constraint given as the ith inequality of (22). By Theorem 6, Y (Pg-fix(Ii)) is maximally (inner) approximated by K (Mφi) for the unique prime CNF expression φi of Ii, where primality implies Pautark(Ii) = Pg-fix(Ii) by Proposition 2. Consider a single inequality:

j J gjxj η, (23)

where J+, J V , J+ J = , gj > 0 for j J+ J , and η Z. Let U denote the set of the extreme infeasible points of (23), i.e., u U satisﬁes that u + ej is feasible to (23) if j J+ and uj = 0, and u ej is feasible to (23) if j J and uj = 1. Then it is known by, e.g., the work of Crama and Hammer (2011, Thm. 1.27) that φ = u U( j J+:uj=0 xj j J :uj=1 xj) is the unique prime CNF representing (23), which implies the following lemma.

Lemma 1. Let φ denote the unique prime CNF representing (23). Then we have

j J+:uj=0 yj

j J :uj=1 yj 0 (u U)

Let φi denote the unique prime CNF expression for the ith inequality in (22) for each i. Then we note that m i=1 K (Mφi) represents linear locally ﬁxable assignments. We show the following result for such assignments.

Theorem 7. We can ﬁnd in pseudo-polynomial time a nontrivial linear locally ﬁxable assignment in m i=1 K (Mφi) for the 0-1 integer linear system (22), 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.

In order to ﬁnd a nontrivial partial assignment in m i=1 K (Mφi), we solve the following two linear programming (LP) problems P+ ℓand P ℓfor each xℓ V :

Problem P+ ℓ maximize yℓ subject to Mφiy 0 (i = 1, . . . , m) 1 yj 1 (j = 1, . . . , n).

Problem P ℓ maximize yℓ subject to Mφiy 0 (i = 1, . . . , m) 1 yj 1 (j = 1, . . . , n). (25)

Linear Satisfiability Preserving Assignments

The constraints 1 yj 1 for j = 1, . . . , n in (25) ensure that the solution space is bounded. We note that the number of the inequalities in the LP problems (25) might be exponential in the size of the input. For example, for a linear inequality n j=1 xj n/2 , the set U of the extreme infeasible points is given by

j=1 uj = n/2 1

Hence |U| = ( n n/2 1 ) = Ω(2n/2 log n) holds, which implies that the LP problems (25) have exponentially many inequalities. Instead of solving (25) directly, we make use of the ellipsoid method described in Subsection 2.3. By Theorem 1 in Subsection 2.3, optimization is polynomially equivalent to solving the separation problem. Namely, given a y Rn, we compute an inequality in (25) that is violated by y, if y is infeasible. Since 1 yj 1 can be checked eﬃciently, we consider how to check if Mφiy 0 is satisﬁed for each i.

Let J(i) + = {j V : Gij > 0}, J(i) = {j V : Gij < 0} and U(i) denote the set of extreme infeasible points of the ith constraint in (22). Then by Lemma 1, the following integer LP problem computes mink{(Mφi)ky}, where (Mφi)k denotes the kth row vector of Mφi.

j J(i) + yj(1 uj)

j J(i) yjuj (=

j J(i) + J(i) yjuj +

j J(i) + yj)

subject to u U(i).

Hence the optimal value of (27) is at least zero if and only if Mφiy 0 holds. It is easy to see that u U(i) if and only if

j J(i) + J(i) Gijuj hi 1,

2) u {0, 1}n,

3) u is extreme, i.e.,

j J(i) + J(i) Gijuj + Gik hi (k J(i) + , uk = 0),

j J(i) + J(i) Gijuj Gik hi (k J(i) , uk = 1).

Although the condition 3) seems to be diﬃcult to deal with, we show that the following dynamic programming approach can solve (27) in pseudo-polynomial time. We assume that 0 < |Gi1| |Gin| holds without loss of generality. For a vector u {0, 1}n, we say that u chooses an element j if either (uj = 1 and j J(i) + ) or (uj = 0 and j J(i) ) holds. Let k be the ﬁrst element that is not chosen by u. Then we can see that u is an extreme infeasible point of the ith constraint if and only if hi Gik+1 n j=1 Gijuj hi holds when k J(i) + , and hi + Gik + 1 n j=1 Gijuj hi holds when k J(i) . Therefore, in order to solve (27), it is enough to solve the following integer LP problem for each

Kimura & Makino

k = 1, . . . , n + 1.

maximize n j=1 yjuj subject to hi Gik + 1 n j=1 Gijuj hi (resp., hi + Gik + 1 n j=1 Gijuj hi) k is the ﬁrst unchosen element by u u {0, 1}n.

Here k = n + 1 means that u chooses all the elements. Let k {1, . . . , n}. For an integer ℓwith k ℓ n and an integer w Z, let v(ℓ, w) denote the objective value of

maximize ℓ j=1 yjuj subject to ℓ j=1 Gijuj = w k is the ﬁrst unchosen element by u u {0, 1}ℓ.

Let us consider the case in which k J(i) + , since the case of k J(i) can be treated similarly. Then we have

j J(i) + : j k 1 yj (w =

j J(i) + : j k 1 Gij),

(otherwise),

v(ℓ, w) = max{v(ℓ 1, w), v(ℓ 1, w Giℓ) + yℓ} (ℓ= k + 1, . . . , n).

Hence, we can see that maxhi Gik+1 w hi v(n, w) is the optimal value of (28). Since the dynamic programming algorithm requires O((n k)nηi) time for each k, where ηi = max{hi, |Gi1|, . . . , |Gin|}, we can solve the separation problem in O(n3mη) time, where η = maxi ηi. Hence, by Theorem 1, we can ﬁnd a nontrivial linear locally ﬁxable assignment for the 0-1 integer linear system (22) in pseudo-polynomial time. We next consider the unit integer linear system, i.e., the integer linear system such that the input matrix G is given by G {0, 1, +1}m n. Note that this includes global cardinality constraints (van Hoeve & Katriel, 2006) and is related to MAX(MIN) ONES (Creignou et al., 2001). Let

j J (1 xj) k (31)

be an inequality in the system. Then it has the unique prime CNF representing φ deﬁned by φ =

I+ J+,I J : |I+|+|I |=|J+|+|J | k+1

xj ) . (32)

Thus, we have the following lemma.

Lemma 2. Let φ be the unique prime CNF representing (31). Then we have

K (Mφ) = {y Rn : j I+ yj j I yj 0, I+ J+, I J , |I+| + |I | = |J+| + |J | k + 1}. (33)

Linear Satisfiability Preserving Assignments

Again the number of the constraints in the LP problems (25) might be exponential in the size of the input. Hence we again use the ellipsoid method to solve the LP problems (25).

Lemma 3. We can solve the separation problem for the LP problems (25) in polynomial time if G {0, 1, +1}m n.

Proof. Suppose that a vector y Rn is given. Then, we note that y K (Mφ1) K (Mφm) holds if and only if

min{ j I+ yj j I yj 0: I+ J(i) + , I J(i) ,

|I+| + |I | = |J(i) + | hi + 1} 0 (34)

holds for all i = 1, . . . , m. The left hand side of (34) can be computed simply by sorting the set {yj : j J(i) + } { yj : j J(i) } and summing the smallest |J(i) + | hi + 1 elements. Hence, we can solve the separation problem in O(mn log n) time.

We therefore proved Theorem 7.

4.2 The Case of General Integer Linear Systems

In this subsection, we consider linear satisﬁability preserving assignments for the non Boolean CSP given by integer linear systems. Let Gx h, x {0, 1, . . . , d}n (35)

denote an integer linear system such that the ith inequality is represented by

αijxj hi, (36)

for αij > 0 (j J(i) + J(i) ). Let Ui denote the set of the extreme infeasible points of (36), i.e., u Ui satisﬁes that u + ej is feasible to (36) if j J+ and uj = d, and u ej is feasible to (36) if j J and uj = 0. Recall the encoding that transform CSP instances with D = {0, 1, . . . , d} to Boolean CSP instances in Section 1. Deﬁne a CNF φi by

j J(i) + :uj =d

j J(i) :uj =0

We note that Gx h and x Dn if and only if all φi (i = 1, . . . , m) and xj,p xj,p+1 (j = 1, . . . , n; p = 1, . . . , d 1) are satisﬁed. Since xj,p xj,p+1 can be represented by a CNF

ψj,p = (xj,p xj,p+1),

by applying the ellipsoid method proposed in the previous subsection, we have the following result.

Kimura & Makino

Theorem 8. We can ﬁnd in pseudo-polynomial time a nontrivial linear locally ﬁxable assignment in m i=1 K (Mφi) j,p K (Mψj,p) for the general integer linear system (22), if it exists.

We then show that TVPI, Horn, and q-Horn systems are solvable in pseudo-polynomial time by repeatedly computing linear partial assignments in Theorem 8. A system Gx h is said to be TVPI if each row of G contains at most two nonzero elements, Horn if each row of G contains at most one positive element, and q-Horn if the optimal value of the following LP problem is at most one (Kimura & Makino, 2016).

minimize β subject to j:Gij>0 αj + j:Gij<0(1 αj) β (i = 1, . . . , m) 0 αj 1 (j = 1, . . . , n). (38)

Also, a CNF φ = m i=1 (

j J(i) + xj

j J(i) xj ) is called 2-CNF if |J(i) + J(i) | 2 holds

for all i = 1, . . . , m, Horn if |J(i) + | 1 holds for all i = 1, . . . , m, and q-Horn if the optimal value of the following LP problem is at most one (Boros et al., 1990).

minimize β subject to

j J(i) + αj +

j J(i) (1 αj) β (i = 1, . . . , m)

0 αj 1 (j = 1, . . . , n). (39)

We note that m i=1 φi j=1,...,n;p=1,...,d 1 ψj,p is Horn (resp., TVPI (i.e., a 2-CNF) and q-Horn) if so is the original integer linear system Gx h (Petke & Jeavons, 2011). It is known by Kullmann (2000) and van Maaren (2000) that 2-, Horn and q-Horn CNFs can be solved by repeatedly ﬁnding nontrivial unweighted linear autark assignments. Therefore, we have the following result.

Theorem 9. If an integer linear system is TVPI, Horn or q-Horn, then it can be solved in pseudo-polynomial time by repeatedly ﬁnding linear locally ﬁxable assignments in m i=1 K (Mφi) j,p K (Mψj,p).

Finally, we note that the following naive encoding does not work, since TVPI (resp., Horn and q-Horn) systems does not always transformed to the 0-1 TVPI (resp., Horn and q-Horn) systems.

G( d p=1 xp) h xj,p xj,p+1 (j = 1, . . . , n; p = 1, . . . , d 1) xp {0, 1}n (p = 1, . . . , d), (40)

where xp = (x1,p, . . . , xn,p) for p = 1, . . . , d.

Acknowledgments

The authors are indebted to the reviewers for their valuable comments and suggestions, which have considerably improved the presentation of the results. The authors also thank

Linear Satisfiability Preserving Assignments

Dr. Yasushi Kawase for fruitful discussion on Theorem 7. The ﬁrst 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.

Bar-Yehuda, R., & Rawitz, D. (2001). Eﬃcient algorithms for integer programs with two variables per constraint. Algorithmica, 29(4), 595 609.

Bordeaux, L., Cadoli, M., & Mancini, T. (2008). A unifying framework for structural properties of CSPs: Deﬁnitions, complexity, tractability. Journal of Artiﬁcial Intelligence Research, 32, 607 629.

Boros, E., Crama, Y., & Hammer, P. L. (1990). Polynomial-time inference of all valid implications for Horn and related formulae. Annals of Mathematics and Artiﬁcial Intelligence, 1, 21 32.

Brualdi, R. A., & Shader, B. L. (1995). Matrices of Sign-Solvable Linear Systems. Cambridge University Press, Cambridge.

Bulatov, A. A. (2006). A dichotomy theorem for constraint satisfaction problems on a 3-element set. Journal of the ACM, 53, 66 120.

Bulatov, A. A. (2017). A dichotomy theorem for nonuniform CSPs. In Proceedings of the 58th IEEE Annual Symposium on Foundations of Computer Science, pp. 319 330.

Chandru, V., & Hooker, J. (1999). Optimization Methods for Logical Inference. Wiley Interscience, New York, USA.

Cook, S. (1971). The complexity of theorem proving procedures. In Proceedings of the Third Annual ACM Symposium on Theory of Computing, pp. 151 158.

Crama, Y., Ekin, O., & Hammer, P. L. (1997). Variable and term removal from Boolean formulae. Discrete Applied Mathematics, 75, 217 230.

Crama, Y., & Hammer, P. L. (2011). Boolean Functions: Theory, Algorithms, and Applications. Cambridge University Press, New York, USA.

Creignou, N., Khanna, S., & Sudan, M. (2001). Complexity classiﬁcations of Boolean constraint satisfaction problems. Society for Industrial and Applied Mathematics, Pennsylvania, USA.

Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem-proving. Communications of the ACM, 5, 394 397.

Davis, M., & Putnam, H. (1960). A computing procedure for quantiﬁcation theory. Journal of the ACM, 7, 201 215.

Dechter, R. (2003). Constraint Processing. Morgan Kaufmann, California, USA.

Even, S., Itai, A., & Shamir, A. (1976). On the complexity of timetable and multicommodity ﬂow problems. SIAM Journal on Computing, 5(4), 691 703.

Kimura & Makino

Freuder, E. C. (1991). Eliminating interchangeable values in constraint satisfaction problems. In Proceedings of the 9th National Conference on Artiﬁcial Intelligence, pp. 227 233.

Garey, M. R., & Johnson, D. S. (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman and Company, USA.

Gaspers, S., & Szeider, S. (2012). Backdoors to satisfaction. In Bodlaender, H. L., Downey, R. G., Fomin, F. V., & Marx, D. (Eds.), The Multivariate Algorithmic Revolution and Beyond, pp. 287 317. Springer-Verlag, Heidelberg, Germany.

Glover, F. (1964). A bound escalation method for the solution of integer linear programs. Cahiers du Centre d Etudes de Recherche Operationelle, 6(3), 131 168.

Gr otschel, M., Lov asz, L., & Schrijver, A. (1993). Geometric Algorithms and Combinatorial Optimization Second Corrected Edition. Springer-Verlag, Heidelberg, Germany.

Henschen, L. J., & Wos, L. A. (1974). Unit refutations and Horn sets. Journal of the ACM, 21, 590 605.

Hochbaum, D. S., Megiddo, N., Naor, J., & Tamir, A. (1993). Tight bounds and 2approximation algorithms for integer programs with two variables per inequality. Mathematical Programming, 62, 69 83.

Hoﬀman, A. J., & Kruskal, J. B. (1956). Integral boundary points of convex polyhedra. In Khun, H., & Tucker, A. (Eds.), Linear Inequalities and Related Systems, pp. 223 246. Princeton University Press, London, UK.

Jeavons, P. G., Cohen, D. A., & Cooper, M. C. (1994). A substitution operation for constraints. In 2nd Workshop on Principles and Practice of Constraint Programming, pp. 1 9.

Jonsson, P., & Krokhin, A. (2004). Recognizing frozen variables in constraint satisfaction problems. Theoretical Computer Science, 329, 93 113.

Kimura, K., & Makino, K. (2016). Trichotomy for integer linear systems based on their sign patterns. Discrete Applied Mathematics, 200, 67 78.

Kleine B uning, H., & Kullmann, O. (2009). Minimal unsatisﬁability and autarkies. In Biere, A., Heule, M., van Maaren, H., & Walsh, T. (Eds.), Handbook of Satisﬁability, pp. 339 401. IOS Press, Amsterdam.

Kullmann, O. (2000). Investigations on autark assignments. Discrete Applied Mathematics, 107, 99 137.

Kullmann, O. (2003). Lean clause-sets: Generalizations of minimally unsatisﬁable clausesets. Discrete Applied Mathematics, 130, 209 249.

Kullmann, O. (2011). Constraint satisfaction problems in clausal form I: Autarkies and deﬁciency. Fundamenta Informaticae, 109, 27 81.

Lagarias, J. C. (1985). The computational complexity of simultaneous Diophantine approximation problems. SIAM Journal on Computing, 14(1), 196 209.

Lenstra, Jr., H. W. (1983). Integer programming with a ﬁxed number of variables. Mathematics of Operations Research, 8, 538 548.

Linear Satisfiability Preserving Assignments

Lewis, H. R. (1978). Renaming a set of clauses as a Horn set. Journal of the ACM, 25, 134 135.

Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B., & Troyansky, L. (1999). Determining computational complexity from characteristic phase transitions . Nature, 400, 133 137.

Monien, B., & Speckenmeyer, E. (1985). Solving satisfaiability in less than 2n steps. Discrete Applied Mathematics, 10, 287 295.

Papadimitriou, C. H. (1981). On the complexity of integer programming. Journal of the ACM, 28(4), 765 768.

Petke, J., & Jeavons, P. (2011). The order encoding: From tractable CSP to tractable SAT. In Proceedings of the 14th International Conference on Theory and Applications of Satisﬁability Testing, pp. 371 372.

Prestwich, S. (2004). Full dynamic substitutability by SAT encoding. In Principles and Practice of Constraint Programming, pp. 512 526.

Rockafellar, R. T. (1970). Convex Analysis. Princeton University Press, New Jersey, USA.

Rossi, F., van Beek, P., & Walsh, T. (Eds.). (2006). Handbook of Constraint Programming. Elsevier Science, New York, USA.

Schaefer, T. J. (1978). The complexity of satisﬁability problems. In Proceedings of the 10th annual ACM Symposium on Theory of Computing, pp. 216 226.

Tamura, N., Taga, A., Kitagawa, S., & Banbara, M. (2009). Compiling ﬁnite linear CSP into SAT. Constraints, 14, 254 272.

Tsang, E. (1993). Foundations of Constraint Satisfaction. Academic Pr, London and San Diego.

van Hoeve, W.-J., & Katriel, I. (2006). Global constraints. In Rossi, F., van Beek, P., & Walsh, T. (Eds.), Handbook of Constraint Programming, pp. 169 208. Elsevier, New York, USA.

van Maaren, H. (2000). A short note on some tractable cases of the satisﬁability problem. Information and Computation, 158, 125 130.

van Maaren, H., & Dang, C. (2002). Simplicial pivoting algorithms for a tractable class of integer programs. Journal of Combinatorial Optimization, 6(2), 133 142.

Williams, R., Gomes, C., & Selman, B. (2003). Backdoors to typical case complexity. In Proceedings of the 8th Internatinal Joint Conference on Artiﬁcial Intelligence, pp. 1173 1178.

Zhuk, D. (2017). A proof of CSP dichotomy conjecture. In Proceedings of the 58th IEEE Annual Symposium on Foundations of Computer Science, pp. 331 342.