SpringerLink
Log in

Transforming Inconsistent Subformulas in MaxSAT Lower Bound Computation

  • Conference paper
Principles and Practice of Constraint Programming (CP 2008)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5202))

Abstract

We define a new heuristic that guides the application of cycle resolution (CR) in MaxSAT, and show that it produces better lower bounds than those obtained by applying CR exhaustively as in Max-DPLL, and by applying CR in a limited way when unit propagation detects a contradiction as in MaxSatz.

This research was funded by MEC research projects TIN2006-15662-C02-02, TIN2007-68005-C04-04, and CONSOLIDER CSD2007-0022, INGENIO 2010.

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
EUR 32.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
EUR 29.95
Price includes VAT (Spain)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 96.29
Price includes VAT (Spain)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

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.

Similar content being viewed by others

References

  1. Li, C.M., Manyà, F., Planes, J.: Exploiting unit propagation to compute lower bounds in branch and bound Max-SAT solvers. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 403–414. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  2. Li, C.M., Manyà, F., Planes, J.: Detecting disjoint inconsistent subformulas for computing lower bounds for Max-SAT. In: Proceedings AAAI 2006, pp. 86–91 (2006)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  4. Li, C.M., Manyà, F., Planes, J.: New inference rules for Max-SAT. Journal of Artificial Intelligence Research 30, 321–359 (2007)

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Hunan Normal University, Changsha, China

    Chu Min Li

  2. MIS, Université de Picardie Jules Verne, 5 Rue du Moulin Neuf, 80000, Amiens, France

    Chu Min Li & Nouredine Ould Mohamedou

  3. Artificial Intelligence Research Institue (IIIA, CSIC), Campus UAB, 08193, Bellaterra, Spain

    Felip Manyà

  4. Computer Science Department, Universitat de Lleida, Jaume II 69, 25001, Lleida, Spain

    Felip Manyà & Jordi Planes

Authors
  1. Chu Min Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Felip Manyà
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nouredine Ould Mohamedou
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jordi Planes
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Peter J. Stuckey

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Li, C.M., Manyà, F., Mohamedou, N.O., Planes, J. (2008). Transforming Inconsistent Subformulas in MaxSAT Lower Bound Computation. In: Stuckey, P.J. (eds) Principles and Practice of Constraint Programming. CP 2008. Lecture Notes in Computer Science, vol 5202. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85958-1_46

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-85958-1_46

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-85957-4

  • Online ISBN: 978-3-540-85958-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation