Message-passing and local heuristics as decimation strategies for satisfiability

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Message-passing and local heuristics as decimation strategies for satisfiability

Full text

Pdf (655 KB)

Source

Symposium on Applied Computing archive
Proceedings of the 2009 ACM symposium on Applied Computing table of contents

Honolulu, Hawaii

SESSION: Constraint solving and programming track table of contents

Pages 1408-1414

Year of Publication: 2009

ISBN:978-1-60558-166-8

Authors

Lukas Kroc	Cornell University, Ithaca, NY
Ashish Sabharwal	Cornell University, Ithaca, NY
Bart Selman	Cornell University, Ithaca, NY

Sponsor

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 11, Downloads (12 Months): 31, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1529282.1529596 What is a DOI?

ABSTRACT

Decimation is a simple process for solving constraint satisfaction problems, by repeatedly fixing variable values and simplifying without reconsidering earlier decisions. We investigate different decimation strategies, contrasting those based on local, syntactic information from those based on message passing, such as statistical physics based Survey Propagation (SP) and the related and more well-known Belief Propagation (BP). Our results reveal that once we resolve convergence issues, BP itself can solve fairly hard random k-SAT formulas through decimation; the gap between BP and SP narrows down quickly as k increases. We also investigate observable differences between BP/SP and other common CSP heuristics as decimation proceeds, exploring the hardness of the decimated formulas and identifying a somewhat unexpected feature of message passing heuristics, namely, unlike other heuristics for satisfiability, they avoid unit propagation as variables are fixed.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	D. Achlioptas, A. Naor, and Y. Peres. Rigorous location of phase transitions in hard optimization problems. Nature, 435: 759--764, 2005.
	2	A. Braunstein and R. Zecchina. Survey propagation as local equilibrium equations. J. Stat. Mech., P06007, 2004. URL http://lanl.arXiv.org/cond-mat/0312483.
	3	Martin Davis , George Logemann , Donald Loveland, A machine program for theorem-proving, Communications of the ACM, v.5 n.7, p.394-397, July 1962 [doi>10.1145/368273.368557]
	4	Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
	5	N. Eén and N. Sörensson. MiniSat: A SAT solver with conflictclause minimization. In 8th SAT, St. Andrews, U.K., June 2005.
	6	M. Hajiaghayi and G. B. Sorkin. The satisability threshold of random 3-SAT is at least 3.52. Technical Report RC22942, IBM Research Report, 2003. http://arxiv.org/pdf/math.CO/0310193.
	7	E. I. Hsu and S. A. McIlraith. Characterizing propagation methods for boolean satisfiabilty. In 9th SAT, volume 4121 of LNCS, pages 325--338, Seattle, WA, Aug. 2006.
	8	Alexis C. Kaporis , Lefteris M. Kirousis , Efthimios G. Lalas, The probabilistic analysis of a greedy satisfiability algorithm, Random Structures & Algorithms, v.28 n.4, p.444-480, July 2006 [doi>10.1002/rsa.v28:4]
	9	L. Kroc, A. Sabharwal, and B. Selman. Survey propagation revisited. In 23rd UAI, pages 217--226, Vancouver, BC, July 2007.
	10	L. Kroc, A. Sabharwal, and B. Selman. Leveraging belief propagation, backtrack search, and statistics for model counting. In 5th CPAIOR, volume 5015 of LNCS, pages 127--141, Paris, France, May 2008.
	11	Elitza Maneva , Elchanan Mossel , Martin J. Wainwright, A new look at survey propagation and its generalizations, Journal of the ACM (JACM), v.54 n.4, p.17-es, July 2007 [doi>10.1145/1255443.1255445]
	12	Stephan Mertens , Marc Mézard , Riccardo Zecchina, Threshold values of random K-SAT from the cavity method, Random Structures & Algorithms, v.28 n.3, p.340-373, May 2006 [doi>10.1002/rsa.v28:3]
	13	M. Mézard, G. Parisi, and R. Zecchina. Analytic and algorithmic solution of random satisfiability problems. Science, 297(5582): 812--815, 2002.
	14	J. M. Mooij, B. Wemmenhove, H. J. Kappen, and T. Rizzo. Loop corrected belief propagation. In Proc. 11th Intl. Conf. on AI and Statistics (AISTATS-07), 2007.
	15	Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
	16	K. Murphy, Y. Weiss, and M. Jordan. Loopy belief propagation for approximate inference: An empirical study. In 15th UAI, pages 467--475, Sweden, July 1999.
	17	Judea Pearl, Probabilistic reasoning in intelligent systems: networks of plausible inference, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
	18	M. Pretti. A message-passing algorithm with damping. J. Stat. Mech., P11008, 2005.
	19	B. Selman, H. Kautz, and B. Cohen. Local search strategies for satisfiability testing. In D. S. Johnson and M. A. Trick, editors, Cliques, Coloring and Satisfiability: the Second DIMACS Implementation Challenge, volume 26 of DIMACS Series in DMTCS, pages 521--532. Amer. Math. Soc., 1996.
	20	J. S. Yedidia, W. T. Freeman, and Y. Weiss. Generalized belief propagation. In NIPS, pages 689--695, 2000.
	21	A. L. Yuille, CCCP algorithms to minimize the Bethe and Kikuchi free energies: convergent alternatives to belief propagation, Neural Computation, v.14 n.7, p.1691-1722, July 2002 [doi>10.1162/08997660260028674]