Finding a satisfying assignment for a $k$-CNF formula $(k \geq 3)$, assuming such exists, is a notoriously hard problem. In this work we consider the uniform distribution over satisfiable $k$-CNF formulas with a linear number of clauses (clause-variable ratio greater than some constant). We rigorously analyze the structure of the space of satisfying assignments of a random formula in that distribution, showing that basically all satisfying assignments are clustered in one cluster, and agree on all but a small, though linear, number of variables. This observation enables us to describe a polynomial time algorithm that finds $\textit{whp}$ a satisfying assignment for such formulas, thus asserting that most satisfiable $k$-CNF formulas are easy (whenever the clause-variable ratio is greater than some constant). This should be contrasted with the setting of very sparse $k$-CNF formulas (which are satisfiable $\textit{whp}$), where experimental results show some regime of clause density to be difficult for many SAT heuristics. One explanation for this phenomena, backed up by partially non-rigorous analytical tools from statistical physics, is the complicated clustering of the solution space at that regime, unlike the more "regular" structure that denser formulas possess. Thus in some sense, our result rigorously supports this explanation.
Complete convergence of message passing algorithms for some satisfiability problems
7 Documents citing this article
Source : OpenCitations
Abbe, Emmanuel; Montanari, Andrea, 2013, Conditional Random Fields, Planted Constraint Satisfaction And Entropy Concentration, Approximation, Randomization, And Combinatorial Optimization. Algorithms And Techniques, pp. 332-346, 10.1007/978-3-642-40328-6_24.
Berthet, Quentin, 2015, Optimal Testing For Planted Satisfiability Problems, Electronic Journal Of Statistics, 9, 1, 10.1214/15-ejs1001.
Bulatov, Andrei A.; Wang, Cong, 2014, Approximating Highly Satisfiable Random 2-SAT, Theory And Applications Of Satisfiability Testing â SAT 2014, pp. 384-398, 10.1007/978-3-319-09284-3_28.
Coja-Oghlan, Amin; Krivelevich, Michael; Vilenchik, Dan, 2009, Why Almost All k-Colorable Graphs Are Easy To Color, Mathematical Systems Theory, 46, 3, pp. 523-565, 10.1007/s00224-009-9231-5.
Gao, Yong, 2009, Data Reductions, Fixed Parameter Tractability, And Random Weighted d-CNF Satisfiability, Artificial Intelligence, 173, 14, pp. 1343-1366, 10.1016/j.artint.2009.06.005.
Sheridan, Brendan; Sherr, Micah, 2016, On Manufacturing Resilient Opaque Constructs Against Static Analysis, Computer Security â ESORICS 2016, pp. 39-58, 10.1007/978-3-319-45741-3_3.
Vyas, Nikhil; Williams, Ryan, 2019, On Super Strong ETH, Theory And Applications Of Satisfiability Testing â SAT 2019, pp. 406-423, 10.1007/978-3-030-24258-9_28.