Bose–Einstein condensation in satisfiability problems

This paper is concerned with the complex behavior arising in satisfiability problems. We present a new statistical physics-based characterization of the satisfiability problem. Specifically, we design an algorithm that is able to produce graphs starting from a k-SAT instance, in order to analyze them and show whether a Bose–Einstein condensation occurs. We observe that, analogously to complex networks, the networks of k-SAT instances follow Bose statistics and can undergo Bose–Einstein condensation. In particular, k-SAT instances move from a fit-get-rich network to a winner-takes-all network as the ratio of clauses to variables decreases, and the phase transition of k-SAT approximates the critical temperature for the Bose–Einstein condensation. Finally, we employ the fitness-based classification to enhance SAT solvers (e.g., ChainSAT) and obtain the consistently highest performing SAT solver for CNF formulas, and therefore a new class of efficient hardware and software verification tools.     

An Empirical Study of MAX-2-SAT Phase Transitions

The decision version of the maximum satisfiability problem (MAX-SAT) is stated as follows: Given a set S of propositional clauses and an integer g, decide if there exists a truth assignment that falsifies at most g clauses in S, where g is called the allowance for false clauses. We conduct an extensive experiment on over a million of random instances of 2-SAT and identify statistically the relationship between g, n (number of variables) and m (number of clauses). In our experiment, we apply an efficient decision procedure based on the branch-and-bound method. The statistical data of the experiment confirm not only the “scaling window” of MAX-2-SAT discovered by Chayes, Kim and Borgs, but also the recent results of Coppersmith et al. While there is no easy-hard-easy pattern for the complexity of 2-SAT at the phase transition, we show that there is such a pattern for the decision problem of MAX-2-SAT associated with the phase transition. We also identify that the hardest problems are among those with high allowance for false clauses but low number of clauses.     

The mathematics of playing golf, or: a new class of difficult non-linear mixed integer programs

We consider a class of non-linear mixed integer programs with n integer variables and k continuous variables. Solving instances from this class to optimality is an NP-hard problem. We show that for the cases with k=1 and k=2, every optimal solution is integral. In contrast to this, for every k≥3 there exist instances where every optimal solution takes non-integral values. Received: August 2001 / Accepted: January 2002?Published online March 27, 2002     

A simplified NP-complete satisfiability problem

3-SAT is NP-complete when restricted to instances where each variable appears in at most four clauses. When no variable appears in more than three clauses, 3-SAT is trivial and SAT is NP-complete. When no variable appears in more than two clauses, SAT may be solved in linear time.     

Finding Small Triangulations of Polytope Boundaries Is Hard

We prove that it is NP-hard to decide whether a polyhedral 3-ball can be triangulated with k simplices. The construction also implies that it is difficult to find the minimal triangulation of such a 3-ball. A lifting argument is used to transfer the result also to triangulations of boundaries of 4-polytopes. The proof is constructive and translates a variant of the 3-SAT problem into an instance of a concrete polyhedral 3-ball for which it is difficult to find a minimal triangulation. Received February 17, 1999, and in revised form October 20, 1999. Online publication May 16, 2000.     

Efficient branch-and-bound algorithms for weighted MAX-2-SAT

MAX-2-SAT is one of the representative combinatorial problems and is known to be NP-hard. Given a set of m clauses on n propositional variables, where each clause contains at most two literals and is weighted by a positive real, MAX-2-SAT asks to find a truth assignment that maximizes the total weight of satisfied clauses. In this paper, we propose branch-and-bound exact algorithms for MAX-2-SAT utilizing three kinds of lower bounds. All lower bounds are based on a directed graph that represents conflicts among clauses, and two of them use a set covering representation of MAX-2-SAT. Computational comparisons on benchmark instances disclose that these algorithms are highly effective in reducing the number of search tree nodes as well as the computation time.     

A General Upper Bound for the Satisfiability Threshold of Randomr-SAT Formulae

Experiments on solvingr-SAT random formulae have provided evidence of a satisfiability threshold phenomenon with respect to the ratio of the number of clauses to the number of variables of formulae. Presently, only the threshold of 2-SAT formulae has been proved to exist and has been computed to be equal to 1. For 3-SAT formulae and more generally forr-SAT formulae, lower and upper bounds of the threshold have been established. The best established bounds concern 3-SAT. For an observed threshold of about 4.25, the best lower bound is 3.003 and the best upper bound 4.76. In this paper we establish a general upper bound of the threshold forr-SAT formulae giving a value for 3-SAT of 4.64, significantly improving the previous best upper bound. For this we have defined a more restrictive structure than a satisfying truth assignment for characterizing the satisfiability of a SAT formula which we have called negatively prime solution (NPS). By merely applying the first moment method to negatively prime solutions of a randomr-SAT formula we obtain our bound.     

Analysis of Local Search Landscapes for <Emphasis Type="Italic">k</Emphasis>-SAT Instances

Stochastic local search is a successful technique in diverse areas of combinatorial optimisation and is predominantly applied to hard problems. When dealing with individual instances of hard problems, gathering information about specific properties of instances in a pre-processing phase is helpful for an appropriate parameter adjustment of local search-based procedures. In the present paper, we address parameter estimations in the context of landscapes induced by k-SAT instances: at first, we utilise a sampling method devised by Garnier and Kallel in 2002 for approximations of the number of local maxima in landscapes generated by individual k-SAT instances and a simple neighbourhood relation. The objective function is given by the number of satisfied clauses. The procedure provides good approximations of the actual number of local maxima, with a deviation typically around 10%. Secondly, we provide a method for obtaining upper bounds for the average number of local maxima in k-SAT instances. The method allows us to obtain the upper bound \(2^{n-O(\sqrt{n/k})}\) for the average number of local maxima, if m is in the region of 2 ^k · n/k.     

Testing satisfiability

Let Φ be a set of general boolean functions on n variables, such that each function depends on exactly k variables, and each variable can take a value from [1,d]. We say that Φ is ε-far from satisfiable, if one must remove at least εn^k functions in order to make the set of remaining functions satisfiable. Our main result is that if Φ is ε-far from satisfiable, then most of the induced sets of functions, on sets of variables of size c(k,d)/ε², are not satisfiable, where c(k,d) depends only on k and d. Using the above claim, we obtain similar results for k-SAT and k-NAEQ-SAT.Assume we relax the decision problem of whether an instance of one of the above mentioned problems is satisfiable or not, to the problem of deciding whether an instance is satisfiable or ε-far from satisfiable. While the above decision problems are NP-hard, our result implies that we can solve their relaxed versions, that is, distinguishing between satisfiable and ε-far from satisfiable instances, in randomized constant time.From the above result we obtain as a special case, previous results of Alon and Krivelevich, and of Czumaj and Sohler, concerning testing of graphs and hypergraphs colorability. We also discuss the difference between testing with one-sided and two-sided error.     

An efficient local search method for random 3-satisfiability

We report on some exceptionally good results in the solution of randomly generated 3-satisfiability instances using the “record-to-record travel (RRT)” local search method. When this simple, but less-studied algorithm is applied to random one-million variable instances from the problem's satisfiable phase, it seems to find satisfying truth assignments almost always in linear time, with the coefficient of linearity depending on the ratio α of clauses to variables in the generated instances. RRT has a parameter for tuning “greediness”. By lessening greediness, the linear time phase can be extended up to very close to the satisfiability threshold α_c. Such linear time complexity is typical for random-walk based local search methods for small values of α. Previously, however, it has been suspected that these methods necessarily lose their time linearity far below the satisfiability threshold. The only previously introduced algorithm reported to have nearly linear time complexity also close to the satisfiability threshold is the survey propagation (SP) algorithm. However, SP is not a local search method and is more complicated to implement than RRT. Comparative experiments with the WalkSAT local search algorithm show behavior somewhat similar to RRT, but with the linear time phase not extending quite as close to the satisfiability threshold.     

Satisfiability of mixed Horn formulas

In this paper the class of mixed Horn formulas is introduced that contain a Horn part and a 2-CNF (conjunctive normal form) (also called quadratic) part. We show that SAT remains NP-complete for such instances and also that any CNF formula can be encoded in terms of a mixed Horn formula in polynomial time. Further, we provide an exact deterministic algorithm showing that SAT for mixed Horn formulas containing n variables is solvable in time O(2^0.5284n). A strong argument showing that it is hard to improve a time bound of O(2^n/2) for mixed Horn formulas is provided. We also obtain a fixed-parameter tractability classification for SAT restricted to mixed Horn formulas C of at most k variables in its positive 2-CNF part providing the bound O(∥C∥2^0.5284k). We further show that the NP-hard optimization problem minimum weight SAT for mixed Horn formulas can be solved in time O(2^0.5284n) if non-negative weights are assigned to the variables. Motivating examples for mixed Horn formulas are level graph formulas [B. Randerath, E. Speckenmeyer, E. Boros, P. Hammer, A. Kogan, K. Makino, B. Simeone, O. Cepek, A satisfiability formulation of problems on level graphs, ENDM 9 (2001)] and graph colorability formulas.     

Disproof of the neighborhood conjecture with implications to SAT

We study a special class of binary trees. Our results have implications on Maker/Breaker games and SAT: We disprove a conjecture of Beck on positional games and construct an unsatisfiable k-CNF formula with few occurrences per variable, thereby improving a previous result by Hoory and Szeider and showing that the bound obtained from the Lovász Local Lemma is tight up to a constant factor. A (k, s)-CNF formula is a boolean formula in conjunctive normal form where every clause contains exactly k distinct literals and every variable occurs in at most s clauses. The (k, s)-SAT problem is the satisfiability problem restricted to (k, s)-CNF formulas. Kratochvíl, Savický and Tuza showed that for every k≥3 there is an integer f(k) such that every (k, f(k))-CNF formula is satisfiable, but (k, f(k) + 1)-SAT is already NP-complete (it is not known whether f(k) is computable). Kratochvíl, Savický and Tuza also gave the best known lower bound $f(k) = \Omega \left( {\tfrac{{2^k }} {k}} \right)$ , which is a consequence of the Lovász Local Lemma. We prove that, in fact, $f(k) = \Theta \left( {\tfrac{{2^k }} {k}} \right)$ , improving upon the best known upper bound $O\left( {(\log k) \cdot \tfrac{{2^k }} {k}} \right)$ by Hoory and Szeider. Finally we establish a connection between the class of trees we consider and a certain family of positional games. The Maker/Breaker game we study is as follows. Maker and Breaker take turns in choosing vertices from a given n-uniform hypergraph $\mathcal{F}$ , with Maker going first. Maker’s goal is to completely occupy a hyperedge and Breaker tries to prevent this. The maximum neighborhood size of a hypergraph $\mathcal{F}$ is the maximal s such that some hyperedge of $\mathcal{F}$ intersects exactly s other hyperedges. Beck conjectures that if the maximum neighborhood size of $\mathcal{F}$ is smaller than 2 ^n?1 ? 1 then Breaker has a winning strategy. We disprove this conjecture by establishing, for every n≥3, the existence of an n-uniform hypergraph with maximum neighborhood size 3·2 ^n?3 where Maker has a winning strategy. Moreover, we show how to construct, for every n, an n-uniform hypergraph with maximum degree at most $\frac{{2^{n + 2} }} {n}$ where Maker has a winning strategy. In addition we show that each n-uniform hypergraph with maximum degree at most $\frac{{2^{n - 2} }} {{en}}$ has a proper halving 2-coloring, which solves another open problem posed by Beck related to the Neighborhood Conjecture.     

An exact algorithm for the maximum k-club problem in an undirected graph

In this paper, we prove that the maximum k-club problem (MkCP) defined on an undirected graph is NP-hard. We also give an integer programming formulation for this problem as well as an exact branch-and-bound algorithm and computational results on instances involving up to 200 vertices. Instances defined on very dense graphs can be solved to optimality within insignificant computing times. When k=2, the most difficult cases appear to be those where the graph density is around 0.15.     

A Randomized Algorithm for 3-<Emphasis Type="Bold">SAT</Emphasis>

In this work we propose and analyze a simple randomized algorithm for 3-SAT (i.e. an algorithm to find a satisfiable assignment for a Boolean formula in conjunctive normal form (CNF) having at most 3 literals in every clause). Given a k-CNF formula \({\phi}\) on n variables, and \({\alpha \in \{0,1\}^n}\) that satisfies \({\phi}\), a clause of \({\phi}\) is critical if exactly one literal of that clause is satisfied under assignment α. Paturi et al. (Chicago J. Theor. Comput. Sci. 115, 1999) proposed a simple randomized algorithm (PPZ) for k-SAT for which success probability increases with the number of critical clauses (with respect to a fixed satisfiable solution of the input formula). Here, we first describe another simple randomized algorithm DEL which performs better if the number of critical clauses in input formula are less (with respect to a fixed satisfiable solution of the input formula). Subsequently, we combine these two simple algorithms such that the success probability of the combined algorithm is maximum of the success probabilities of PPZ and DEL on every input instance. We show that when the average number of clauses for a variable that appear as unique true literals in one or more critical clauses in \({\phi}\) is between 1 and 2/(3 · log (3/2)), combined algorithm performs better than the PPZ algorithm.     

SAT graph-based representation: A new perspective

In this paper a new graph based representation of Boolean formulas in conjunctive normal form (CNF) is proposed. It extends the well-known graph representation of binary CNF formulas (2-SAT) to the general case. Every clause is represented as a set of (conditional) implications and encoded with different edges labeled with a set of literals, called context. This representation admits many interesting features. For example, a path from the node labeled with a literal ¬x to the node labeled with a literal x gives us an original way to compute the condition under which the literal x is implied. Using this representation, we show that classical resolution can be reformulated as a transitive closure on the generated graph. Interestingly enough, using the SAT graph-based representation three original applications are then derived. The first one deals with the 2-SAT strong backdoor set computation problem, whereas in the second one the underlying representation is used to derive hard SAT instances with respect to the state-of-the-art satisfiability solvers. Finally, a new preprocessing technique of CNF formulas which extends the well-known hyper-resolution rule is proposed. Experimental results show interesting improvements on many classes of SAT instances taken from the last SAT competitions.     

The number of 2-sat functions

Our aim in this paper is to address the following question: of the 2^{2 n} Boolean functions onn variables, how many are expressible as 2-SAT formulae? In other words, we wish to count the number of different instances of 2-SAT, counting two instances as equivalent if they have the same set of satisfying assignments. Viewed geometrically, we are asking for the number of subsets of then-dimensional discrete cube that are unions of (n-2)-dimensional subcubes.There is a trivial upper bound of 2^4(n/2), the number of 2-SAT formulae. There is also an obvious lower bound of 2^(n/2), corresponding to the monotone 2-SAT formulae. Our main result is that, rather surprisingly, this lower bound gives the correct speed: the number of 2-SAT functions is 2^(1+0(1)) n ^{2 2}.     

Minimum decomposition of a digital surface into digital plane segments is NP-hard

This paper deals with the complexity of the decomposition of a digital surface into digital plane segments (DPSs for short). We prove that the decision problem (does there exist a decomposition with less than λ DPSs?) is NP-complete, and thus that the optimization problem (finding the minimum number of DPSs) is NP-hard. The proof is based on a polynomial reduction of any instance of the well-known 3-SAT problem to an instance of the digital surface decomposition problem. A geometric model for the 3-SAT problem is proposed.     

Tail bounds for occupancy and the satisfiability threshold conjecture

The classical occupancy problem is concerned with studying the number of empty bins resulting from a random allocation of m balls to n bins. We provide a series of tail bounds on the distribution of the number of empty bins. These tail bounds should find application in randomized algorithms and probabilistic analysis. Our motivating application is the following well-known conjecture on threshold phenomenon for the satisfiability problem. Consider random 3-SAT formulas with cn clauses over n variables, where each clause is chosen uniformly and independently from the space of all clauses of size 3. It has been conjectured that there is a sharp threshold for satisfiability at c* ≈? 4.2. We provide a strong upper bound on the value of c*, showing that for c > 4.758 a random 3-SAT formula is unsatisfiable with high probability. This result is based on a structural property, possibly of independent interest, whose proof needs several applications of the occupancy tail bounds.     

Estimating satisfiability

The problem of estimating the proportion of satisfiable instances of a given CSP (constraint satisfaction problem) can be tackled through weighting. It consists in putting onto each solution a non-negative real value based on its neighborhood in a way that the total weight is at least 1 for each satisfiable instance. We define in this paper a general weighting scheme for the estimation of satisfiability of general CSPs. First we give some sufficient conditions for a weighting system to be correct. Then we show that this scheme allows for an improvement on the upper bound on the existence of non-trivial cores in 3-SAT obtained by Maneva and Sinclair (2008) [17] to 4.419. Another more common way of estimating satisfiability is ordering. This consists in putting a total order on the domain, which induces an orientation between neighboring solutions in a way that prevents circuits from appearing, and then counting only minimal elements. We compare ordering and weighting under various conditions.