{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T09:50:36Z","timestamp":1743069036373,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030242572"},{"type":"electronic","value":"9783030242589"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-24258-9_6","type":"book-chapter","created":{"date-parts":[[2019,6,28]],"date-time":"2019-06-28T21:02:31Z","timestamp":1561755751000},"page":"90-99","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Knowledge Compilation Languages as Proof Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2842-8223","authenticated-orcid":false,"given":"Florent","family":"Capelli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,6,29]]},"reference":[{"key":"6_CR1","unstructured":"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)"},{"issue":"8\u2014-9","key":"6_CR2","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1016\/j.artint.2007.03.001","volume":"171","author":"ML Bonet","year":"2007","unstructured":"Bonet, M.L., Levy, J., Many\u00e0, F.: Resolution for Max-SAT. Artif. Intell. 171(8\u2014-9), 606\u2013618 (2007)","journal-title":"Artif. Intell."},{"key":"6_CR3","unstructured":"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\u201315 July 2016, pp. 1008\u20131014 (2016)"},{"key":"6_CR4","unstructured":"Capelli, F.: Structural restrictions of CNF formulas: application to model counting and knowledge compilation. PhD thesis, Universit\u00e9 Paris Diderot (2016)"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/237814.237860"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing, pp. 151\u2013158. ACM (1971)","DOI":"10.1145\/800157.805047"},{"issue":"1","key":"6_CR7","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36\u201350 (1979)","journal-title":"J. Symb. Log."},{"issue":"1\u20132","key":"6_CR8","doi-asserted-by":"publisher","first-page":"11","DOI":"10.3166\/jancl.11.11-34","volume":"11","author":"A Darwiche","year":"2001","unstructured":"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\u20132), 11\u201334 (2001)","journal-title":"J. Appl. Non-Classical Log."},{"key":"6_CR9","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1613\/jair.989","volume":"17","author":"A Darwiche","year":"2002","unstructured":"Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. 17, 229\u2013264 (2002)","journal-title":"J. Artif. Intell. Res."},{"issue":"7","key":"6_CR10","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"3","key":"6_CR11","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"6_CR12","unstructured":"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\u2013162 (2005)"},{"key":"6_CR13","series-title":"Algorithms and combinatorics","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24508-4","volume-title":"Boolean Function Complexity - Advances and Frontiers","author":"S Jukna","year":"2012","unstructured":"Jukna, S.: Boolean Function Complexity - Advances and Frontiers. Algorithms and combinatorics, vol. 27. Springer, Heidelberg (2012)"},{"key":"6_CR14","unstructured":"Koriche, F., Le Berre, D., Lonca, E., Marquis, P.: Fixed-parameter tractable optimization under DNNF constraints. In: ECAI 2016\u201322nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands - Including Prestigious Applications of Artificial Intelligence (PAIS 2016), pp. 1194\u20131202 (2016)"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.24963\/ijcai.2017\/93"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Lagniez, J.-M., Marquis, P., Szczepanski, N.: DMC: a distributed model counter. In: IJCAI, pp. 1331\u20131338 (2018)","DOI":"10.24963\/ijcai.2018\/185"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MAXSAT resolution. In: Twenty-Eighth AAAI Conference on Artificial Intelligence (2014)","DOI":"10.1609\/aaai.v28i1.9124"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Nordstr\u00f6m, J.: Pebble games, proof complexity, and time-space trade-offs. Logical Methods Comput. Sci. (LMCS) 9(3) (2013)","DOI":"10.2168\/LMCS-9(3:15)2013"},{"key":"6_CR19","unstructured":"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\u20133148 (2015)"},{"issue":"2","key":"6_CR20","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","volume":"175","author":"K Pipatsrisawat","year":"2011","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning sat solvers as resolution engines. Artif. Intell. 175(2), 512\u2013525 (2011)","journal-title":"Artif. Intell."},{"key":"6_CR21","first-page":"7th","volume":"4","author":"T Sang","year":"2004","unstructured":"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)","journal-title":"Theory Appl. Satisf. Test."},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/11814948_38","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"M Thurley","year":"2006","unstructured":"Thurley, M.: sharpSAT \u2013 counting models with advanced component caching and implicit BCP. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 424\u2013429. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814948_38"},{"key":"6_CR23","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898719789","volume-title":"Branching Programs and Binary Decision Diagrams","author":"I Wegener","year":"2000","unstructured":"Wegener, I.: Branching Programs and Binary Decision Diagrams. SIAM, Philadelphia (2000)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2019"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-24258-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,22]],"date-time":"2022-09-22T10:32:36Z","timestamp":1663842756000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-24258-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030242572","9783030242589"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-24258-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"29 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sat2019.tecnico.ulisboa.pt\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"64","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}