Hostname: page-component-74656f9884-8r8nv Total loading time: 0 Render date: 2026-11-10T05:37:31.961Z Has data issue: false hasContentIssue false
  • English
  • Français

Multi-threaded ASP solving with clasp

Published online by Cambridge University Press:  05 September 2012

MARTIN GEBSER ,
BENJAMIN KAUFMANN  and
TORSTEN SCHAUB
MARTIN GEBSER
Affiliation:
Institut für Informatik, Universität Potsdam
BENJAMIN KAUFMANN
Affiliation:
Institut für Informatik, Universität Potsdam
TORSTEN SCHAUB
Affiliation:
Institut für Informatik, Universität Potsdam
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

We present the new multi-threaded version of the state-of-the-art answer set solver clasp. We detail its component and communication architecture and illustrate how they support the principal functionalities of clasp. Also, we provide some insights into the data representation used for different constraint types handled by clasp. All this is accompanied by an extensive experimental analysis of the major features related to multi-threading in clasp.

Information

Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 12 , Issue 4-5: 28th International Conference on Logic Programming , July 2012 , pp. 525 - 545
Copyright
Copyright © Cambridge University Press 2012

References

Audemard, G. and Simon, L. 2009. Predicting learnt clauses quality in modern SAT solvers. See Boutilier, 399–404.Google Scholar
Balduccini, M., Pontelli, E., El-Khatib, O. and Le, H. 2005. Issues in parallel execution of non-monotonic reasoning systems. Parallel Computing 31, 6, 608–647.CrossRefGoogle Scholar
Baral, C. 2003. Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press.Google Scholar
Biere, A. 2011. Lingeling and Friends at the SAT Competition 2011. Technical Report FMV 11/1, Institute for Formal Models and Verification, Johannes Kepler University.Google Scholar
Biere, A., Heule, M., vanMaaren, H. Maaren, H. and Walsh, T., Eds. 2009. Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press.Google Scholar
Blochinger, W., Sinz, C. and Küchlin, W. 2003. Parallel propositional satisfiability checking with distributed dynamic learning. Parallel Computing 29, 7, 969–994.CrossRefGoogle Scholar
Boutilier, C., Ed. 2009. Proceedings of the Twenty-first International Joint Conference on Artificial Intelligence (IJCAI'09). AAAI Press.Google Scholar
and Codognet, P. 1994. Parallel logic programming systems. ACM Computing Surveys 26, 3, 295–336.Google Scholar
Clark, K. 1978. Negation as failure. In Logic and Data Bases, Gallaire, H. and Minker, J., Eds. Plenum Press, 293–322.Google Scholar
Davis, M., Logemann, G. and Loveland, D. 1962. A machine program for theorem-proving. Communications of the ACM 5, 394–397.Google Scholar
Davis, M. and Putnam, H. 1960. A computing procedure for quantification theory. Journal of the ACM 7, 201–215.Google Scholar
Eén, N. and Biere, A. 2005. Effective preprocessing in SAT through variable and clause elimination. In Proceedings of the Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT'05), Bacchus, F. and Walsh, T., Eds. Lecture Notes in Computer Science, vol. 3569. Springer-Verlag, 61–75.Google Scholar
Ellguth, E., Gebser, M., Gusowski, M., Kaminski, R., Kaufmann, B., Liske, S., Schaub, T., Schneidenbach, L. and Schnor, B. 2009. A simple distributed conflict-driven answer set solver. In Proceedings of the Tenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'09), Erdem, E., Lin, F. and Schaub, T., Eds. Lecture Notes in Artificial Intelligence, vol. 5753. Springer-Verlag, 490–495.CrossRefGoogle Scholar
Finkel, R., Marek, V., Moore, N. and Truszczyński, M. 2001. Computing stable models in parallel. In Proceedings of the First International Workshop on Answer Set Programming (ASP'01), Provetti, A. and Son, T., Eds. AAAI Press, 72–76.Google Scholar
Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T. and Schneider, M. 2011a. Potassco: The Potsdam answer set solving collection. AI Communications 24, 2, 105–124.Google Scholar
Gebser, M., Kaminski, R., Kaufmann, B. and Schaub, T. 2011b. Multi-criteria optimization in answer set programming. In Technical Communications of the Twenty-seventh International Conference on Logic Programming (ICLP'11), Gallagher, J. and Gelfond, M., Eds. Leibniz International Proceedings in Informatics, vol. 11. Dagstuhl Publishing, 1–10.Google Scholar
Gebser, M., Kaminski, R., Kaufmann, B. and Schaub, T. 2011c. Multi-criteria optimization in ASP and its application to Linux package configuration. Available at http://www.cs.uni-potsdam.de/wv/pdfformat/gekakasc11b.pdf.Google Scholar
Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T. and Schnor, B. 2011d. Cluster-based ASP solving with claspar. In Proceedings of the Eleventh International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'11), Delgrande, J. and Faber, W., Eds. Lecture Notes in Artificial Intelligence, vol. 6645. Springer-Verlag, 364–369.CrossRefGoogle Scholar
Gebser, M., Kaufmann, B., Neumann, A. and Schaub, T. 2007a. Conflict-driven answer set enumeration. In Proceedings of the Ninth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'07), Baral, C., Brewka, G. and Schlipf, J., Eds. Lecture Notes in Artificial Intelligence, vol. 4483. Springer-Verlag, 136–148.Google Scholar
Gebser, M., Kaufmann, B., Neumann, A. and Schaub, T. 2007b. Conflict-driven answer set solving. In Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI'07), Veloso, M., Ed. AAAI Press, 386–392.Google Scholar
Gebser, M., Kaufmann, B., Neumann, A. and Schaub, T. 2008. Advanced preprocessing for answer set solving. In Proceedings of the Eighteenth European Conference on Artificial Intelligence (ECAI'08), Ghallab, M., Spyropoulos, C., Fakotakis, N. and Avouris, N., Eds. IOS Press, 15–19.Google Scholar
Gebser, M., Ostrowski, M. and Schaub, T. 2009. Constraint answer set solving. In Proceedings of the Twenty-fifth International Conference on Logic Programming (ICLP'09), Hill, P. and Warren, D., Eds. Lecture Notes in Computer Science, vol. 5649. Springer-Verlag, 235–249.Google Scholar
Gomes, C. and Selman, B. 2001. Algorithm portfolios. Artificial Intelligence 126, 1–2, 43–62.Google Scholar
Gressmann, J., Janhunen, T., Mercer, R., Schaub, T., Thiele, S. and Tichy, R. 2005. Platypus: A platform for distributed answer set solving. In Proceedings of the Eighth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'05), C. Baral, Greco, G., Leone, N. and Terracina, G., Eds. Lecture Notes in Artificial Intelligence, vol. 3662. Springer-Verlag, 227–239.Google Scholar
Gressmann, J., Janhunen, T., Mercer, R., Schaub, T., Thiele, S. and Tichy, R. 2006. On probing and multi-threading in platypus. In Proceedings of the Seventeenth European Conference on Artificial Intelligence (ECAI'06), Brewka, G., Coradeschi, S., Perini, A. and Traverso, P., Eds. IOS Press, 392–396.Google Scholar
Gropp, W., Lusk, E. and Thakur, R. 1999. Using MPI-2: Advanced Features of the Message-Passing Interface. MIT Press.Google Scholar
Gupta, G., Pontelli, E., Ali, K., Carlsson, M. and Hermenegildo, M. 2001. Parallel execution of Prolog programs: A survey. ACM Transactions on Programming Languages and Systems 23, 4, 472–602.CrossRefGoogle Scholar
Hamadi, Y., Jabbour, S. and Sais, L. 2009a. Control-based clause sharing in parallel SAT solving. See Boutilier, 499–504.Google Scholar
Hamadi, Y., Jabbour, S. and Sais, L. 2009b. ManySAT: A parallel SAT solver. Journal on Satisfiability, Boolean Modeling and Computation 6, 245–262.CrossRefGoogle Scholar
Han, H. and Somenzi, F. 2009. On-the-fly clause improvement. See Kullmann, 209–222.Google Scholar
Herlihy, M. and Shavit, N. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann Publishers.Google Scholar
Hirsimäki, T. 2001. Distributing Backtracking Search Trees. Technical Report, Helsinki University of Technology.Google Scholar
Hyvärinen, A., Junttila, T. and Niemelä, I. 2011. Partitioning search spaces of a randomized search. Fundamenta Informaticae 107, 2-3, 289–311.Google Scholar
Järvisalo, M., Biere, A. and Heule, M. 2010. Blocked clause elimination. In Proceedings of the Sixteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10), Esparza, J. and Majumdar, R., Eds. Lecture Notes in Computer Science, vol. 6015. Springer-Verlag, 129–144.Google Scholar
Kullmann, O., Ed. 2009. Proceedings of the Twelfth International Conference on Theory and Applications of Satisfiability Testing (SAT'09). Lecture Notes in Computer Science, vol. 5584. Springer-Verlag.Google Scholar
Li, C. and Manyà, F. 2009. MaxSAT. See Biere et al., Chapter 19, 613–631.Google Scholar
Marques-Silva, J., Argelich, J., Graça, A. and Lynce, I. 2011. Boolean lexicographic optimization: Algorithms and applications. Annals of Mathematics and Artificial Intelligence 62, 3-4, 317–343.Google Scholar
Marques-Silva, J. and Sakallah, K. 1999. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers 48, 5, 506–521.Google Scholar
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L. and Malik, S. 2001. Chaff: Engineering an efficient SAT solver. In Proceedings of the Thirty-eighth Conference on Design Automation (DAC'01). ACM Press, 530–535.Google Scholar
Pontelli, E., Balduccini, M. and Bermudez, F. 2003. Non-monotonic reasoning on Beowulf platforms. In Proceedings of the Fifth International Symposium on Practical Aspects of Declarative Languages (PADL'03), Dahl, V. and Wadler, P., Eds. Lecture Notes in Artificial Intelligence, vol. 2562. Springer-Verlag, 37–57.Google Scholar
Roussel, O. 2011. Description of ppfolio. Available at http://www.cril.univ-artois.fr/~roussel/ppfolio/solver1.pdf.Google Scholar
Ryan, L. 2004. Efficient Algorithms for Clause-learning SAT Solvers. Master's Thesis, Simon Fraser University.Google Scholar
Schubert, T., Lewis, M. and Becker, B. 2009. PaMiraXT: Parallel SAT solving with threads and message passing. Journal on Satisfiability, Boolean Modeling and Computation 6, 203–222.Google Scholar
Simons, P., Niemelä, I. and Soininen, T. 2002. Extending and implementing the stable model semantics. Artificial Intelligence 138, 1-2, 181–234.Google Scholar
Soos, M., Nohl, K. and Castelluccia, C. 2009. Extending SAT solvers to cryptographic problems. See Kullmann, 244–257.Google Scholar
Syrjänen, T. Lparse 1.0 user's manual. Available at http://www.tcs.hut.fi/Software/smodels/lparse.ps.gz.Google Scholar
Zhang, H., Bonacina, M. and Hsiang, J. 1996. PSATO: A distributed propositional prover and its application to quasigroup problems. Journal of Symbolic Computation 21, 4, 543–560.Google Scholar
Zhang, L., Madigan, C., Moskewicz, M. and Malik, S. 2001. Efficient conflict driven learning in a Boolean satisfiability solver. In Proceedings of the International Conference on Computer-Aided Design (ICCAD'01). 279–285.Google Scholar
Zhang, L. and Malik, S. 2003. Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In Proceedings of the Sixth Conference on Design, Automation and Test in Europe (DATE'03). IEEE Computer Society, 10880–10885.Google Scholar