Abstract
Bipartitioning the set of variables \( Var (\varSigma )\) of a propositional formula \(\varSigma \) w.r.t. definability consists in pointing out a bipartition \(\langle I, O\rangle \) of \( Var (\varSigma )\) such that \(\varSigma \) defines the variables of O (outputs) in terms of the variables in I (inputs), i.e., for every \(o \in O\), there exists a formula \(\varPhi _o\) over I such that \(o \Leftrightarrow \varPhi _o\) is a logical consequence of \(\varSigma \). The existence of \(\varPhi _o\) given o, I, and \(\varSigma \) is a coNP-complete problem, and as such, it can be addressed in practice using a SAT solver. From a computational perspective, definability bipartitioning has been shown as a valuable preprocessing technique for model counting, a key task for a number of AI problems involving probabilities. To maximize the benefits offered by such a preprocessing, one is interested in deriving subset-minimal bipartitions in terms of input variables, i.e., definability bipartitions \(\langle I, O\rangle \) such that for every \(i \in I\), \(\langle I \setminus \{i\}, O \cup \{i\}\rangle \) is not a definability bipartition. We show how the computation of subset-minimal bipartitions can be boosted by leveraging not only the decisions furnished by SAT solvers (as done in previous approaches), but also the SAT witnesses (models and cores) justifying those decisions.
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.
In practice, computing smallest bipartitions in terms of input variables, i.e., bipartitions \(\langle I, O\rangle \) such that |I| is minimal, is in general too demanding for being useful.
- 2.
Obviously enough, in the remaining case when \(y \in X\), \(\varSigma \) defines y in terms of X.
- 3.
See http://www.cril.univ-artois.fr/kc/benchmarks.html for details.
References
Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309–317. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39071-5_23
Beth, E.: On Padoa’s method in the theory of definition. Indag. Math. 15, 330–339 (1953)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3_37
Ivrii, A., Malik, S., Meel, K.S., Vardi, M.Y.: On computing minimal independent support and its applications to sampling and counting. Constraints Int. J. 21(1), 41–58 (2016). https://doi.org/10.1007/s10601-015-9204-z
Kiesel, R., Totis, P., Kimmig, A.: Efficient knowledge compilation beyond weighted model counting. Theory Pract. Log. Program. 22(4), 505–522 (2022). https://doi.org/10.1017/S147106842200014X
Lagniez, J., Lonca, E., Marquis, P.: Improving model counting by leveraging definability. In: Kambhampati, S. (ed.) Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9–15 July 2016, pp. 751–757. IJCAI/AAAI Press (2016). http://www.ijcai.org/Abstract/16/112
Lagniez, J., Lonca, E., Marquis, P.: Definability for model counting. Artif. Intell. 281, 103229 (2020). https://doi.org/10.1016/j.artint.2019.103229
Lagniez, J., Marquis, P.: On preprocessing techniques and their impact on propositional model counting. J. Autom. Reason. 58(4), 413–481 (2017). https://doi.org/10.1007/s10817-016-9370-8
Lang, J., Liberatore, P., Marquis, P.: Propositional independence: formula-variable independence and forgetting. J. Artif. Intell. Res. 18, 391–443 (2003)
Lang, J., Marquis, P.: On propositional definability. Artif. Intell. 172(8–9), 991–1017 (2008). https://doi.org/10.1016/j.artint.2007.12.003
Lin, F., Reiter, R.: Forget it! In: Proceedings of AAAI Fall Symposium on Relevance, pp. 154–159 (1994)
Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition. Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 133–182. IOS Press (2021). https://doi.org/10.3233/FAIA200987
Padoa, A.: Essai d’une théorie algébrique des nombres entiers, précédé d’une introduction logique à une théorie déductive quelconque. In: Bibliothèque du Congrès International de Philosophie, Paris, pp. 309–365 (1903)
Soos, M., Meel, K.S.: Arjun: an efficient independent support computation technique and its applications to counting and sampling. In: Mitra, T., Young, E.F.Y., Xiong, J. (eds.) Proceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2022, San Diego, California, USA, 30 October–3 November 2022, p. 71. ACM (2022). https://doi.org/10.1145/3508352.3549406
Acknowledgements
The authors would like to thank the anonymous reviewers for their comments and insights. This work has benefited from the support of the PING/ACK project (ANR-18-CE40-0011) of the French National Research Agency (ANR).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Lagniez, JM., Marquis, P. (2023). Boosting Definability Bipartition Computation Using SAT Witnesses. In: Gaggl, S., Martinez, M.V., Ortiz, M. (eds) Logics in Artificial Intelligence. JELIA 2023. Lecture Notes in Computer Science(), vol 14281. Springer, Cham. https://doi.org/10.1007/978-3-031-43619-2_47
Download citation
DOI: https://doi.org/10.1007/978-3-031-43619-2_47
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-43618-5
Online ISBN: 978-3-031-43619-2
eBook Packages: Computer ScienceComputer Science (R0)