Approximation Hardness and Satisfiability of Bounded Occurrence Instances of SAT

Piotr Berman ^{∗} Marek Karpinski ^{†} Alex D. Scott ^{‡}

Abstract

We study approximation hardness and satisfiability of bounded occurrence uniform instances of SAT. Among other things, we prove the inapproximability for SAT instances in which every clause has exactly 3 literals and each variable occurs exactly 4 times, and display an explicit approximation lower bound for this problem. We also provide a tighter characterization of the uniformly bounded occurrence instances which are surely satisfiable.

1 Introduction

We define a k-SAT instance as a set of clauses that are disjunctions of exactly k literals. The decision problem asks for an assignment of truth values to the variables that satisfies all the clauses. The maximimization problem is to find a truth assignment that satisfies maximally many clauses. Cook [C71] has shown that k-SAT is NPcomplete for k ≥ 3, and Papadimitriou and Yannakakis have shown that k-SAT is MAX-SNP-complete for k ≥ 2.

In this paper we study uniform and regular instances of SAT. An instance of (k, s)- SAT is a formula in which every clause has length k, and each variable occurs exactly s times. Another (somewhat longer) notation used for that problem is EsOCC-EkSAT (cf. [K01], [BK03]).

In this paper we show that there exists a (3,4)-SAT formula with 15 variables and 20 clauses which is not satisfiable, and use this to prove that MAX-(3,4)-SAT is not approximable to within some constant factor. We provide also an explicit approximation lower bound for that problem (Theorem 1). The number 4 is easily seen to be the smallest number of occurrences for which the problem is hard to approximate (by a direct bipartite perfect matching argument). The best previous result in this direction was the result of Feige [F98] to the effect that (3,5)-SAT is hard to approximate to within a certain constant. We provide similar results for other cases as well, e.g. for (4,6)-SAT and (5,9)-SAT.

∗Dept. of Computer Science and Engineering, The Pennsylvania State University. Research done in part while visiting Dept. of Computer Science, University of Bonn. Work partially supported by NSF grant CCR-9700053, NIH grant 9R01HG02238-12 and DFG grant Bo 56/157-1. E-mail berman@cse.psu.edu.

†Dept. of Computer Science, University of Bonn. Research done in part while vising Princeton University, and IHÉS Institute, Bures-sur-Yvette. Work partially supported by DFG grants, Max-Planck Research Prize, DIMACS, and IST grant 14036 (RAND-APX). Research at the Max-Planck Institute for Mathematics was supported by the Special Program on Computational Complexity.

E-mail marek@cs.uni-bonn.de.

‡Dept. of Mathematics, University College London. E-mail scott@math.ucl.ac.uk

We have learned later that Tovey [T84] also displayed an unsatisfiable (3,4)-SAT formula and proved that the decision version of (3,4)-SAT is NP-complete. Further progress was obtained by Dubois [D90] who has shown that (4,6)- and (5,11)-SAT are NP-complete. In turn, Kratochvíl et. al. [KST93] defined f(k) as the largest s such that (k, s)-SAT has a satisfiable formula and have shown the following: (a) if s > f(k) then (k, s)-SAT is NP-complete, (b) f(k + 1) ≤ 2f(k) + 1 and (c) f(k) ≥ ⌊2^{k}/ek⌋.

In this paper we improve the results of Dubois [D90] and Kratochvíl et. al. [KST93] as follows. We show that if s > f(k) then (k, s)-SAT is MAX-SNP-complete. We also give improved bounds on f(k) for small values of k, for instance showing that f(5) < 9 (so that f(k) < 9 × 2^{k−5} for k > 4), and that f(6) ≥ 7.

2 Small Enforcers

We need to show how to force the Boolean value of a variable within the limitations of a (k, s)-SAT instance. This means providing a set of k-clauses that is satisfied if and only if x_{i} is true, and where x_{i} (x) occurs s − 1 times—so it can be used once more—and where auxiliary variables occur at most s times. To achieve regularity, we may have to add some arbitrary clauses for the auxiliary variables. Since these clauses are arbitrary, we will only provide their number, which may be a fraction, e.g. a fractional number 1/3 means that when forcing values of 3 variables we need to create one arbitrary clause. We represent a set of clauses as an array, where each row lists literals of one of the clauses. By aligning the occurences of a variables we make it easy to count.

If we want to use a proof of MAX-SNP-completeness to find an unattainable approximation ratio for a problem, it is important to have as small size of the instance translation as possible, and by extension, to minimize the size of all the gadgets that collectively form a solution. Converting an unsatisfiable clause set into an enforcer is in practice wastful, because our examples of small unsatisfiable set are composed from several enforcers.

If a clause was obtained as an implication from a set of clauses, we annotate each literal with a superscript in parenthesis that indicates the number of occurrences of each variable in this set. From this perspective, an enforcer for (k, s)-SAT has the form of x^{(i)} where i < s. If there exists such an enforcer, we can produce an unsatisfiable set as x_{1}^{(i)}, ..., x_{k}^{(i)} and ¬x_{1} ∨ ... ∨ ¬x_{k}. We represent a set of clauses as an array, where each row lists literals of one of the clauses. By aligning the occurences of variables we make it easy to count.

2.1 Enforcers in (3,4)-SAT

The enforcer given here is somewhat smaller than the one described by Tovey [T84]. It contains 19 clauses, rather than 22 in the construction of [T84].

We can force variable x to be true using the following six 3-clauses:

x^{(3)}  ≡  \begin{aligned}x & a & ¬b \\ & a & b & ¬c \\ & & b & c & ¬d \\ & & b & c & d \\ x & ¬a & & & ¬d \\ x & ¬a & & & d \end{aligned}

Because we need to add some arbitrary clause to have the fourth occurence of c, we altogether use 19/3 clauses to force x.

Three enforcers together with ¬x_{1} ∨¬x_{2} ∨¬x_{3} create a nonsatisfiable formula with 20 clauses and 15 variables.

To make our conventions more clear, we will prove that the forcing indeed occurs. Suppose that x is false and all 6 of the above clauses are true. Because we can delete x from these clauses, we know that ¬a ∨ ¬d and ¬a ∨ d, hence ¬a. Now we can delete a from the remaining clauses and the first clause yields ¬b. Now we can delete b and the second clause yields ¬c. Consequently, the third and fourth clauses yield ¬d and d, a contradiction.

2.2 Enforcers in (4,6)-SAT

To define a set of clauses that forces x withing the constraints of (4,6)-SAT we define the notion of supervised implication which in actuality is a set of six 4-clauses:

x^{(1)} → ( y^{(2)} → z^{(2)} )  ≡  \begin{aligned}¬x & ¬y & z & ¬a \\ & ¬y & z & a & ¬b \\ & & & a & b & c & d \\ & & & a & b & ¬c & d \\ & & & a & b & & ¬d & e \\ & & & a & b & c & ¬d & ¬e \end{aligned}

Note that if we have two supervised implications, the same variable can play the role of c in both, and a variable can play the role of d in one and the role of e in the other. As a result, only b’s have the deficit of occurences, and to remove this deficit we add one clause to every four supervised implications. Therefore one such implication requires 6.25 clauses.

Literal x forced to be true by 4-clauses:

x^{(5)}  ≡  \begin{aligned}¬x^{(1)} & → & ( a^{(2)} → b^{(2)} ) \\ ¬x^{(1)} & → & ( b^{(2)} → c^{(2)} ) \\ ¬x^{(1)} & → & ( c^{(2)} → a^{(2)} ) \\ ¬x & → & ( a ∨ b ∨ c ) \\ ¬x & → & ( ¬a ∨ ¬b ∨ ¬c ) \end{aligned}

One can see that we force x using 20.75 clauses.

2.3 Forcing a Variable in (5,9)-SAT

The set of clauses that forces a variable to be false withing the limitations of (5,9)-SAT has a complicated construction. We define the following auxiliary notion: ℱ(ix, jy) is a set of clauses in which x occurs i times, y occurs j times and which cannot be satisfied if both x and y are false, but which is otherwise satisfiable. Let f(ix, jy) = |ℱ(ix, jy)|. We will use a similar notion for a single variable (a contradiction if it is false) or for three variables (a contradiction if they are all false).

Our goal is to define ℱ(8x) and to find f(8x).

ℱ(8x) = {x ∨ ¬y_{0} ∨ ¬y_{1} ∨ ¬y_{2} ∨ ¬y_{3}} ∪ ℱ(8y_{0}, 1x) ∪ ⋃_{i=1}^{3} ℱ(8y_{i}, 2x).

Indeed, if x is false, then the only way to avoid contradiction is if y_{i} is false for some i = 0, 1, 2, 3, but then either both x and y_{0} are false, and we have a contradiction from ℱ(8y_{0}, 1x), or both x and y_{1} are false, and we have a contradiction from ℱ(8y_{1}, 2x) etc. Conversely, if y is true, both the initial clause and each of the 4 clause sets used in the definition is satisfiable.

We define ℱ(8x, 1z) as

ℱ(8x, 1z) = {x ∨ z ∨ ¬y_{0} ∨ ¬y_{1} ∨ ¬y_{2}} ∪ ℱ(8y_{0}, 2x) ∪ ℱ(8y_{1}, 2x) ∪ ℱ(8y_{2}, 3x).

We define ℱ(8x, 2z) as

ℱ(8x, 2z) = {x ∨ z ∨ ¬y_{0} ∨ ¬y_{1} ∨ ¬y_{2}} ∪ ℱ(8y_{0}, 3x) ∪ ℱ(8y_{1}, 3x) ∪ ℱ(8y_{2}, 1x, 1y).

We define ℱ(8x, 1a, 1b) as

ℱ(8x, 1a, 1b) = {x ∨ a ∨ b ∨ ¬y_{0} ∨ ¬y_{1}} ∪ ℱ(8y_{0}, 3x) ∪ ℱ(8y_{1}, 4x).

One can see that

\begin{matrix}f(8x) = 1 + f(8x, 1y) + 3f(8x, 2y) = 2 + 5f(8x, 2y) + f(8x, 3y) = \\ 7 + 11f(8x, 3y) + 5f(8x, 1y, 1z) = 12 + 16f(8x, 3y) + 5f(8x, 4y). \end{matrix}

To define ℱ(8x, 3y) we need to define three types of supervised implications, i.e. special sets of clauses. A supervised implication of type I can be viewed in two ways, and it is realized by nine 5-clauses:

\begin{aligned}w^{(1)} ∧ x^{(2)} & → & (z^{(3)} → y^{(2)} ) \\ w^{(1)} → ( z^{(3)} & → & (x^{(2)} → y^{(2)} )) \end{aligned} ≡ \begin{aligned}¬w & ¬x & y & ¬z & ¬a \\ & ¬x & y & ¬z & a & ¬b \\ & & & ¬z & a & b & ¬c & ¬d \\ & & & & a & b & ¬c & d & ¬e \\ & & & & a & b & c & ¬d & ¬e \\ & & & & a & b & c & d & ¬e \\ & & & & a & b & ¬c & d & e \\ & & & & a & b & c & ¬d & e \\ & & & & a & b & c & d & e \end{aligned}

A supervised implication of type II can be realized with two supervised implications of type I, and thus we use 18 5-clauses:

x^{(2)} → ( y^{(4)} → z^{(4)} )  ≡  \begin{aligned}x^{(1)} & → & ( z^{(3)} → (x^{(2)} → y^{(2)} ) \\ x^{(1)} & → & ( ¬z^{(3)} → (x^{(2)} → y^{(2)} ) \end{aligned}

Type III is realized with one type II and two type I and one normal clause, thus we use 37 5-clauses:

s^{(7)} ∧ t^{(3)} → u_{1}^{(7)} ∧ u_{2}^{(7)} ∧ u_{3}^{(7)} ≡ \begin{aligned}s^{(2)} & → & (u_{1}^{(4)} → u_{2}^{(4)} ) \\ s^{(2)} ∧ t^{(1)} & → & (u_{2}^{(2)} → u_{3}^{(3)} ) \\ s^{(2)} ∧ t^{(1)} & → & (u_{3}^{(3)} → u_{1}^{(2)} ) \\ s ∧ t & → & (u_{1} ∨ u_{2} ∨ u_{2}) \end{aligned}

Finally, ℱ(8x, 3y) is formed from two type III implications and three normal clauses, for the total of f(8x, 3y) = 77 5-clauses:

ℱ(8x, 3y) ≡ x^{(8)} ∧ y^{(3)} ≡ \begin{aligned}¬x^{(7)} ∧ ¬t^{(3)} & → & a_{1}^{(7)} ∧ a_{2}^{(7)} ∧ a_{3}^{(7)} \\ ¬x ∧ a_{1} ∧ a_{2} ∧ a_{3} & → & b \\ b ∧ a_{1} ∧ a_{2} ∧ a_{3} & → & c \\ c^{(7)} ∧ b^{(3)} & → & d_{1}^{(7)} ∧ d_{2}^{(7)} ∧ d_{3}^{(7)} \\ c ∧ b & → & ¬(d_{1} ∧ d_{2} ∧ d_{3}) \end{aligned}

One can use the above idea to get f(8x, 4y) = 39. This leads to f(8x) = 12 + 16 × 77 + 5 × 39 = 1439. We also need to add some extra clauses to increase the number of occurences of some auxiliary variables to 9.

3 NP-completeness

Suppose that we can force a variable to be true withing constraints of (k, s)-SAT, i.e. there exists a set ℱ(x) of clauses of length k in which each variable occurs at most s times, x occurs at most s − 1 times and such that all clauses in ℱ(x) can be satisified if and only if x is false. Then we can construct an unsatisfiable formula of (k, s)-SAT: start with a clause x_{1} ∨ … ∨ x_{k} and for each i = 1, …, k we add set of clauses ℱ(x_{i}); we need to take care that if i ≠ j then ℱ(x_{i}) and ℱ(9x_{j}) have no variables in common. If some of the variables occurs less than s times, we can add extra clauses.

We can use the same approach to translate 3-SAT into (k, s)-SAT. First, we reduce the number of occurences of each variables to 3. Then we replace a clause c with c ∨ x_{4} ∨ x_{k}, using different variables for every clause. Next, we add ℱ(x) for each new variable. Finally, we add extra clauses to assure that each variable occurs exactly s times. With little care, these extra clauses can be easy to satisfy.

We can conclude that if in (k, s)-SAT we can force a Boolean value of a variable, then (k, s)-SAT is NP-complete.

4 MAX-SNP Hardness

Given an instance of MAX-2-SAT, we can increase the length of clauses by inserting literals that are forced to be false. In this manner we can create a MAX-SAT instance with the same minimum number of unsatisfied clauses in which all clauses have a desired length. Towards the inapproximability result, we start from instances constructed in [BK03]. In that paper, in order to show the hardness of approximating MAX-2-SAT restricted to a certain class of instances, one have to construct the classes of clause sets with the following properties:

1. It is NP-hard to distinguish on whether the minimum number of unsatisfied clauses is at least (5 − ε)k or at most (4 + ε)k; 2. all variables occur the same number of times except for those that occur in 4k

copies of a gadget called replacements of equations of a single auxiliary variable (Fig. 6 in [BK03]), here we will call this gadget RESAV;

In Theorem 12 of [BK03] the size of these class sets is given as 256k for the case when each variable occurs at most 4 times, and RESAV contains one clase with only one literal and one variable with only 3 occurences. This proves the following lemma.

Lemma 1. There exists a family of sets of 2-clauses such that each, for some n, consists of 252n 2-clauses and 4n 1-clauses for which it is NP-hard to distinguish between the systems where (25n − ε)n clauses can be satisfied and systems where at most (251 + ε)n clauses can be satisfied (for ε < 1/2). Moreover, 4n variables in this system occur 3 times, while other variables have exactly 4 occurences.

We can transform a system from this theorem into an instance of Max-(3,4)- SAT in two stages. First, we increase the length of all clauses to 3 by inserting 260n variables that are forced to be false. Forcing them to be force requires (260 × 19/3 = 1646 + 2/3)n 3-clauses. Second, we need to increase the number of occurences of 4n variables using 4/3 n clauses. Thus we increased the number of clauses in the system from 256n to 1904n and we can conclude that

Theorem 1. There exists a family of instances of Max-(3,4)-SAT such that each, for some n, consists of 1904n clauses, for which it is NP-hard to distinguish between the systems where (1900 − ε)n clauses can be satisfied and systems where at most (1899 + ε)n clauses can be satisfied (for ε < 1/2).

This entails the following corollary.

Corollary 1. It is NP-hard to approximate MAX-(3,4)-SAT to within any factor below 1.00052.

Moreover, Theorem 12 of [BK03] shows that the size of the difficult clause sets for the case when each variable occurs at most 6 times is 168, and RESAV contains two variables with only 5 occurances. This shows the following.

Lemma 2. There exists a family of sets of 2-clauses such that each, for some n, consists of 168n 2-clauses for which it is NP-hard to distinguish between the systems where (164−ε)n clauses can be satisfied and systems where at most (163+ε)n clauses can be satisfied (for ε < 1/2). Moreover, 8n variables in this system occur 5 times, while other variables have exactly 6 occurences.

We can transform a system from this theorem into an instance of Max-(4,6)-SAT in two stages. First, we increase the length of all clauses to 4 by inserting 336n variables that are forced to be false. Forcing them to be false requires 336 × 20.75 = 6972 3-clauses. Second, we need to increase the number of occurences of 8n variables using 2n clauses. Thus we increased the number of clauses in the system from 168n to 7144n and we can conclude that

Theorem 2. There exists a family of instances of Max-(4,6)-SAT such that each, for some n, consists of 7144n clauses, for which it is NP-hard to distinguish between the systems where (7140 − ε)n clauses can be satisfied and systems where at most (7139 + ε)n clauses can be satisfied (for ε < 1/2).

In the same fashion we can show that Max-(5,9)-SAT is also MAX-SNP-hard, but the calculation of the provable inapproximability ratio is a bit difficult. A system of 2-clauses in which there is a difficult gap of almost n clauses would have about 100n clauses, and thus it would require an insertion of about 300n variables forced to be false—so we increase the clause length to 5. For each of the 300n variables we need roughly 1500 clauses that force it, and thus we get a system with ca. 400, 000n clauses. (It may be possible to decrease this estimate by a factor of 2.)

Note that if there exists an unsatisfiable formula of (k, s)-SAT, then there exists a system in which some variable x occurs less then s times and which can be satisfied if and only if x is false. Such a system can be used to define an Eq-reduction that transform (2, s)-SAT instances into instances of (k, s)-SAT, using the same approach as in the last two theorems. Therefore we can conclude that

Theorem 3. If s > f(k) then (k, s)-SAT is MAX-SNP-complete.

5 Satisfiability of Small Occurrence Instances

We now turn to lower bounds on f(k), the largest integer s such that every instance of (k, s)-SAT is satisfiable. Lower bounds on f(k) were given by Kratochvíl, Savický and Tuza [KST93], who used the Lovász Local Lemma to show that f(k) ≥ ⌊2^{k}/ek⌋; they also showed f(i) = i for i ≤ 3 and 4 ≤ f(4) ≤ 6.

The Lovász Local Lemma has also been used in the study of the related problem of hypergraph colouring; indeed this was one of its original applications (see [EL75], [AS00], [B01], [MR02]). A hypergraph H = (V, E) is 2-colourable if there is a partition V = V_{1} ∪V_{2} such that each edge contains vertices from both V_{1} and V_{2}. For k ≥ 2, let g(k) be the largest integer such that every k-uniform hypergraph in which every vertex is contained in at most g(k) edges is 2-colourable. It follows from a result of Seymour [S74] that g(k) ≥ k − 1 for every k, and after significant work it is now known when g(k) ≥ k: the Local Lemma shows g(k) ≥ k for k ≥ 9, Alon and Bregman [AB88] showed that g(k) ≥ k for k ≥ 8, and finally Thomassen [T92] showed g(k) ≥ k for k ≥ 4; while the Fano plane shows that g(3) < 3. More recently, McDiarmid [M97] showed that it is possible to improve on bounds for g(k) obtained from the Local Lemma by using the ‘lopsided’ version of the Local Lemma given by Erdős and Spencer [ES91]. In this section we use a similar approach to obtain bounds on f(k).

Let G be a graph with vertex set X, and let {A_{x}}_{x∈X} be a collection of events in some probability space. We say that G is a lopsidependency graph for {A_{x}}_{x∈X} if, for each x ∈ X, and each subset Y ⊂ X \ Γ^{∗}(x), we have

ℙ(A_{x}| ⋀_{y∈Y} \overline{A}_{y}\} ≤ ℙ(A_{x}).

Here we write Γ(x) for the set of neighbours of x and set Γ^{∗}(x) = {x} ∪ Γ(x). We can now state the Lopsided Local Lemma.

Theorem 4. [ES91] Suppose that G = (X, E) is a lopsidependency graph for a collection of events (A_{x})_{x∈X}. If there are real numbers (q_{x})_{x∈X} such that, for each x ∈ X,

ℙ(A_{x}) ≤ q_{x} ∏_{y∈Γ(x)}(1 − q_{y})

then ℙ(⋀_{x∈X} \overline{A}_{x}) > 0.

Some notation: for a clause C, we write C^{+} for the set of variables that occur in C without negation, and C^{−} for the set of variables that appear negated. We write V (C) = C + ∪C^{−} for the set of all variables that occur in C.

Theorem 5. Suppose d ≥ k ≥ 1 are positive integers and there is x ∈ (0, 1) such that

x^{1/k}((1 − x)^{⌊d/2⌋} + (1 − x)^{⌈d/2⌉}) > 1.  (1)

Then every instance of (k, d)-SAT has a satisfying assignment.

Proof. Let 𝒞 be the set of clauses in an instance of (k, d)-SAT, and let X be the set of variables occurring in clauses from 𝒞. We define a graph G with vertex set 𝒞 and an edge between clauses C and C′ if and only if there is a variable x that occurs negated in one clause and without negation in the other. Given a sequence (p_{i})_{i∈X} of reals p_{i} ∈ [0, 1], we generate a random assigment for X by setting each variable i ∈ X true independently with probability p_{i} and false otherwise. Note that then

ℙ(C not satisfied) = ∏_{i∈C^{−}} p_{i} ∏_{∈C^{+}}(1 − p_{i}).

For C ∈ 𝒞, let A_{C} be the event that C is not satisfied. We first show that G is a lopsidependency graph for the events (A_{C})_{C∈𝒞}. Indeed, let C be a clause in 𝒞 and let {C_{j} : j ∈ J} be a set of clauses that does not contain C or any of its neighbours. Let B be the event that C_{j} is satisfied for every j ∈ J. Let X_{0} be the set of variables that occur both in C and in some C_{j}: changing the sign of all occurrences of some of these variables if necessary, we may assume that all variables in X_{0} occur without negation in C. By the definition of G, it follows that these variables do not occur negated in any of the C_{j}. Thus \overline{A}_{C} and B are both increasing in the variables in X_{0}. Since A and B are independent if we condition on the assignment restricted to X_{0}, it follows from the FKG inequality [FKG71], or the inequality of Harris [H60], that \overline{A} and B are positively correlated, and hence A and B are negatively correlated, which is the condition required for a lopsidependency graph.

Let x ∈ (0, 1) satisfy (1). We will choose probabilities (p_{i})_{i∈X} so that, for every clause C,

∏_{i∈C^{−}} p_{i} ∏_{i∈C^{+}}(1 − p_{i}) < x(1 − x)^{d(C)},

where d(C) is the degree of C in G. Now it follows from (1) that, for 0 ≤ i ≤ k, we have

x^{1/k}((1 − x)^{i} + (1 − x)^{d−i}) > 1

(note that (1 − x)^{i} + (1 − x)^{d−i} is minimized for integers in this range when i = ⌈d/2⌉ or ⌊d/2⌋). Thus we can choose numbers η_{0}, …, η_{d} ∈ (0, 1) such that, for 0 ≤ i ≤ d,

η_{i} < x^{1/k}(1 − x)^{d−i}

and

η_{i} + η_{d−i} = 1.

For each i ∈ X, let pos(i) be the number of positive occurrences of i in clauses of 𝒞. We define p_{i} = η_{pos(i)}.

For a clause C and a variable a ∈ V (C), we define d_{C}(a) as follows: if a occurs without negation in C then d_{C}(a) is the number of negated occurrences of a in clauses of 𝒞; if ¬a occurs in C then d_{C}(a) is the number of non-negated occurrences of a in clauses of 𝒞. Since C is adjacent to a clause C′ exactly when there is a variable that occurs negated in one clause and without negation in the other, we have d(C) ≤ ∑_{a∈V (C)} d_{C}(a). Now if a is not negated in C then p_{a} = η_{d−d_{C}(a)}, while if a is negated then p_{a} = η_{d_{C}(a)}. So

ℙ(C unsatisfied) = ∏_{i∈C^{−}} p_{i} ∏_{i∈C^{+}}(1 − p_{i}) = ∏_{i∈C^{−}} η_{d−d_{C}(a)} ∏_{i∈C^{+}}(1 − η_{d_{C}(a)})
= ∏_{i∈V (C)} η_{d−d_{C}(a)} < ∏_{i∈V (C)} x^{1/k}(1 − x)^{d_{C}(a)}
≤ x(1 − x)^{d(C)}.

It therefore follows from Theorem 4 that, with positive probability, all clauses of 𝒞 are satisfied and, in particular, it follows that 𝒞 is satisfiable.

We can now prove our lower bounds on f(k).

Corollary 2. All instances of (6, 7)-SAT, (7, 13)-SAT, (8, 23)-SAT and (9, 41)-SAT are satisfiable.

Proof. Apply Theorem 5 with x = 1/21, x = 1/47, x = 1/100 and x = 1/200 respectively.

Dubois [D90] showed that if every instance of (r, s)-SAT is satisfiable then every instance of (r + 1, s + ⌊s/r⌋)-SAT is satisfiable. Corollary 2 therefore implies the following.

Corollary 3. Every instance of (k, k + 1)-SAT is satisfiable for k ≥ 6.

We remark that Theorem 5 is not enough to show that every instance of (5, 6)- SAT is satisfiable. Indeed, considering an instance in which each variable occurs three times without negation and three times with negation, we see that we would need some x ∈ (0, 1) such that 2x^{1/5}(1 − x)^{3} > 1, but the left hand side has maximum less than 0.95. However, we conjecture the following.

Conjecture 1. Every instance of (5, 6)-SAT is satisfiable.

Theorem 5 also gives an asymptotic lower bound on f(k) that is slightly better than that of Kratochvíl, Savický and Tuza [KST93]. However, it should be possible to obtain better bounds by employing techniques from hypergraph colouring (see, for instance, Radhakrishnan and Srinivasan [RS00]).

Finally, we remark that the arguments above show only the existence of a solution for instances of (r, s)-SAT with s ≤ f(r). Beck [B91] gave an algorithmic version of the local lemma, which provides that a randomized algorithm finding a satisfying assignment with a large probability, but his proof requires a much smaller value of s. For fixed r, and s ≤ f(r), is there a polynomial-time algorithm that finds a satisfying assignment for all instances of (r, s)-SAT?

Acknowledgments.

We thank Johan Håstad for drawing our attention to the problem of approximating (3,4)-SAT and Jörg Rothe for informing us about previous results on that problem.

References

[AS00] N. Alon and J. Spencer, The Probabilistic Method, 2nd ed. (Wiley, New York, 2000)

[AB88] N. Alon and Z. Bregman, Every 8-uniform 8-regular hypergraph is 2colourable, Graphs Combin. 4:303–305, 1988

[A95] S. Arora, C. Lund, Hardness of Approximations, in Approximation Algorithms, D. S. Hochbaum (ed.), PWS Publishing, Boston 1995, 399-446 [B91] J. Beck, An algorithmic approach to the Lovász local lemma I, in Random

Structures and Algorithms 2:343-365, 1991

[BK03] P. Berman and M. Karpinski, Improved Approximation Lower Bounds on Small Occurrence Optimization, Elec. Coll. on Comp. Compl., Report 8 (2003)

[B01] B. Bollobás, Random graphs, Second edition, Cambridge Studies in Advanced Mathematics 73, Cambridge University Press, Cambridge, 2001, xviii+498 pp.

[C71] S.C. Cook, The complexity of theorem-proving procedures, Proc. 3rd ACM STOC, 151-158, 1971

[D90] O. Dubois, On the r,s-SAT satisfiability problem and a conjecture of Tovey, Discrete Applied Math. 26:51-60, 1990

[EL75] P. Erdős and L. Lovász, Problems and results on 3-chromatic hypergraphs and some related questions, Infinite and finite sets, Vol. II, Colloq. Math. Soc. Janos Bolyai, Vol. 10, North-Holland, Amsterdam, 1975, pp. 609–627

[ES91] P. Erdős and J. Spencer, Lopsided Lovász local lemma and latin transversals, Discrete Applied Math. 30:151–154, 1991

[F98] U. Feige, A threshold of ln n for approximating set cover, Journal of ACM, 45(4):634–652, July 1998

[FKG71] C.M. Fortuin, P.W. Kasteleyn and J. Ginibre, Correlation inequalities on some partially ordered sets, Communications in Mathematical Physics 22:89– 103, 1971

[H97] J. Håstad, Some optimal inapproximability results, Proc. 29th ACM STOC, 1-10, 1997

[H00] J. Håstad, On bounded occurrence constraint satisfaction, Information Processing Letters 74:1-6, 2000

[H60] T.E. Harris, A lower bound for the critical probability in a certain percolation process, Proceedings of the Cambridge Philosophical Society 56:13–20, 1960

[K01] M. Karpinski, Approximating bounded degree instances of NP-hard problems, Proc. 13th Symp. on Fundamentals of Computation Theory, LNCS 2138, Springer, 2001, 24-34

[KST93] J. Kratochvíl, P. Savický and Z. Tuza, One more occurence of variable makes satisfiability jump from trivial to NP-complete, SIAM J. Comput. 8:203-210, 1993

[M97] C. McDiarmid, Hypergraph colouring and the Lovász Local Lemma, Discrete Math. 167/168:481–486, 1997 [MR02] M. Molloy and B. Reed, Graph colouring and the probabilistic method, Al-

gorithms and Combinatorics 23, Springer-Verlag, Berlin, 2002, xiv+326 pp

[PY91] C. Papadimitriou and M. Yannakakis, Optimization, approximation and complexity classes, JCSS 43:425-440, 1991

[P94] C. Papadimitriou, Computational Complexity, Addison-Wesley, New York, 1994, 315-319

[RS00] J. Radhakrishnan and A. Srinivasan, Improved bounds and algorithms for hypergraph 2-colouring, Rand. Structures and Algorithms 16:4–32, 2000

[S74] P.D. Seymour, On the two colouring of hypergraphs, Quart. J. Math. Oxford Series 3 25:303–312, 1974

[T92] C. Thomassen, The even cycle problem for directed graphs, J. Amer. Math. Soc. 5:217–229, 1992

[T84] C.A. Tovey, A simplified satisfiability problem, Discrete Applied Math. 8:85-89, 1984.

[T01] L. Trevisan, Non-approximability results for optimization problems on bounded degree instances, Proc. 33rd ACM STOC, 2001