Survey propagation: an algorithm for satisfiability

Abstract

We study the satisfiability of randomly generated formulas formed by $M$ clauses of exactly $K$ literals over $N$ Boolean variables. For a given value of $N$ the problem is known to be most difficult with $\alpha =M/N$ close to the experimental threshold ${\alpha }_c$ separating the region where almost all formulas are SAT from the region where all formulas are UNSAT. Recent results from a statistical physics analysis suggest that the difficulty is related to the existence of a clustering phenomenon of the solutions when $\alpha$ is close to (but smaller than) ${\alpha }_c$. We introduce a new type of message passing algorithm which allows to find efficiently a satisfiable assignment of the variables in the difficult region. This algorithm is iterative and composed of two main parts. The first is a message-passing procedure which generalizes the usual methods like Sum-Product or Belief Propagation: it passes messages that are surveys over clusters of the ordinary messages. The second part uses the detailed probabilistic information obtained from the surveys in order to fix variables and simplify the problem. Eventually, the simplified problem that remains is solved by a conventional heuristic.

19 pages, 6 figure

References in corpus (10)

• The Bethe lattice spin glass revisited
• The random K-satisfiability problem: from an analytic solution to an efficient algorithm
• Coloring random graphs
• Rigorous decimation-based construction of ground pure states for spin glass models on random lattices
• Typical random 3-SAT formulae and the satisfiability threshold
• Survey Propagation as local equilibrium equations
• A variational description of the ground state structure in random satisfiability problems
• A backtracking survey propagation algorithm for K-satisfiability
• Complexity transitions in global algorithms for sparse linear systems over finite fields
• On the survey-propagation equations for the random K-satisfiability problem

Cited by in corpus (32)

• Perturbation Biology: inferring signaling networks in cellular systems
• Survey Propagation as local equilibrium equations
• Efficient supervised learning in networks with binary synapses
• Focused Local Search for Random 3-Satisfiability
• A better algorithm for random k-SAT
• The asymptotic $k$-SAT threshold
• An event-based architecture for solving constraint satisfaction problems
• Local entropy as a measure for sampling solutions in Constraint Satisfaction Problems
• The backtracking survey propagation algorithm for solving random K-SAT problems
• Pairs of SAT Assignment in Random Boolean Formulae
• Networking - A Statistical Physics Perspective
• On the exactness of the cavity method for Weighted b-Matchings on Arbitrary Graphs and its Relation to Linear Programs
• Efficient Solution of Boolean Satisfiability Problems with Digital MemComputing
• Collaboration in Social Networks
• Aligning graphs and finding substructures by a cavity approach
• Relaxed Survey Propagation for The Weighted Maximum Satisfiability Problem
• Minimizing energy below the glass thresholds
• Join-Graph Propagation Algorithms
• The large deviations of the whitening process in random constraint satisfaction problems
• Exact Ramsey Theory: Green-Tao numbers and SAT
• Explaining Adaptation in Genetic Algorithms With Uniform Crossover: The Hyperclimbing Hypothesis
• Performance of the Survey Propagation-guided decimation algorithm for the random NAE-K-SAT problem
• Phase Transitions of the Typical Algorithmic Complexity of the Random Satisfiability Problem Studied with Linear Programming
• Statistical mechanics of budget-constrained auctions
• Survey propagation at finite temperature: application to a Sourlas code as a toy model
• Why adiabatic quantum annealing is unlikely to yield speed-up
• Coordination problems on networks revisited: statics and dynamics
• The Boolean SATisfiability Problem in Clifford algebra
• Processor Allocation for Optimistic Parallelization of Irregular Programs
• Learning Markov Random Fields for Combinatorial Structures via Sampling through Lovász Local Lemma
• Efficient message passing for cascade size distributions on finite trees
• Shared SAT Solvers and SAT Memory in Distributed Business Applications