Abstract
Although parity constraints are at the heart of many relevant reasoning modes like sampling or model counting, little attention has so far been paid to their integration into ASP systems. We address this shortcoming and investigate a variety of alternative approaches to implementing parity constraints, ranging from rather basic ASP encodings to more sophisticated theory propagators (featuring Gauss-Jordan elimination). All of them are implemented in the xorro system by building on the theory reasoning capabilities of the ASP system clingo. Our comparative empirical study investigates the impact of the number and size of parity constraints on performance and indicates the merits of the respective implementation techniques. Finally, we benefit from parity constraints to equip xorro with means to sample answer sets, paving the way for new applications of ASP.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
This is achieved by uncompiling them during grounding using meta-encodings.
- 2.
- 3.
The distinction of eager and lazy approaches follows the methodology in Satisfiability modulo theories [1].
- 4.
In turn, multiple conditional terms within an aggregate are separated by semicolons.
- 5.
Our implementation of parity constraints fits perfectly with the parity constraints used in sampling and model counting.
- 6.
This is analogous to parity evaluation using binary decision diagrams (BDDs).
- 7.
- 8.
The transformation process mimicks the use of a theory grammar for clingo [8].
- 9.
- 10.
For more detailed benchmarks results, including individual times per classes please go to http://flavioeverardo.com/research/benchmarks/xorro/.
References
Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere et al. [2], chap. 26, pp. 825–885
Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)
Chakraborty, S., Meel, K.S., Vardi, M.Y.: A scalable and nearly uniform generator of SAT witnesses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 608–623. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_40
Chakraborty, S., Meel, K.S., Vardi, M.Y.: A scalable approximate model counter. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 200–216. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40627-0_18
Denecker, M., Vennekens, J., Bond, S., Gebser, M., Truszczyński, M.: The second answer set programming competition. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS (LNAI), vol. 5753, pp. 637–654. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04238-6_75
Gebser, M., Harrison, A., Kaminski, R., Lifschitz, V., Schaub, T.: Abstract Gringo. Theory Pract. Logic Program. 15(4–5), 449–463 (2015)
Gebser, M., et al.: Potassco User Guide, 2 edn. (2015). http://potassco.org
Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T., Wanko, P.: Theory solving made easy with clingo 5. In: Carro, M., King, A. (eds.) Technical Communications of the Thirty-second International Conference on Logic Programming (ICLP 2016), vol. 52, pp. 2:1–2:15. Open Access Series in Informatics (OASIcs) (2016)
Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T.: Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan and Claypool Publishers, San Rafael (2012)
Gebser, M., Kaminski, R., König, A., Schaub, T.: Advances in gringo series 3. In: Delgrande, J.P., Faber, W. (eds.) LPNMR 2011. LNCS (LNAI), vol. 6645, pp. 345–351. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20895-9_39
Gomes, C.P., Hoffmann, J., Sabharwal, A., Selman, B.: Short XORs for model counting: from theory to practice. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 100–106. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-72788-0_13
Gomes, C., Sabharwal, A., Selman, B.: Near-uniform sampling of combinatorial spaces using XOR constraints. In: Schölkopf, B., Platt, J., Hofmann, T. (eds.) Proceedings of the Twentieth Annual Conference on Neural Information Processing Systems (NIPS 2006), pp. 481–488. MIT Press (2007)
Greßler, A., Oetsch, J., Tompits, H.: \(\sf Harvey\): a system for random testing in ASP. In: Balduccini, M., Janhunen, T. (eds.) LPNMR 2017. LNCS (LNAI), vol. 10377, pp. 229–235. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-61660-5_21
Haanpää, H., Järvisalo, M., Kaski, P., Niemelä, I.: Hard satisfiable clause sets for benchmarking equivalence reasoning techniques. J. Satisfiability Boolean Model. Comput. 2(1–4), 27–46 (2006)
Han, C.-S., Jiang, J.-H.R.: When boolean satisfiability meets gaussian elimination in a simplex way. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 410–426. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_31
Kaminski, R., Schaub, T., Wanko, P.: A tutorial on hybrid answer set solving with clingo. In: Ianni, G., et al. (eds.) Reasoning Web 2017. LNCS, vol. 10370, pp. 167–203. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-61033-7_6
Kaufmann, B., Leone, N., Perri, S., Schaub, T.: Grounding and solving in answer set programming. AI Mag. 37(3), 25–32 (2016)
Laitinen, T.: Extending SAT solver with parity reasoning. Dissertation, Aalto University, November 2014
Meel, K.: Constrained counting and sampling: bridging the gap between theory and practice. Dissertation, Rice University, August 2018
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the Thirty-Eighth Conference on Design Automation (DAC 2001), pp. 530–535. ACM Press (2001)
Schaefer, T.: The complexity of satisfiability problems. In: Lipton, R., Burkhard, W., Savitch, W., Friedman, E., Aho, A. (eds.) Proceedings of the Tenth Annual ACM Symposium on Theory of Computing (STOCS 1978), pp. 216–226. ACM Press (1978)
Soos, M.: Enhanced Gaussian elimination in DPLL-based SAT solvers. In: Le Berre, D. (ed.) Proceedings of the First Workshop on Pragmatics of SAT (PoS 2010). EPiC Series in Computing, vol. 8, pp. 2–14. EasyChair (2012)
Soos, M., Meel, K.: Bird: Engineering an efficient CNF-XOR sat solver and its applications to approximate model counting. In: Van Hentenryck, P., Zhou, Z. (eds.) Proceedings of the Thirty-Third National Conference on Artificial Intelligence (AAAI 2019). AAAI Press (2019, to appear)
Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244–257. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02777-2_24
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Everardo, F., Janhunen, T., Kaminski, R., Schaub, T. (2019). The Return of xorro. In: Balduccini, M., Lierler, Y., Woltran, S. (eds) Logic Programming and Nonmonotonic Reasoning. LPNMR 2019. Lecture Notes in Computer Science(), vol 11481. Springer, Cham. https://doi.org/10.1007/978-3-030-20528-7_21
Download citation
DOI: https://doi.org/10.1007/978-3-030-20528-7_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-20527-0
Online ISBN: 978-3-030-20528-7
eBook Packages: Computer ScienceComputer Science (R0)