Skip to main content
SpringerLink
Log in

Inprocessing Rules

  • Conference paper
Automated Reasoning (IJCAR 2012)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 7364))

Included in the following conference series:

Abstract

Decision procedures for Boolean satisfiability (SAT), especially modern conflict-driven clause learning (CDCL) solvers, act routinely as core solving engines in various real-world applications. Preprocessing, i.e., applying formula rewriting/simplification rules to the input formula before the actual search for satisfiability, has become an essential part of the SAT solving tool chain. Further, some of the strongest SAT solvers today add more reasoning to search by interleaving formula simplification and CDCL search. Such inprocessing SAT solvers witness the fact that implementing additional deduction rules in CDCL solvers leverages the efficiency of state-of-the-art SAT solving further. In this paper we establish formal underpinnings of inprocessing SAT solving via an abstract inprocessing framework that covers a wide range of modern SAT solving techniques.

The 1st author is supported by Academy of Finland (grants 132812 and 251170), 2nd and 3rd authors by Austrian Science Foundation (FWF) NFN Grant S11408-N23 (RiSE).

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 39.99
Price excludes VAT (USA)
  • Available as 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Computers 48(5), 506–521 (1999)

    Article  MathSciNet  Google Scholar 

  2. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proc. DAC, pp. 530–535. ACM (2001)

    Google Scholar 

  3. Bacchus, F.: Enhancing Davis Putnam with extended binary clause reasoning. In: Proc. AAAI, pp. 613–619. AAAI Press (2002)

    Google Scholar 

  4. Bacchus, F., Winter, J.: Effective Preprocessing with Hyper-Resolution and Equality Reduction. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 341–355. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  5. Subbarayan, S., Pradhan, D.K.: NiVER: Non-increasing Variable Elimination Resolution for Preprocessing SAT Instances. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 276–291. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  6. Gershman, R., Strichman, O.: Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 423–429. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  8. Jin, H., Somenzi, F.: An incremental algorithm to check satisfiability for bounded model checking. Electronic Notes in Theoretical Computer Science 119(2), 51–65 (2005)

    Article  Google Scholar 

  9. Han, H., Somenzi, F.: Alembic: An efficient algorithm for CNF preprocessing. In: Proc. DAC, pp. 582–587. IEEE (2007)

    Google Scholar 

  10. Piette, C., Hamadi, Y., Saïs, L.: Vivifying propositional clausal formulae. In: Proc. ECAI, pp. 525–529. IOS Press (2008)

    Google Scholar 

  11. Heule, M.J.H., Järvisalo, M., Biere, A.: Clause Elimination Procedures for CNF Formulas. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 357–371. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  12. Järvisalo, M., Biere, A., Heule, M.J.H.: Simulating circuit-level simplifications on CNF. Journal of Automated Reasoning (2012); OnlineFirst 2011

    Google Scholar 

  13. Heule, M.J.H., Järvisalo, M., Biere, A.: Efficient CNF Simplification Based on Binary Implication Graphs. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 201–215. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  14. Heule, M.J.H., Järvisalo, M., Biere, A.: Covered clause elimination. In: LPAR-17 Short Papers (2010), http://arxiv.org/abs/1011.5202

  15. Biere, A.: P{re,i}coSAT@SC 2009. In: SAT 2009 Competitive Event Booklet (2009)

    Google Scholar 

  16. Soos, M.: CryptoMiniSat 2.5.0, SAT Race 2010 solver description (2010)

    Google Scholar 

  17. Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMV Technical Report 10/1, Johannes Kepler University, Linz, Austria (2010)

    Google Scholar 

  18. Järvisalo, M., Biere, A.: Reconstructing Solutions after Blocked Clause Elimination. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 340–345. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  19. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM 53(6), 937–977 (2006)

    Article  MathSciNet  Google Scholar 

  20. Nieuwenhuis, R., Oliveras, A.: On SAT Modulo Theories and Optimization Problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 156–169. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  21. Larrosa, J., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: A framework for certified boolean branch-and-bound optimization. Journal of Automated Reasoning 46(1) (2011)

    Google Scholar 

  22. Andersson, G., Bjesse, P., Cook, B., Hanna, Z.: A proof engine approach to solving combinational design automation problems. In: Proc. DAC, pp. 725–730. ACM (2002)

    Google Scholar 

  23. Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning 2, pp. 466–483. Springer (1983)

    Google Scholar 

  24. Li, C.M.: Integrating equivalency reasoning into Davis-Putnam procedure. In: Proc. AAAI, pp. 291–296. AAAI Press (2000)

    Google Scholar 

  25. Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. 22, 319–351 (2004)

    MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  27. Huang, J.: Extended clause learning. Artificial Intelligence 174(15), 1277–1284 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  28. Han, H., Somenzi, F.: On-the-Fly Clause Improvement. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 209–222. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  29. Hamadi, Y., Jabbour, S., Saïs, L.: Learning for dynamic subsumption. In: Proc. ICTAI, pp. 328–335. IEEE (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science & HIIT, University of Helsinki, Finland

    Matti Järvisalo

  2. Department of Software Technology, Delft University of Technology, The Netherlands

    Marijn J. H. Heule

  3. Institute for Formal Models and Verification, Johannes Kepler University, Linz, Austria

    Marijn J. H. Heule & Armin Biere

Authors
  1. Matti Järvisalo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marijn J. H. Heule
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Armin Biere
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Fakultät für Informatik, Technische Universität Wien, Favoritenstr. 9, E185/2, 1040, Wien, Austria

    Bernhard Gramlich

  2. École Polytechnique, INRIA Saclay and Laboratoire d’Informatique, Route de Saclay, 91128, Palaiseau Cedex, France

    Dale Miller

  3. School of Computer Science, University of Manchester, Oxford Road, M13 9PL, Manchester, UK

    Uli Sattler

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Järvisalo, M., Heule, M.J.H., Biere, A. (2012). Inprocessing Rules. In: Gramlich, B., Miller, D., Sattler, U. (eds) Automated Reasoning. IJCAR 2012. Lecture Notes in Computer Science(), vol 7364. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31365-3_28

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31365-3_28

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31364-6

  • Online ISBN: 978-3-642-31365-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation