Skip to main content
SpringerLink
Log in

SAT Modulo Graphs: Acyclicity

  • Conference paper
Logics in Artificial Intelligence (JELIA 2014)

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

Included in the following conference series:

Abstract

Acyclicity is a recurring property of solutions to many important combinatorial problems. In this work we study embeddings of specialized acyclicity constraints in the satisfiability problem of the classical propositional logic (SAT). We propose an embedding of directed graphs in SAT, with arcs labelled with propositional variables, and an extended SAT problem in which all clauses have to be satisfied and the subgraph consisting of arcs labelled true is acyclic. We devise a constraint propagator for the acyclicity constraint and show how it can be incorporated in off-the-shelf SAT solvers. We show that all existing encodings of acyclicity constraints in SAT are either prohibitively large or do not sanction all inferences made by the constraint propagator. Our experiments demonstrate the advantages of our solver over other approaches for handling acyclicity.

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. Audemard, G., Bertoli, P.G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: A SAT based approach for solving formulas over Boolean and linear mathematical propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 195–210. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  2. Corander, J., Janhunen, T., Rintanen, J., Nyman, H., Pensar, J.: Learning chordal Markov networks by constraint satisfaction. In: Burges, C.J.C., Bottou, L., Welling, M., Ghahramani, Z., Weinberger, K. (eds.) Advances in Neural Information Processing Systems 26, pp. 1349–1357 (2014)

    Google Scholar 

  3. Cotton, S., Maler, O.: Fast and flexible difference constraint propagation for DPLL(T). In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 170–183. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  4. Cussens, J.: Bayesian network learning by compiling to weighted MAX-SAT. In: Proceedings of the Conference on Uncertainty in Artificial Intelligence, pp. 105–112. AUAI Press (2008)

    Google Scholar 

  5. Denecker, M., Ternovska, E.: A logic of nonmonotone inductive definitions. ACM Transactions on Computational Logic 9(2), 14:1–14:52 (2008)

    Google Scholar 

  6. Dooms, G., Deville, Y., Dupont, P.E.: Cp(graph): Introducing a graph computation domain in constraint programming. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 211–225. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  7. Dooms, G., Katriel, I.: The minimum spanning tree constraint. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 152–166. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  8. Gebser, M., Janhunen, T., Rintanen, J.: Answer set programming as SAT modulo acyclicity. In: Proceedings of the 21st European Conference on Artificial Intelligence, ECAI 2014. IOS Press (2014)

    Google Scholar 

  9. Heljanko, K., Keinänen, M., Lange, M., Niemelä, I.: Solving parity games by a reduction to SAT. Journal for Computer and System Sciences 78(2), 430–440 (2012)

    Article  MATH  Google Scholar 

  10. Hoffmann, H.F., van Beek, P.: A global acyclicity constraint for Bayesian network structure learning (September 2013) (unpublished manuscript in the Doctoral Program of the International Conference on Principles and Practice of Constraint Programming)

    Google Scholar 

  11. Janhunen, T.: Evaluating the effect of semi-normality on the expressiveness of defaults. Artificial Intelligence 144(1-2), 233–250 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  12. Janhunen, T.: Some (in)translatability results for normal logic programs and propositional theories. Journal of Applied Non-Classical Logics 16(1-2), 35–86 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  13. Kautz, H., Selman, B.: Pushing the envelope: planning, propositional logic, and stochastic search. In: Proceedings of the 13th National Conference on Artificial Intelligence and the 8th Innovative Applications of Artificial Intelligence Conference, pp. 1194–1201. AAAI Press (1996)

    Google Scholar 

  14. Lin, F., Zhao, Y.: ASSAT: Computing answer sets of a logic program by SAT solvers. Artificial Intelligence Journal 157(1), 115–137 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  15. Mahfoudh, M., Niebert, P., Asarin, E., Maler, O.: A satisfiability checker for difference logic. In: Proceedings of SAT 2002 – Theory and Applications of Satisfiability Testing, vol. 2, pp. 222–230 (2002)

    Google Scholar 

  16. Marques-Silva, J.P., Sakallah, K.A.: GRASP: A new search algorithm for satisfiability. In: 1996 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 1996. Digest of Technical Papers, pp. 220–227 (1996)

    Google Scholar 

  17. Mitchell, D.G.: A SAT solver primer. EATCS Bulletin 85, 112–133 (2005)

    MATH  Google Scholar 

  18. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th ACM/IEEE Design Automation Conference (DAC 2001), pp. 530–535. ACM Press (2001)

    Google Scholar 

  19. Niemelä, I.: Stable models and difference logic. Annals of Mathematics and Artificial Intelligence 53(1-4), 313–329 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  20. Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 321–334. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  21. Rintanen, J., Heljanko, K., Niemelä, I.: Parallel encodings of classical planning as satisfiability. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 307–319. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  22. Subbarayan, S., Pradhan, D.K.: NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 276–291. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  23. Tamura, N., Taga, A., Kitagawa, S., Banbara, M.: Compiling finite linear CSP into SAT. Constraints 14(2), 254–272 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  24. Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM Journal on Computing 1(2), 146–160 (1972)

    Article  MathSciNet  MATH  Google Scholar 

  25. Wolfman, S.A., Weld, D.S.: The LPSAT engine & its application to resource planning. In: Proceedings of the 16th International Joint Conference on Artificial Intelligence, pp. 310–315. Morgan Kaufmann Publishers (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Helsinki Institute for Information Technology HIIT, Department of Information and Computer Science, Aalto University, FI-00076, AALTO, Finland

    Martin Gebser, Tomi Janhunen & Jussi Rintanen

Authors
  1. Martin Gebser
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tomi Janhunen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jussi Rintanen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Madeira, Funchal, Madeira, Portugal

    Eduardo Fermé

  2. CENTRIA, Universidade Nova de Lisboa, Caparica, Portugal

    João Leite

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Gebser, M., Janhunen, T., Rintanen, J. (2014). SAT Modulo Graphs: Acyclicity. In: Fermé, E., Leite, J. (eds) Logics in Artificial Intelligence. JELIA 2014. Lecture Notes in Computer Science(), vol 8761. Springer, Cham. https://doi.org/10.1007/978-3-319-11558-0_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-11558-0_10

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-11557-3

  • Online ISBN: 978-3-319-11558-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation