Skip to main content

Characterizing Propagation Methods for Boolean Satisfiability

  • Conference paper
Theory and Applications of Satisfiability Testing - SAT 2006 (SAT 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4121))

Abstract

Iterative algorithms such as Belief Propagation and Survey Propagation can handle some of the largest randomly-generated satisfiability problems (SAT) created to this point. But they can make inaccurate estimates or fail to converge on instances whose underlying constraint graphs contain small loops–a particularly strong concern with structured problems. More generally, their behavior is only well-understood in terms of statistical physics on a specific underlying model. Our alternative characterization of propagation algorithms presents them as value and variable ordering heuristics whose operation can be codified in terms of the Expectation Maximization (EM) method. Besides explaining failure to converge in the general case, understanding the equivalence between Propagation and EM yields new versions of such algorithms. When these are applied to SAT, such an understanding even yields a slight modification that guarantees convergence.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Braunstein, A., Mezard, M., Zecchina, R.: Survey propagation: An algorithm for satisfiability. Random Structures and Algorithms 27, 201–226 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  2. Kask, K., Dechter, R., Gogate, V.: Counting-based look-ahead schemes for constraint satisfaction. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, Springer, Heidelberg (2004)

    Google Scholar 

  3. Wang, Y., Zhang, J., Fossorier, M., Yedidia, J.: Reduced latency iterative decoding of LDPC codes. In: IEEE Conference on Global Telecommunications (GLOBECOM) (2005)

    Google Scholar 

  4. Braunstein, A., Zecchina, R.: Learning by message passing in networks of discrete synapses. Physics Review Letters 96(5) (2006)

    Google Scholar 

  5. Pearl, J.: Probabilistic Reasoning in Intelligent Systems. Morgan Kaufmann, San Mateo (1988)

    Google Scholar 

  6. Kschischang, F.R., Frey, B.J., Loeliger, H.A.: Factor graphs and the sum-product algorithm. IEEE Transactions on Information Theory 47(2) (2001)

    Google Scholar 

  7. Braunstein, A., Zecchina, R.: Survey propagation as local equilibrium equations. Journal of Statistical Mechanics: Theory and Experiments PO6007 (2004)

    Google Scholar 

  8. Yedidia, J., Freeman, W., Weiss, Y.: Understanding belief propagation and its generalizations. In: Nebel, B., Lakemeyer, G. (eds.) Exploring Artificial Intelligence in the New Millennium, pp. 239–256. Morgan Kaufmann, San Francisco (2003)

    Google Scholar 

  9. Dechter, R., Mateescu, R.: A simple insight into properties of iterative belief propagation. In: Proc. of 19th International Conference on Uncertainty in Artificial Intelligence (UAI 2003), Acapulco, Mexico (2003)

    Google Scholar 

  10. Lardeux, F., Saubion, F., Hao, J.K.: Three Truth Values for the SAT and MAX-SAT Problems. In: Proc. of the Nineteenth International Joint Conference on Artificial Intelligence (IJCAI 2005), Edinburgh, Scotland (2005)

    Google Scholar 

  11. Yedidia, J., Freeman, W., Weiss, Y.: Constructing free-energy approximations and generalized belief propagation algorithms. IEEE Transactions on Information Theory 51(7), 2282–2312 (2005)

    Article  MathSciNet  Google Scholar 

  12. Dechter, R., Kask, K., Mateescu, R.: Iterative join-graph propagation. In: Proc. of 18th International Conference on Uncertainty in Artificial Intelligence (UAI 2002), Edmonton, Canada, pp. 128–136 (2002)

    Google Scholar 

  13. Kask, K., Dechter, R., Larrosa, J., Pfeffer, A.: Cluster-tree decompostitions for reasoning in graphical models. Artificial Intelligence 166(1-2) (2005)

    Google Scholar 

  14. Selman, B., Kautz, H., Cohen, B.: Local search strategies for satisfiability testing. DIMACS Series in Discrete Mathematics and Theoretical Computer Science 26 (1996)

    Google Scholar 

  15. Goemans, M., Williamson, D.: New 3/4-approximation algorithms for the maximum satisfiability problem. SIAM Journal on Discrete Mathematics 7, 656–666 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  16. Goemans, M., Williamson, D.: Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming. Journal of the ACM (42), 1115–1145 (1995)

    Google Scholar 

  17. Williams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: Proc. of 18th International Joint Conference on Artificial Intelligence (IJCAI 2003), Acapulco, Mexico (2003)

    Google Scholar 

  18. Gomes, C., Selman, B., Crato, N., Kautz, H.: Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. Journal of Automated Reasoning 24(1-2), 67–100 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  19. Dempster, A., Laird, N., Rubin, D.: Maximum likelihood from incomplete data via the EM algorithm. Journal of the Royal Statistical Society 39(1), 1–39 (1977)

    MATH  MathSciNet  Google Scholar 

  20. Shang, Y., Wah, B.: A discrete Lagrangian-based global-search method for solving satisfiability problems. Journal of Global Optimization 12(1), 61–99 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  21. Neal, R., Hinton, G.: A view of the EM algorithm that justifies incremental, sparse, and other variants. In: Jordan, M. (ed.) Learning in Graphical Models, pp. 355–368. Kluwer Academic Publishers, Dordrecht (1998)

    Google Scholar 

  22. Jordan, M., Ghahramani, Z., Jaakkola, T., Saul, L.: An introduction to variational methods for graphical models. In: Jordan, M. (ed.) Learning in Graphical Models, MIT Press, Cambridge (1998)

    Google Scholar 

  23. Braunstein, A., Leone, M., Mezard, M., Weigt, M., Zecchina, R.: Sp-1.3 survey propagatrion implementation, http://www.ictp.trieste.it/~zecchina/SP/

  24. Hsu, E., McIlraith, S.: Characterizing loopy belief propagation as expectation maximization (2006), Manuscript in preparation

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hsu, E.I., McIlraith, S.A. (2006). Characterizing Propagation Methods for Boolean Satisfiability. In: Biere, A., Gomes, C.P. (eds) Theory and Applications of Satisfiability Testing - SAT 2006. SAT 2006. Lecture Notes in Computer Science, vol 4121. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11814948_31

Download citation

  • DOI: https://doi.org/10.1007/11814948_31

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-37206-6

  • Online ISBN: 978-3-540-37207-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics