Research Article: Phase transitions of the typical algorithmic complexity of the random satisfiability problem studied with linear programming

Date Published: April 19, 2019

Publisher: Public Library of Science

Author(s): Hendrik Schawe, Roman Bleim, Alexander K. Hartmann, Andrea Gambassi.


Here we study linear programming applied to the random K-SAT problem, a fundamental problem in computational complexity. The K-SAT problem is to decide whether a Boolean formula with N variables and structured as a conjunction of M clauses, each being a disjunction of K variables or their negations is satisfiable or not. The ensemble of random K-SAT attracted considerable interest from physicists because for a specific ratio αs = M/N it undergoes in the limit of large N a sharp phase transition from a satisfiable to an unsatisfiable phase. In this study we will concentrate on finding for linear programming algorithms “easy-hard” transitions between phases of different typical hardness of the problems on either side. Linear programming is widely applied to solve practical optimization problems, but has been only rarely considered in the physics community. This is a deficit, because those typically studied types of algorithms work in the space of feasible {0, 1}N configurations while linear programming operates outside the space of valid configurations hence gives a very different perspective on the typical-case hardness of a problem. Here, we demonstrate that the technique leads to one simple-to-understand transition for the well known 2-SAT problem. On the other hand we detect multiple transitions in 3-SAT and 4-SAT. We demonstrate that, in contrast to the previous work on vertex cover and therefore somewhat surprisingly, the hardness transitions are not driven by changes of any of various standard percolation or solution space properties of the problem instances. Thus, here a more complex yet undetected property must be related to the easy-hard transition.

Partial Text

The Satisfiability problem (SAT) [1] is to decide whether some Boolean formula is satisfiable or not, i.e., whether for a given Boolean formula, there is an assignment of the variables such that the formula evaluates to “true”. All Boolean formulas can be expressed in conjunctive normal form (CNF) which is a disjunction of clauses, each being a conjunction of variables or negated variables. Therefore K-SAT, which is a Boolean formula in CNF with K distinct variables per clause, is a commonly scrutinized version of the satisfiability problem.

We sample random 3-SAT instances, where each clause may contain any variable at most once. For up to 12 system sizes N ∈ [64, 131072] we simulated n = 5000 realizations for 30 to 100 different values of the density α. For comparison, we also performed simulations for 2-SAT and 4-SAT, with a smaller range of sizes. All error estimates are obtained by bootstrap resampling [33–35], except for errors of fit parameters shown in the plots, which are Gnuplot’s asymptotic standard errors corrected according to Ref. [34]. To solve the LP realizations, the implementation of the dual-simplex algorithms of the commercial optimization library CPLEX [36] is used. During the research additionally the primal- and dual-simplex implementations of Gurobi [37] and lp_solve [38] with multiple pricing strategies were used to ensure that the results are independent from the algorithm and the details of the implementation.

We study the solvability of random K-SAT realizations at different values of the clause-to-variable density α using linear programming. A realization is solved if the LP yields an integer solution. Since one can use LP algorithms that run in polynomial time even in the worst case, this means such a realization is “easy” in regard to this algorithm. Therefore it is sensible to assume that the structure of the typical instances changes at such a transition point, and this change is detected by the algorithm.