Why almost all satisfiable $k$-CNF formulas are easy
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 rigorous...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Discrete Mathematics & Theoretical Computer Science
2007-01-01
|
| Series: | Discrete Mathematics & Theoretical Computer Science |
| Subjects: | |
| Online Access: | https://dmtcs.episciences.org/3538/pdf |
| _version_ | 1797270427513389056 |
|---|---|
| author | Amin Coja-Oghlan Michael Krivelevich Dan Vilenchik |
| author_facet | Amin Coja-Oghlan Michael Krivelevich Dan Vilenchik |
| author_sort | Amin Coja-Oghlan |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T02:04:06Z |
| format | Article |
| id | doaj.art-841e9774acef45c99216751bf95af9f7 |
| institution | Directory Open Access Journal |
| issn | 1365-8050 |
| language | English |
| last_indexed | 2024-04-25T02:04:06Z |
| publishDate | 2007-01-01 |
| publisher | Discrete Mathematics & Theoretical Computer Science |
| record_format | Article |
| series | Discrete Mathematics & Theoretical Computer Science |
| spelling | doaj.art-841e9774acef45c99216751bf95af9f72024-03-07T14:34:52ZengDiscrete Mathematics & Theoretical Computer ScienceDiscrete Mathematics & Theoretical Computer Science1365-80502007-01-01DMTCS Proceedings vol. AH,...Proceedings10.46298/dmtcs.35383538Why almost all satisfiable $k$-CNF formulas are easyAmin Coja-Oghlan0Michael Krivelevich1Dan Vilenchik2Department of Mathematical SciencesSchool of Mathematical Sciences [Tel Aviv]Blavatnik School of Computer Science [Tel Aviv]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.https://dmtcs.episciences.org/3538/pdfsatcomputational and structural complexityalgorithms and data structuresmessage passing algorithms[info.info-ds] computer science [cs]/data structures and algorithms [cs.ds][info.info-dm] computer science [cs]/discrete mathematics [cs.dm][math.math-co] mathematics [math]/combinatorics [math.co][info.info-cg] computer science [cs]/computational geometry [cs.cg] |
| spellingShingle | Amin Coja-Oghlan Michael Krivelevich Dan Vilenchik Why almost all satisfiable $k$-CNF formulas are easy Discrete Mathematics & Theoretical Computer Science sat computational and structural complexity algorithms and data structures message passing algorithms [info.info-ds] computer science [cs]/data structures and algorithms [cs.ds] [info.info-dm] computer science [cs]/discrete mathematics [cs.dm] [math.math-co] mathematics [math]/combinatorics [math.co] [info.info-cg] computer science [cs]/computational geometry [cs.cg] |
| title | Why almost all satisfiable $k$-CNF formulas are easy |
| title_full | Why almost all satisfiable $k$-CNF formulas are easy |
| title_fullStr | Why almost all satisfiable $k$-CNF formulas are easy |
| title_full_unstemmed | Why almost all satisfiable $k$-CNF formulas are easy |
| title_short | Why almost all satisfiable $k$-CNF formulas are easy |
| title_sort | why almost all satisfiable k cnf formulas are easy |
| topic | sat computational and structural complexity algorithms and data structures message passing algorithms [info.info-ds] computer science [cs]/data structures and algorithms [cs.ds] [info.info-dm] computer science [cs]/discrete mathematics [cs.dm] [math.math-co] mathematics [math]/combinatorics [math.co] [info.info-cg] computer science [cs]/computational geometry [cs.cg] |
| url | https://dmtcs.episciences.org/3538/pdf |
| work_keys_str_mv | AT amincojaoghlan whyalmostallsatisfiablekcnfformulasareeasy AT michaelkrivelevich whyalmostallsatisfiablekcnfformulasareeasy AT danvilenchik whyalmostallsatisfiablekcnfformulasareeasy |