Average-Case Analysis of Random 3-SAT Instances with Backtrack Algorithms

Title: Average-Case Analysis of Random 3-SAT Instances with Backtrack Algorithms

Research Question: How does the complexity of solving random 3-SAT instances change as the ratio of clauses to variables increases?

Methodology: The authors use a backtrack algorithm, specifically the Davis-Putnam-Loveland-Logemann (DPLL) algorithm, to solve random 3-SAT instances. They analyze the average complexity of these instances by considering three regimes based on the ratio of clauses to variables: lower sat, upper sat, and unsat.

Results:

1. Lower Sat Phase: For small ratios of clauses to variables, the DPLL algorithm almost surely finds a solution in a time growing linearly with the number of variables. 2. Upper Sat Phase: For intermediate ratios, instances are almost surely satisfiable but finding a solution requires exponential time (∼2Nω) with high probability. 3. Unsat Phase: For large ratios, there is almost always no solution, and proofs of refutation are exponential.

Implications: The authors' analysis provides insights into the average complexity of solving random 3-SAT instances with backtrack algorithms. They identify three regimes based on the ratio of clauses to variables, each with different complexities. This work contributes to the understanding of the onset of complexity in random 3-SAT instances and the efficiency of backtrack algorithms.

Link to Article: https://arxiv.org/abs/0401011v1 Authors: arXiv ID: 0401011v1