Abstract
In this paper, we study proof systems in the sense of Cook-Reckhow for problems that are higher in the Polynomial Hierarchy than coNP, in particular, #SAT and maxSAT. We start by explaining how the notion of Cook-Reckhow proof systems can be apply to these problems and show how one can twist existing languages in knowledge compilation such as decision DNNF so that they can be seen as proof systems for problems such as #SAT and maxSAT.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
A regular resolution proof is a resolution proof where, on each path, a variable is resolved at most once.
References
Beame, P., Li, J., Roy, S., Suciu, D.: Lower bounds for exact model counting and applications in probabilistic databases. In: Proceedings of the Twenty-Ninth Conference on Uncertainty in Artificial Intelligence (2013)
Bonet, M.L., Levy, J., Manyà, F.: Resolution for Max-SAT. Artif. Intell. 171(8—-9), 606–618 (2007)
Bova, S., Capelli, F., Mengel, S., Slivovsky, F.: Knowledge compilation meets communication complexity. In: Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9–15 July 2016, pp. 1008–1014 (2016)
Capelli, F.: Structural restrictions of CNF formulas: application to model counting and knowledge compilation. PhD thesis, Université Paris Diderot (2016)
Clegg, M., Edmonds, J., Impagliazzo, R.: Using the groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing, STOC 1996 (1996)
Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing, pp. 151–158. ACM (1971)
Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36–50 (1979)
Darwiche, A.: On the tractable counting of theory models and its application to truth maintenance and belief revision. J. Appl. Non-Classical Log. 11(1–2), 11–34 (2001)
Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. 17, 229–264 (2002)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)
Huang, J., Darwiche, A.: DPLL with a trace: from SAT to knowledge compilation. In: Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, pp. 156–162 (2005)
Jukna, S.: Boolean Function Complexity - Advances and Frontiers. Algorithms and combinatorics, vol. 27. Springer, Heidelberg (2012)
Koriche, F., Le Berre, D., Lonca, E., Marquis, P.: Fixed-parameter tractable optimization under DNNF constraints. In: ECAI 2016–22nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands - Including Prestigious Applications of Artificial Intelligence (PAIS 2016), pp. 1194–1202 (2016)
Lagniez, J.-M., Marquis, P.: An improved decision-DNNF compiler. In: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017 (2017)
Lagniez, J.-M., Marquis, P., Szczepanski, N.: DMC: a distributed model counter. In: IJCAI, pp. 1331–1338 (2018)
Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MAXSAT resolution. In: Twenty-Eighth AAAI Conference on Artificial Intelligence (2014)
Nordström, J.: Pebble games, proof complexity, and time-space trade-offs. Logical Methods Comput. Sci. (LMCS) 9(3) (2013)
Oztok, U., Darwiche, A.: A top-down compiler for sentential decision diagrams. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, pp. 3141–3148 (2015)
Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning sat solvers as resolution engines. Artif. Intell. 175(2), 512–525 (2011)
Sang, T., Bacchus, F., Beame, P., Kautz, H.A., Pitassi, T.: Combining component caching and clause learning for effective model counting. Theory Appl. Satisf. Test. 4, 7th (2004)
Thurley, M.: sharpSAT – counting models with advanced component caching and implicit BCP. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 424–429. Springer, Heidelberg (2006). https://doi.org/10.1007/11814948_38
Wegener, I.: Branching Programs and Binary Decision Diagrams. SIAM, Philadelphia (2000)
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
Capelli, F. (2019). Knowledge Compilation Languages as Proof Systems. In: Janota, M., Lynce, I. (eds) Theory and Applications of Satisfiability Testing – SAT 2019. SAT 2019. Lecture Notes in Computer Science(), vol 11628. Springer, Cham. https://doi.org/10.1007/978-3-030-24258-9_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-24258-9_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-24257-2
Online ISBN: 978-3-030-24258-9
eBook Packages: Computer ScienceComputer Science (R0)