Skip to main content
SpringerLink
Log in

Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances

  • 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

Very large MaxSAT instances, comprising \(10^{20}\) clauses and beyond, commonly arise in a variety of domains. We present VOLT, a framework for solving such instances, using an iterative, lazy grounding approach. In each iteration, VOLT grounds a subset of clauses in the MaxSAT problem, and solves it using an off-the-shelf MaxSAT solver. VOLT provides a common ground to compare and contrast different lazy grounding approaches for solving large MaxSAT instances. We cast four diverse approaches from the literature on information retrieval and program analysis as instances of VOLT. We have implemented VOLT and evaluate its performance under different state-of-the-art MaxSAT solvers.

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. http://www.maxsat.udl.cat/14/index.html

  2. http://web.udl.es/usuaris/q4374304/

  3. Blackburn, S.M., Garner, R., Hoffman, C., Khan, A.M., McKinley, K.S., Bentzur, R., Diwan, A., Feinberg, D., Frampton, D., Guyer, S.Z., Hirzel, M., Hosking, A., Jump, M., Lee, H., Moss, J.E.B., Phansalkar, A., Stefanović, D., VanDrunen, T., von Dincklage, D., Wiedermann, B.: The DaCapo benchmarks: Java benchmarking development and analysis. In: OOPSLA (2006)

    Google Scholar 

  4. Chaganty, A., Lal, A., Nori, A.V., Rajamani, S.K.: Combining relational learning with SMT solvers using CEGAR. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 447–462. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  5. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. JACM 50(5) (2003)

    Google Scholar 

  6. Davies, J., Bacchus, F.: Postponing optimization to speed up MAXSAT solving. In: CP (2013)

    Google Scholar 

  7. Janota, M.: MiFuMax – a literate MaxSAT solver (2013)

    Google Scholar 

  8. Marques-Silva, J., Ignatiev, A., Morgado, A.: MSCG - Maximum Satisfiability: a Core-Guided approach (2014)

    Google Scholar 

  9. Kok, S., Sumner, M., Richardson, M., Singla, P., Poon, H., Lowd, D., Domingos, P.: The alchemy system for statistical relational AI. Tech. rep., Department of Computer Science and Engineering, University of Washington, Seattle, WA (2007). http://alchemy.cs.washington.edu

  10. Kügel, A.: Improved exact solver for the weighted MAX-SAT problem. In: POS 2010. Pragmatics of SAT (2010)

    Google Scholar 

  11. Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci. 21(3), 317–353 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  12. Luo, C., Cai, S., Wu, W., Jie, Z., Su, K.: CCLS: an efficient local search algorithm for weighted maximum satisfiability. IEEE Trans. Computers 64(7), 1830–1843 (2015)

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  14. Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSAT resolution. In: AAAI (2014)

    Google Scholar 

  15. Niu, F., Ré, C., Doan, A., Shavlik, J.W.: Tuffy: scaling up statistical inference in markov logic networks using an RDBMS. In: VLDB (2011)

    Google Scholar 

  16. Noessner, J., Niepert, M., Stuckenschmidt, H.: RockIt: Exploiting parallelism and symmetry for MAP inference in statistical relational models. In: AAAI (2013)

    Google Scholar 

  17. Riedel, S.: Improving the accuracy and efficiency of MAP inference for markov logic. In: UAI (2008)

    Google Scholar 

  18. Whaley, J., Lam, M.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In: PLDI (2004)

    Google Scholar 

  19. Zhang, X., Mangal, R., Grigore, R., Naik, M., Yang, H.: On abstraction refinement for program analyses in datalog. In: PLDI (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Georgia Institute of Technology, Atlanta, USA

    Ravi Mangal, Xin Zhang & Mayur Naik

  2. Microsoft Research, Bangalore, India

    Aditya V. Nori

Authors
  1. Ravi Mangal
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Xin Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Aditya V. Nori
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Mayur Naik
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ravi Mangal .

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

Mangal, R., Zhang, X., Nori, A.V., Naik, M. (2015). Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances. 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_22

Download citation

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

  • 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