Skip to main content
SpringerLink
Log in

Exploiting Resolution-Based Representations for MaxSAT Solving

  • Conference paper
  • First Online:
Theory and Applications of Satisfiability Testing -- SAT 2015 (SAT 2015)

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

Abstract

Most recent MaxSAT algorithms rely on a succession of calls to a SAT solver in order to find an optimal solution. In particular, several algorithms take advantage of the ability of SAT solvers to identify unsatisfiable subformulas. Usually, these MaxSAT algorithms perform better when small unsatisfiable subformulas are found in early iterations of the algorithm. However, this is not the case in many problem instances, since the whole formula is given to the SAT solver in each call.

In this paper, we propose to partition the MaxSAT formula using a resolution-based graph representation. Partitions are then iteratively joined by using a proximity measure extracted from the graph representation of the formula. The algorithm ends when only one partition remains and the optimal solution is found. Experimental results show that this new approach further enhances a state of the art MaxSAT solver to optimally solve a larger set of industrial problem instances.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.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. Ansótegui, C., Giráldez-Cru, J., Levy, J.: The Community structure of SAT formulas. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 410–423. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  2. Asín, R., Nieuwenhuis, R.: Curriculum-based course timetabling with SAT and MaxSAT. Annals of Operations Research 218(1), 71–91 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. Blondel, V., Guillaume, J., Lambiotte, R., Lefebvre, E.: Fast unfolding of communities in large networks. Journal of Statistical Mechanics 2008(10), P10008 (2008)

    Article  Google Scholar 

  5. Brandes, U., Delling, D., Gaertler, M., Goerke, R., Hoefer, M., Nikoloski, Z., Wagner, D.: Maximizing modularity is hard (2006). arXiv: physics/0608255

  6. 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)

    Chapter  Google Scholar 

  7. Girvan, M., Newman, M.E.J.: Community structure in social and biological networks. Proceedings of the National Academy of Sciences 99(12), 7821–7826 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  8. Heras, F., Morgado, A., Marques-Silva, J.: Core-guided binary search algorithms for maximum satisfiability. In: AAAI Conference on Artificial Intelligence. AAAI Press (2011)

    Google Scholar 

  9. Ignatiev, A., Morgado, A., Manquinho, V., Lynce, I., Marques-Silva, J.: Progression in maximum satisfiability. In: European Conference on Artificial Intelligence, pp. 453–458. IOS Press (2014)

    Google Scholar 

  10. Janota, M., Lynce, I., Manquinho, V., Marques-Silva, J.: PackUp: Tools for Package Upgradability Solving. Journal on Satisfiability, Boolean Modeling and Computation 8(1/2), 89–94 (2012)

    MathSciNet  MATH  Google Scholar 

  11. Järvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129–144. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  12. Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: Programming Language Design and Implementation, pp. 437–446. ACM (2011)

    Google Scholar 

  13. Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: A Partial Max-SAT Solver. Journal on Satisfiability, Boolean Modeling and Computation 8(1/2), 95–100 (2012)

    MathSciNet  MATH  Google Scholar 

  14. Kullmann, O.: On a generalization of extended resolution. Discrete Applied Mathematics 96–97, 149–176 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  15. Le Berre, D., Rapicault, P.: Dependency management for the eclipse ecosystem: an update. In: International Workshop on Logic and Search

    Google Scholar 

  16. Marques-Silva, J., Planes, J.: On Using Unsatisfiability for Solving Maximum Satisfiability (2007). CoRR

    Google Scholar 

  17. 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, Heidelberg (2014)

    Google Scholar 

  18. Martins, R., Manquinho, V., Lynce, I.: Open-WBO: a modular MaxSAT solver\(^\text{, }\). In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 438–445. Springer, Heidelberg (2014)

    Google Scholar 

  19. Martins, R., Manquinho, V., Lynce, I.: Community-based partitioning for MaxSAT solving. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 182–191. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  20. Morgado, A., Heras, F., Liffiton, M., 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 

  21. Morgado, A., Heras, F., Marques-Silva, J.: Improvements to core-guided binary search for MaxSAT. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 284–297. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  22. Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSAT resolution. In: AAAI Conference on Artificial Intelligence, pp. 2717–2723. AAAI Press (2014)

    Google Scholar 

  23. Newman, M.E.J., Girvan, M.: Finding and evaluating community structure in networks. Physical Review E 69(026113) (2004)

    Google Scholar 

  24. Safarpour, S., Mangassarian, H., Veneris, A.G., Liffiton, M.H., Sakallah, K.A.: Improved design debugging using maximum satisfiability. In: Formal Methods in Computer-Aided Design, pp. 13–19. IEEE Computer Society (2007)

    Google Scholar 

  25. Van Gelder, A.: Variable independence and resolution paths for quantified boolean formulas. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 789–803. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  26. Yates, R.A., Raphael, B., Hart, T.P.: Resolution graphs. Artificial Intelligence 1(4), 257–289 (1970)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INESC-ID / Instituto Superior Técnico, Universidade de Lisboa, Lisbon, Portugal

    Miguel Neves, Mikoláš Janota, Inês Lynce & Vasco Manquinho

  2. University of Texas at Austin, Austin, USA

    Ruben Martins

  3. Department of Computer Science, University of Oxford, Oxford, UK

    Ruben Martins

Authors
  1. Miguel Neves
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ruben Martins
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mikoláš Janota
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Inês Lynce
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Vasco Manquinho
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ruben Martins .

Editor information

Editors and Affiliations

  1. Algorithms, University of Texas, Austin, Texas, USA

    Marijn Heule

  2. Trusted Systems Research Group, Fort Meade, Texas, USA

    Sean Weaver

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Neves, M., Martins, R., Janota, M., Lynce, I., Manquinho, V. (2015). Exploiting Resolution-Based Representations for MaxSAT Solving. In: Heule, M., Weaver, S. (eds) Theory and Applications of Satisfiability Testing -- SAT 2015. SAT 2015. Lecture Notes in Computer Science(), vol 9340. Springer, Cham. https://doi.org/10.1007/978-3-319-24318-4_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-24318-4_20

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-24317-7

  • Online ISBN: 978-3-319-24318-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation