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

On Tackling the Limits of Resolution in SAT Solving

  • Conference paper
  • First Online:
Theory and Applications of Satisfiability Testing – SAT 2017 (SAT 2017)

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

Abstract

The practical success of Boolean Satisfiability (SAT) solvers stems from the CDCL (Conflict-Driven Clause Learning) approach to SAT solving. However, from a propositional proof complexity perspective, CDCL is no more powerful than the resolution proof system, for which many hard examples exist. This paper proposes a new problem transformation, which enables reducing the decision problem for formulas in conjunctive normal form (CNF) to the problem of solving maximum satisfiability over Horn formulas. Given the new transformation, the paper proves a polynomial bound on the number of MaxSAT resolution steps for pigeonhole formulas. This result is in clear contrast with earlier results on the length of proofs of MaxSAT resolution for pigeonhole formulas. The paper also establishes the same polynomial bound in the case of modern core-guided MaxSAT solvers. Experimental results, obtained on CNF formulas known to be hard for CDCL SAT solvers, show that these can be efficiently solved with modern MaxSAT solvers.

This work was supported by FCT funding of post-doctoral grants SFRH/BPD/103609/2014, SFRH/BPD/120315/2016, and LASIGE Research Unit, ref. UID/CEC/00408/2013.

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.

    An extended version of the paper containing additional detail and proofs can be found in [42].

  2. 2.

    Different implementations of the MSU3 have been proposed over the years [2, 50, 51, 55], which often integrate different improvements. A well-known implementation of MSU3 is OpenWBO [51], one of the best MaxSAT solvers in the MaxSAT Evaluations since 2014.

  3. 3.

    This section studies the original pairwise encoding of \({{\text {PHP}}}^{m+1}_m\). However, a similar argument can be applied to \({{\text {PHP}}}^{m+1}_m\) provided any encoding of AtMost1 constraints \({\mathcal {M}}_j\), as confirmed by the experimental results in Sect. 5.2.

  4. 4.

    Basic knowledge of core-guided MaxSAT algorithms is assumed. The reader is referred to recent surveys for more information [2, 55].

  5. 5.

    The notation \(\Phi \vdash _{{1}}\bot \) indicates that inconsistency (i.e. a falsified clause) is derived by unit propagation on the propositional encoding of \(\Phi \). This is the case with existing encodings of AtMost k constraints.

  6. 6.

    The discussion focuses on the results of the best performing representatives. Solvers that are missing in the discussion are meant to be “dominated” by their representatives.

  7. 7.

    http://www.maxsat.udl.cat.

  8. 8.

    The two tested versions of cc-opb behave almost identically with a minor advantage of linear search. As a result, cc-opb stands for the linear search version of the solver.

  9. 9.

    We chose LMHS (not MaxHS) because it has a command-line option to disable eq-seeding.

  10. 10.

    Note that all the shown cactus plots below scale the Y axis logarithmically.

References

  1. Abío, I., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: BDDs for pseudo-boolean constraints – revisited. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 61–75. Springer, Heidelberg (2011). doi:10.1007/978-3-642-21581-0_7

    Chapter  Google Scholar 

  2. Ansótegui, C., Bonet, M.L., Levy, J.: SAT-based MaxSAT algorithms. Artif. Intell. 196, 77–105 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  3. Ansótegui, C., Didier, F., Gabàs, J.: Exploiting the structure of unsatisfiable cores in MaxSAT. In: IJCAI, pp. 283–289 (2015)

    Google Scholar 

  4. Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality networks and their applications. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 167–180. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02777-2_18

    Chapter  Google Scholar 

  5. Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality networks: a theoretical and empirical study. Constraints 16(2), 195–221 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  6. Atserias, A., Kolaitis, P.G., Vardi, M.Y.: Constraint propagation as a proof system. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 77–91. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30201-8_9

    Chapter  Google Scholar 

  7. Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning SAT solvers. In: AAAI (2010)

    Google Scholar 

  8. Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309–317. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39071-5_23

    Chapter  Google Scholar 

  9. Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of boolean cardinality constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 108–122. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45193-8_8

    Chapter  Google Scholar 

  10. Bailleux, O., Boufkhad, Y., Roussel, O.: New encodings of pseudo-boolean constraints into CNF. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 181–194. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02777-2_19

    Chapter  Google Scholar 

  11. Beame, P., Pitassi, T.: Simplified and improved resolution lower bounds. In: FOCS, pp. 274–282 (1996)

    Google Scholar 

  12. Berre, D.L., Parrain, A.: The Sat4j library, release 2.2. JSAT 7(2–3), 59–64 (2010)

    Google Scholar 

  13. Biere, A.: Picosat essentials. JSAT 4(2–4), 75–97 (2008)

    MATH  Google Scholar 

  14. Biere, A.: Lingeling, plingeling and treengeling entering the SAT competition 2013. In: Balint, A., Belov, A., Heule, M., Järvisalo, M. (eds.) Proceedings of SAT Competition 2013, vol. B-2013-1, pp. 51–52. Department of Computer Science Series of Publications B, University of Helsinki (2013)

    Google Scholar 

  15. Biere, A.: Lingeling essentials, a tutorial on design and implementation aspects of the SAT solver lingeling. In: Pragmatics of SAT Workshop, p. 88 (2014)

    Google Scholar 

  16. Biere, A., Berre, D., Lonca, E., Manthey, N.: Detecting cardinality constraints in CNF. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 285–301. Springer, Cham (2014). doi:10.1007/978-3-319-09284-3_22

    Google Scholar 

  17. Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)

    MATH  Google Scholar 

  18. Bonet, M.L., Levy, J., Manyà, F.: Resolution for Max-SAT. Artif. Intell. 171(8–9), 606–618 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  19. Bryant, R.E., Beatty, D., Brace, K., Cho, K., Sheffler, T.: COSMOS: a compiled simulator for MOS circuits. In: DAC, pp. 9–16 (1987)

    Google Scholar 

  20. Buss, S.R.: Polynomial size proofs of the propositional pigeonhole principle. J. Symb. Log. 52(4), 916–927 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  21. Buss, S.R., Turán, G.: Resolution proofs of generalized pigeonhole principles. Theor. Comput. Sci. 62(3), 311–317 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  22. Chatalic, P., Simon, L.: Multiresolution for SAT checking. Int. J. Artif. Intell. Tools 10(4), 451–481 (2001)

    Article  Google Scholar 

  23. Chvátal, V., Szemerédi, E.: Many hard examples for resolution. J. ACM 35(4), 759–768 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  24. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  25. Codish, M., Zazon-Ivry, M.: Pairwise cardinality networks. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 154–172. Springer, Heidelberg (2010). doi:10.1007/978-3-642-17511-4_10

    Chapter  Google Scholar 

  26. Cook, S.A.: A short proof of the pigeon hole principle using extended resolution. ACM SIGACT News 8(4), 28–32 (1976)

    Article  Google Scholar 

  27. Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36–50 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  28. Cook, W.J., Coullard, C.R., Turán, G.: On the complexity of cutting-plane proofs. Discrete Appl. Math. 18(1), 25–38 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  29. Davies, J., Bacchus, F.: Solving MAXSAT by solving a sequence of simpler SAT instances. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 225–239. Springer, Heidelberg (2011). doi:10.1007/978-3-642-23786-7_19

    Chapter  Google Scholar 

  30. Davies, J., Bacchus, F.: Exploiting the power of mip solvers in maxsat. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 166–181. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39071-5_13

    Chapter  Google Scholar 

  31. Davies, J., Bacchus, F.: Postponing optimization to speed up MAXSAT solving. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 247–262. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40627-0_21

    Chapter  Google Scholar 

  32. Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Log. Program. 1(3), 267–284 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  33. 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 

  34. Eén, N., Sörensson, N.: Translating pseudo-Boolean constraints into SAT. JSAT 2(1–4), 1–26 (2006)

    MATH  Google Scholar 

  35. Jan Elffers’ personal webpage. http://www.csc.kth.se/~elffers

  36. Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252–265. Springer, Heidelberg (2006). doi:10.1007/11814948_25

    Chapter  Google Scholar 

  37. Goldberg, E.: Testing satisfiability of CNF formulas by computing a stable set of points. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 161–180. Springer, Heidelberg (2002). doi:10.1007/3-540-45620-1_15

    Chapter  Google Scholar 

  38. Goldberg, E.: Testing satisfiability of CNF formulas by computing a stable set of points. Ann. Math. Artif. Intell. 43(1), 65–89 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  39. Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39, 297–308 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  40. Huang, J.: Extended clause learning. Artif. Intell. 174(15), 1277–1284 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  41. IBM ILOG: CPLEX optimizer 12.7.0 (2016). http://www-01.ibm.com/software/commerce/optimization/cplex-optimizer

  42. Ignatiev, A. Morgado, A., Marques-Silva, J.: On tackling the limits of resolution in SAT solving. CoRR, abs/1705.01477 (2017). https://arxiv.org/abs/1705.01477

  43. Jabbour, S., Marques-Silva, J., Sais, L., Salhi, Y.: Enumerating prime implicants of propositional formulae in conjunctive normal form. In: Fermé, E., Leite, J. (eds.) JELIA 2014. LNCS (LNAI), vol. 8761, pp. 152–165. Springer, Cham (2014). doi:10.1007/978-3-319-11558-0_11

    Google Scholar 

  44. Jovanović, D., Moura, L.: Cutting to the chase solving linear integer arithmetic. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 338–353. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22438-6_26

    Chapter  Google Scholar 

  45. Jovanovic, D., de Moura, L.M.: Cutting to the chase - solving linear integer arithmetic. J. Autom. Reason. 51(1), 79–108 (2013)

    Article  MATH  Google Scholar 

  46. Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: a partial Max-SAT solver. JSAT 8(1/2), 95–100 (2012)

    MathSciNet  MATH  Google Scholar 

  47. Larrosa, J., Heras, F., de Givry, S.: A logical approach to efficient Max-SAT solving. Artif. Intell. 172(2–3), 204–233 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  48. Manquinho, V.M., Flores, P.F., Silva, J.P.M., Oliveira, A.L.: Prime implicant computation using satisfiability algorithms. In: ICTAI, pp. 232–239 (1997)

    Google Scholar 

  49. Marques-Silva, J., Ignatiev, A., Mencía, C., Peñaloza, R.: Efficient reasoning for inconsistent horn formulae. In: Michael, L., Kakas, A. (eds.) JELIA 2016. LNCS (LNAI), vol. 10021, pp. 336–352. Springer, Cham (2016). doi:10.1007/978-3-319-48758-8_22

    Chapter  Google Scholar 

  50. Marques-Silva, J., Planes, J.: On using unsatisfiability for solving maximum satisfiability. CoRR, abs/0712.1097 (2007). https://arxiv.org/abs/0712.1097

  51. Martins, R., Joshi, S., Manquinho, V., Lynce, I.: Incremental cardinality constraints for MaxSAT. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 531–548. Springer, Cham (2014). doi:10.1007/978-3-319-10428-7_39

    Google Scholar 

  52. Martins, R., Manquinho, V., Lynce, I.: Open-WBO: a modular MaxSAT solver. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 438–445. Springer, Cham (2014). doi:10.1007/978-3-319-09284-3_33

    Google Scholar 

  53. Minoux, M.: LTUR: a simplified linear-time unit resolution algorithm for Horn formulae and computer implementation. Inf. Process. Lett. 29(1), 1–12 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  54. Morgado, A., Dodaro, C., Marques-Silva, J.: Core-guided MaxSAT with soft cardinality constraints. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 564–573. Springer, Cham (2014). doi:10.1007/978-3-319-10428-7_41

    Google Scholar 

  55. Morgado, A., Heras, F., Liffiton, M.H., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints 18(4), 478–534 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  56. Morgado, A., Ignatiev, A., Marques-Silva, J.: MSCG: robust core-guided MaxSAT solving. JSAT 9, 129–134 (2015)

    MathSciNet  Google Scholar 

  57. Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSAT resolution. In: AAAI, pp. 2717–2723 (2014)

    Google Scholar 

  58. Nordström, J.: On the interplay between proof complexity and SAT solving. SIGLOG News 2(3), 19–44 (2015)

    Google Scholar 

  59. Ogawa, T., Liu, Y., Hasegawa, R., Koshimura, M., Fujita, H.: Modulo based CNF encoding of cardinality constraints and its application to MaxSAT solvers. In: ICTAI, pp. 9–17 (2013)

    Google Scholar 

  60. Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175(2), 512–525 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  61. Previti, A. Ignatiev, A. Morgado, A., Marques-Silva, J.: Prime compilation of non-clausal formulae. In: IJCAI, pp. 1980–1988 (2015)

    Google Scholar 

  62. Razborov, A.A.: Proof complexity of pigeonhole principles. In: Kuich, W., Rozenberg, G., Salomaa, A. (eds.) DLT 2001. LNCS, vol. 2295, pp. 100–116. Springer, Heidelberg (2002). doi:10.1007/3-540-46011-X_8

    Chapter  Google Scholar 

  63. Roorda, J.-W., Claessen, K.: A new SAT-based algorithm for symbolic trajectory evaluation. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 238–253. Springer, Heidelberg (2005). doi:10.1007/11560548_19

    Chapter  Google Scholar 

  64. Saikko, P., Berg, J., Järvisalo, M.: LMHS: a SAT-IP hybrid MaxSAT solver. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 539–546. Springer, Cham (2016). doi:10.1007/978-3-319-40970-2_34

    Google Scholar 

  65. Segerlind, N.: The complexity of propositional proofs. Bul. Symb. Logic 13(4), 417–481 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  66. Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827–831. Springer, Heidelberg (2005). doi:10.1007/11564751_73

    Chapter  Google Scholar 

  67. Soos, M.: Enhanced Gaussian elimination in DPLL-based SAT solvers. In: POS@SAT, pp. 2–14 (2010)

    Google Scholar 

  68. Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244–257. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02777-2_24

    Chapter  Google Scholar 

  69. Urquhart, A.: Hard examples for resolution. J. ACM 34(1), 209–219 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  70. Warners, J.P.: A linear-time transformation of linear inequalities into conjunctive normal form. Inf. Process. Lett. 68(2), 63–69 (1998)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LASIGE, Faculty of Science, University of Lisbon, Lisbon, Portugal

    Alexey Ignatiev, Antonio Morgado & Joao Marques-Silva

  2. ISDCT SB RAS, Irkutsk, Russia

    Alexey Ignatiev

Authors
  1. Alexey Ignatiev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Antonio Morgado
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Joao Marques-Silva
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexey Ignatiev .

Editor information

Editors and Affiliations

  1. UNSW Sydney, Sydney, New South Wales, Australia

    Serge Gaspers

  2. University of New South Wales , Sydney, New South Wales, Australia

    Toby Walsh

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Ignatiev, A., Morgado, A., Marques-Silva, J. (2017). On Tackling the Limits of Resolution in SAT Solving. In: Gaspers, S., Walsh, T. (eds) Theory and Applications of Satisfiability Testing – SAT 2017. SAT 2017. Lecture Notes in Computer Science(), vol 10491. Springer, Cham. https://doi.org/10.1007/978-3-319-66263-3_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66263-3_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66262-6

  • Online ISBN: 978-3-319-66263-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation