{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T04:59:48Z","timestamp":1743137988240,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"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_16","type":"book-chapter","created":{"date-parts":[[2019,6,28]],"date-time":"2019-06-28T21:02:31Z","timestamp":1561755751000},"page":"222-238","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Revisiting Graph Width Measures for CNF-Encodings"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Mengel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Romain","family":"Wallon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,6,29]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Amarilli, A., Capelli, F., Monet, M., Senellart, P.: Connecting knowledge compilation classes and width parameters CoRR, abs\/1811.02944 (2018)","DOI":"10.1007\/s00224-019-09930-2"},{"key":"16_CR2","unstructured":"Amarilli, A., Monet, M., Senellart, P.: Connecting width and structure in knowledge compilation. In: 21st International Conference on Database Theory, ICDT, Vienna, Austria, 26\u201329 March 2018 (2018)"},{"key":"16_CR3","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press (2009)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-319-24318-4_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"S Bova","year":"2015","unstructured":"Bova, S., Capelli, F., Mengel, S., Slivovsky, F.: On compiling CNFs into structured deterministic DNNFs. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 199\u2013214. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_15"},{"key":"16_CR5","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 (2016)"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Bova, S., Szeider, S.: Circuit treewidth, sentential decision, and query compilation (2017)","DOI":"10.1145\/3034786.3034787"},{"key":"16_CR7","unstructured":"Brault-Baron, J., Capelli, F., Mengel, S.: Understanding model counting for $$\\beta $$ -acyclic CNF-formulas CoRR, abs\/1405.6043 (2014)"},{"issue":"1","key":"16_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.dam.2010.09.007","volume":"159","author":"I Briquel","year":"2011","unstructured":"Briquel, I., Koiran, P., Meer, K.: On the expressive power of CNF formulas of bounded tree- and clique-width. Discrete Appl. Math. 159(1), 1\u201314 (2011)","journal-title":"Discrete Appl. Math."},{"key":"16_CR9","unstructured":"Capelli, F., Mengel, S.: Tractable QBF by knowledge compilation. In: 36th International Symposium on Theoretical Aspects of Computer Science, STACS 2019, vol. 126, pp. 18:1\u201318:16 (2019)"},{"key":"16_CR10","unstructured":"Chen, H.: Quantified constraint satisfaction and bounded treewidth. In: Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI 2004 (2004)"},{"key":"16_CR11","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."},{"key":"16_CR12","series-title":"Volume 173 of Graduate texts in Mathematics","volume-title":"Graph Theory","author":"R Diestel","year":"2012","unstructured":"Diestel, R.: Graph Theory. Volume 173 of Graduate texts in Mathematics, 4th edn. Springer, Heidelberg (2012)","edition":"4"},{"issue":"4","key":"16_CR13","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1016\/j.dam.2006.06.020","volume":"156","author":"E Fischer","year":"2008","unstructured":"Fischer, E., Makowsky, J., Ravve, E.: Counting truth assignments of formulas of bounded tree-width or clique-width. Discrete Appl. Math. 156(4), 511\u2013529 (2008)","journal-title":"Discrete Appl. Math."},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-319-66263-3_3","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"R Ganian","year":"2017","unstructured":"Ganian, R., Szeider, S.: New width parameters for model counting. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 38\u201352. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_3"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Gaspers, S., Szeider, S.: Strong backdoors to bounded treewidth SAT. In: 54th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2013 (2013)","DOI":"10.1109\/FOCS.2013.59"},{"key":"16_CR16","unstructured":"Gent, I.P., Nightingale, P.: A new encoding of AllDifferent into SAT. In: International Workshop on Modelling and Reformulating Constraint Satisfaction Problems (2004)"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Maratea, E., Tacchella, A.: Dependent and independent variables in propositional satisfiability. In: Logics in Artificial Intelligence. JELIA 2002 (2002)","DOI":"10.1007\/3-540-45757-7_25"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Golumbic, M.C., Gurvich, V.: Read-once functions. In: Boolean Functions: Theory, Algorithms and Applications, pp. 519\u2013560 (2011)","DOI":"10.1017\/CBO9780511852008.011"},{"issue":"1","key":"16_CR19","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/j.artint.2009.10.003","volume":"174","author":"Georg Gottlob","year":"2010","unstructured":"Gottlob, G., Pichler, R., Wei, F.: Bounded treewidth as a key to tractability of knowledge representation and reasoning. Artif. Intell., 174(1), 105\u2013132 (2010)","journal-title":"Artificial Intelligence"},{"key":"16_CR20","unstructured":"Jakl, M., Pichler, R., Woltran, S.: Answer-set programming with bounded treewidth. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence. IJCAI 2009 (2009)"},{"issue":"3","key":"16_CR21","first-page":"99","volume":"24","author":"M Krause","year":"1988","unstructured":"Krause, M.: Exponential lower bounds on the complexity of local and real-time branching programs. Elektronische Informationsverarbeitung und Kybernetik 24(3), 99\u2013110 (1988)","journal-title":"Elektronische Informationsverarbeitung und Kybernetik"},{"key":"16_CR22","volume-title":"Communication Complexity","author":"E Kushilevitz","year":"1997","unstructured":"Kushilevitz, E., Nisan, N.: Communication Complexity. Cambridge University Press, Cambridge (1997)"},{"key":"16_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-319-94144-8_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"M Lampis","year":"2018","unstructured":"Lampis, M., Mengel, S., Mitsou, V.: QBF as an alternative to Courcelle\u2019s theorem. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 235\u2013252. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_15"},{"key":"16_CR24","unstructured":"Paulusma, D., Slivovsky, F., Szeider, S.: Model counting for CNF formulas of bounded modular treewidth. In: 30th International Symposium on Theoretical Aspects of Computer Science, STACS 2013 (2013)"},{"issue":"1","key":"16_CR25","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/s00453-015-0030-x","volume":"76","author":"D Paulusma","year":"2016","unstructured":"Paulusma, D., Slivovsky, F., Szeider, S.: Model counting for CNF formulas of bounded modular treewidth. Algorithmica 76(1), 168\u2013194 (2016)","journal-title":"Algorithmica"},{"key":"16_CR26","unstructured":"Pipatsrisawat, K., Darwiche, A.: New compilation languages based on structured decomposability. In: Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, AAAI 2008 (2008)"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Pipatsrisawat, T., Darwiche, A.: A lower bound on the size of decomposable negation normal form. In: Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2010 (2010)","DOI":"10.1609\/aaai.v24i1.7600"},{"key":"16_CR28","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1613\/jair.4831","volume":"54","author":"SH S\u00e6ther","year":"2015","unstructured":"S\u00e6ther, S.H., Telle, J.A., Vatshelle, M.: Solving #SAT and MAXSAT by dynamic programming. J. Artif. Intell. Res. 54, 59\u201382 (2015)","journal-title":"J. Artif. Intell. Res."},{"issue":"1","key":"16_CR29","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1016\/j.jda.2009.06.002","volume":"8","author":"M Samer","year":"2010","unstructured":"Samer, M., Szeider, S.: Algorithms for propositional model counting. J. Discrete Algorithms 8(1), 50\u201364 (2010)","journal-title":"J. Discrete Algorithms"},{"issue":"2","key":"16_CR30","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.jcss.2009.04.003","volume":"76","author":"M Samer","year":"2010","unstructured":"Samer, M., Szeider, S.: Constraint satisfaction with bounded treewidth revisited. J. Comput. Syst. Sci. 76(2), 103\u2013114 (2010)","journal-title":"J. Comput. Syst. Sci."},{"key":"16_CR31","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/11564751_73","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"Carsten Sinz","year":"2005","unstructured":"Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: 11th International Conference Principles and Practice of Constraint Programming - CP 2005. CP 2005 (2005)"},{"key":"16_CR32","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/978-3-642-45030-3_63","volume-title":"Algorithms and Computation","author":"Friedrich Slivovsky","year":"2013","unstructured":"Slivovsky, F., Szeider, S.: Model counting for formulas of bounded clique-width. In: 24th International Symposium on Algorithms and Computation. ISAAC 2013 (2013)"},{"key":"16_CR33","unstructured":"Vatshelle, M.: New width parameters of graphs. Ph.D. Thesis, University of Bergen (2012)"},{"key":"16_CR34","doi-asserted-by":"crossref","unstructured":"Wegener, I.: Branching Programs and Binary Decision Diagrams. SIAM (2000)","DOI":"10.1137\/1.9780898719789"}],"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_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,22]],"date-time":"2022-09-22T10:34:02Z","timestamp":1663842842000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-24258-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030242572","9783030242589"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-24258-9_16","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)"}}]}}