Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Decomposing SAT Instances with Pseudo Backbones

  • Conference paper
  • First Online:
Evolutionary Computation in Combinatorial Optimization (EvoCOP 2017)

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

Abstract

Two major search paradigms have been proposed for SAT solving: Systematic Search (SS) and Stochastic Local Search (SLS). In SAT competitions, while SLS solvers are effective on uniform random instances, SS solvers dominate SLS solvers on application instances with internal structures. One important structural property is decomposability. SS solvers have long been exploited the decomposability of application instances with success. We conjecture that SLS solvers can be improved by exploiting decomposability of application instances, and propose the first step toward exploiting decomposability with SLS solvers using pseudo backbones. We then propose two SAT-specific optimizations that lead to better decomposition than on general pseudo Boolean optimization problems. Our empirical study suggests that pseudo backbones can vastly simplify SAT instances, which further results in decomposing the instances into thousands of connected components. This decomposition serves as a key stepping stone for applying the powerful recombination operator, partition crossover, to the SAT domain. Moreover, we establish a priori analysis for identifying problem instances with potential decomposability using visualization of MAXSAT instances and treewidth.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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 EPUB and 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

Similar content being viewed by others

Notes

  1. 1.

    http://www.satcompetition.org/2014/.

  2. 2.

    The original benchmark set in the industrial track contains 150 satisfiable instances, but openstacks-sequencedstrips-nonadl-nonnegated-os-sequencedstrips-p30_3.085-SAT.cnf and openstacks-p30_3.085-SAT.cnf are identical, despite their different names.

  3. 3.

    We use the Python package graph-tool (https://graph-tool.skewed.de/). Graph-tool is known for its efficiency on large graphs, due to its C++ core implementation.

References

  1. Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing, pp. 151–158. ACM (1971)

    Google Scholar 

  2. Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7–34 (2001)

    Article  MATH  Google Scholar 

  3. Velev, M.N., Bryant, R.E.: Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. J. Symb. Comput. 35(2), 73–106 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  4. Konev, B., Lisitsa, A.: Computer-aided proof of Erdős discrepancy properties. Artif. Intell. 224, 103–118 (2015)

    Article  MATH  Google Scholar 

  5. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24605-3_37

    Chapter  Google Scholar 

  6. Tompkins, D.A.D., Hoos, H.H.: UBCSAT: an implementation and experimentation environment for SLS algorithms for SAT and MAX-SAT. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 306–320. Springer, Heidelberg (2005). doi:10.1007/11527695_24

    Chapter  Google Scholar 

  7. The International SAT Competitions Webpage. http://www.satcompetition.org/

  8. Amir, E., McIlraith, S.: Partition-based logical reasoning for first-order and propositional theories. Artif. Intell. 162(1), 49–88 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  9. Prestwich, S.D.: CNF encodings. Handb. Satisfiability 185, 75–97 (2009)

    Google Scholar 

  10. Ansótegui, C., Giráldez-Cru, J., Levy, J., Simon, L.: Using community structure to detect relevant learnt clauses. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 238–254. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24318-4_18

    Chapter  Google Scholar 

  11. Bjesse, P., Kukula, J., Damiano, R., Stanion, T., Zhu, Y.: Guiding SAT diagnosis with tree decompositions. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 315–329. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24605-3_24

    Chapter  Google Scholar 

  12. Huang, J., Darwiche, A.: A structure-based variable ordering heuristic for SAT. In: IJCAI, vol. 3, pp. 1167–1172 (2003)

    Google Scholar 

  13. Monnet, A., Villemaire, R.: Scalable formula decomposition for propositional satisfiability. In: Proceedings of the Third C* Conference on Computer Science and Software Engineering, pp. 43–52. ACM (2010)

    Google Scholar 

  14. Whitley, D., Hains, D., Howe, A.: Tunneling between optima: partition crossover for the traveling salesman problem. In: Proceedings of the 11th Annual Conference on Genetic and Evolutionary Computation, pp. 915–922. ACM (2009)

    Google Scholar 

  15. Tinós, R., Whitley, D., Chicano, F.: Partition crossover for pseudo-boolean optimization. In: Proceedings of the 2015 ACM Conference on Foundations of Genetic Algorithms XIII, pp. 137–149. ACM (2015)

    Google Scholar 

  16. Ochoa, G., Chicano, F., Tinós, R., Whitley, D.: Tunnelling crossover networks. In: Proceedings of the 2015 Annual Conference on Genetic and Evolutionary Computation, GECCO 2015, pp. 449–456. ACM, New York (2015)

    Google Scholar 

  17. Lin, S.: Computer solutions of the traveling salesman problem. Bell Syst. Tech. J. 44(10), 2245–2269 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  18. Tinós, R., Whitley, D., Ochoa, G.: Generalized asymmetric partition crossover (GAPX) for the asymmetric TSP. In: Proceedings of the 2014 Annual Conference on Genetic and Evolutionary Computation, pp. 501–508. ACM (2014)

    Google Scholar 

  19. Kauffman, S., Levin, S.: Towards a general theory of adaptive walks on rugged landscapes. J. Theor. Biol. 128(1), 11–45 (1987)

    Article  MathSciNet  Google Scholar 

  20. Zhang, W.: Configuration landscape analysis and backbone guided local search: part i: satisfiability and maximum satisfiability. Artif. Intell. 158, 1–26 (2004)

    Article  MATH  Google Scholar 

  21. Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B., Troyansky, L.: Determining computational complexity from characteristic ‘phase transitions’. Nature 400(6740), 133–137 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  22. Aspvall, B., Plass, M.F., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Inf. Process. Lett. 8(3), 121–123 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  23. Robertson, N., Seymour, P.D.: Graph minors. II. Algorithmic aspects of tree-width. J. Algorithms 7(3), 309–322 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  24. Bodlaender, H.L.: Dynamic programming on graphs with bounded treewidth. In: Lepistö, T., Salomaa, A. (eds.) ICALP 1988. LNCS, vol. 317, pp. 105–118. Springer, Heidelberg (1988). doi:10.1007/3-540-19488-6_110

    Chapter  Google Scholar 

  25. Arnborg, S., Corneil, D.G., Proskurowski, A.: Complexity of finding embeddings in a k-tree. SIAM J. Algebraic Discret. Methods 8(2), 277–284 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  26. Bodlaender, H.L.: Discovering treewidth. In: Vojtáš, P., Bieliková, M., Charron-Bost, B., Sýkora, O. (eds.) SOFSEM 2005. LNCS, vol. 3381, pp. 1–16. Springer, Heidelberg (2005). doi:10.1007/978-3-540-30577-4_1

    Chapter  Google Scholar 

  27. Kroc, L., Sabharwal, A., Gomes, C.P., Selman, B.: Integrating systematic and local search paradigms: a new strategy for MaxSAT. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, pp. 544–551. Morgan Kaufmann Publishers Inc., San Francisco (2009)

    Google Scholar 

  28. Li, C.M., Wei, W., Zhang, H.: Combining adaptive noise and look-ahead in local search for SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 121–133. Springer, Heidelberg (2007). doi:10.1007/978-3-540-72788-0_15

    Chapter  Google Scholar 

  29. Gaspers, S., Szeider, S.: Strong backdoors to bounded treewidth SAT. In: 2013 IEEE 54th Annual Symposium on Foundations of Computer Science (FOCS), pp. 489–498. IEEE (2013)

    Google Scholar 

  30. Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005). doi:10.1007/11499107_5

    Chapter  Google Scholar 

  31. Sinz, C.: Visualizing SAT instances and runs of the DPLL algorithm. J. Autom. Reason. 39(2), 219–243 (2007)

    Article  MATH  Google Scholar 

  32. Fruchterman, T.M., Reingold, E.M.: Graph drawing by force-directed placement. Softw.: Pract. Exp. 21(11), 129–1164 (1991)

    Google Scholar 

  33. Frank, J.D., Cheeseman, P., Stutz, J.: When gravity fails: local search topology. J. Artif. Intell. Res. 7, 249–281 (1997)

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Colorado State University, Fort Collins, CO, 80523, USA

    Wenxiang Chen & Darrell Whitley

Authors
  1. Wenxiang Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Darrell Whitley
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wenxiang Chen .

Editor information

Editors and Affiliations

  1. Austrian Institute of Technology, Vienna, Austria

    Bin Hu

  2. University of Manchester, Manchester, United Kingdom

    Manuel López-Ibáñez

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Chen, W., Whitley, D. (2017). Decomposing SAT Instances with Pseudo Backbones. In: Hu, B., López-Ibáñez, M. (eds) Evolutionary Computation in Combinatorial Optimization. EvoCOP 2017. Lecture Notes in Computer Science(), vol 10197. Springer, Cham. https://doi.org/10.1007/978-3-319-55453-2_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-55453-2_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-55452-5

  • Online ISBN: 978-3-319-55453-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation