Theory and Applications of Satisfiability Testing

DOI10.1007/11527695zbMATH Open1122.68605arXivcond-mat/0408190OpenAlexW2483910514MaRDI QIDQ5714751FDOQ5714751

Bart Selman, Cristopher Moore, Haixia Jia

Publication date: 16 December 2005

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: We introduce a highly structured family of hard satisfiable 3-SAT formulas corresponding to an ordered spin-glass model from statistical physics. This model has provably "glassy" behavior; that is, it has many local optima with large energy barriers between them, so that local search algorithms get stuck and have difficulty finding the true ground state, i.e., the unique satisfying assignment. We test the hardness of our formulas with two Davis-Putnam solvers, Satz and zChaff, the recently introduced Survey Propagation (SP), and two local search algorithms, Walksat and Record-to-Record Travel (RRT). We compare our formulas to random 3-XOR-SAT formulas and to two other generators of hard satisfiable instances, the minimum disagreement parity formulas of Crawford et al., and Hirsch's hgen. For the complete solvers the running time of our formulas grows exponentially in sqrt(n), and exceeds that of random 3-XOR-SAT formulas for small problem sizes. SP is unable to solve our formulas with as few as 25 variables. For Walksat, our formulas appear to be harder than any other known generator of satisfiable instances. Finally, our formulas can be solved efficiently by RRT but only if the parameter d is tuned to the height of the barriers between local minima, and we use this parameter to measure the barrier heights in random 3-XOR-SAT formulas as well.

Full work available at URL: https://arxiv.org/abs/cond-mat/0408190

Recommendations

• scientific article; zbMATH DE number 1113991
• An efficient local search method for random 3-satisfiability
• Survey propagation: An algorithm for satisfiability
• Generating hard satisfiability problems
• SAT local search algorithms: Worst-case study

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cited In (5)

• Generating hard satisfiable instances by planting into random constraint satisfaction problem model with growing constraint scope length
• \(\boldsymbol{borealis}\) -- a generalized global update algorithm for Boolean optimization problems
• A physical model for the satisfiability problem
• Random constraint satisfaction: easy generation of hard (satisfiable) instances
• The solution space structure of planted constraint satisfaction problems with growing domains

Uses Software

• Walksat
• hgen2
• zChaff

This page was built for publication: Theory and Applications of Satisfiability Testing

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5714751)