{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,16]],"date-time":"2025-12-16T12:22:14Z","timestamp":1765887734837},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243177"},{"type":"electronic","value":"9783319243184"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24318-4_10","type":"book-chapter","created":{"date-parts":[[2015,9,11]],"date-time":"2015-09-11T01:42:56Z","timestamp":1441935776000},"page":"121-137","source":"Crossref","is-referenced-by-count":16,"title":["$$\\#\\exists $$ SAT: Projected Model Counting"],"prefix":"10.1007","author":[{"given":"Rehan Abdul","family":"Aziz","sequence":"first","affiliation":[]},{"given":"Geoffrey","family":"Chu","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Muise","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Stuckey","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,10,27]]},"reference":[{"key":"10_CR1","unstructured":"Bacchus, F., Dalmao, S., Pitassi, T.: DPLL with Caching: A new algorithm for #SAT and Bayesian Inference. Electronic Colloquium on Computational Complexity (ECCC) 10(003) (2003)"},{"key":"10_CR2","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1613\/jair.2648","volume":"34","author":"F Bacchus","year":"2009","unstructured":"Bacchus, F., Dalmao, S., Pitassi, T.: Solving #SAT and Bayesian Inference with Backtracking Search. Journal of Artificial Intelligence Research (JAIR) 34, 391\u2013442 (2009)","journal-title":"Journal of Artificial Intelligence Research (JAIR)"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-642-22110-1_17","volume-title":"Computer Aided Verification","author":"J Brauer","year":"2011","unstructured":"Brauer, J., King, A., Kriener, J.: Existential quantification as incremental SAT. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 191\u2013207. Springer, Heidelberg (2011)"},{"issue":"4","key":"10_CR4","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1145\/502090.502091","volume":"48","author":"A Darwiche","year":"2001","unstructured":"Darwiche, A.: Decomposable negation normal form. J. ACM 48(4), 608\u2013647 (2001)","journal-title":"J. ACM"},{"key":"10_CR5","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1613\/jair.989","volume":"17","author":"A Darwiche","year":"2002","unstructured":"Darwiche, A., Marquis, P.: A knowledge compilation map. Journal of Artificial Intelligence Research (JAIR) 17, 229\u2013264 (2002)","journal-title":"Journal of Artificial Intelligence Research (JAIR)"},{"issue":"7","key":"10_CR6","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. Communications of the ACM 5(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"10_CR7","unstructured":"Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Conflict-driven answer set solving. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence, p. 386. MIT Press, January 2007"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-01929-6_7","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"M Gebser","year":"2009","unstructured":"Gebser, M., Kaufmann, B., Schaub, T.: Solution enumeration for projected boolean search problems. In: van Hoeve, W.-J., Hooker, J.N. (eds.) CPAIOR 2009. LNCS, vol. 5547, pp. 71\u201386. Springer, Heidelberg (2009)"},{"key":"10_CR9","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.artint.2012.04.001","volume":"187","author":"M Gebser","year":"2012","unstructured":"Gebser, M., Kaufmann, B., Schaub, T.: Conflict-driven answer set solving: From theory to practice. Artificial Intelligence 187, 52\u201389 (2012)","journal-title":"Artificial Intelligence"},{"key":"10_CR10","unstructured":"Ginsberg, M.L., Parkes, A.J., Roy, A.: Supermodels and robustness. In: Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference, AAAI 1998, IAAI 1998, July 26\u201330, 1988, Madison, Wisconsin, USA, pp. 334\u2013339 (1998)"},{"key":"10_CR11","unstructured":"Goldberg, E., Manolios, P.: Quantifier elimination by dependency sequents. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 34\u201343, October 2012"},{"key":"10_CR12","unstructured":"Gomes, C.P., Sabharwal, A., Selman, B.: Model counting (2008)"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-40196-1_16","volume-title":"Quantitative Evaluation of Systems","author":"V Klebanov","year":"2013","unstructured":"Klebanov, V., Manthey, N., Muise, C.: SAT-based analysis and quantification of information flow in programs. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 177\u2013192. Springer, Heidelberg (2013)"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"10_CR15","unstructured":"Palacios, H., Bonet, B., Darwiche, A., Geffner, H.: Pruning conformant plans by counting models on compiled d-dnnf representations. In: Proceedings of the Fifteenth International Conference on Automated Planning and Scheduling (ICAPS 2005), June 5\u201310, 2005, Monterey, California, USA, pp. 141\u2013150 (2005)"},{"key":"10_CR16","unstructured":"Sang, T., Bacchus, F., Beame, P., Kautz, H.A., Pitassi, T.: Combining component caching and clause learning for effective model counting. In: Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT 2004) (2004)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/11499107_17","volume-title":"Theory and Applications of Satisfiability Testing","author":"T Sang","year":"2005","unstructured":"Sang, T., Beame, P., Kautz, H.: Heuristics for fast exact model counting. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 226\u2013240. Springer, Heidelberg (2005)"},{"key":"10_CR18","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)"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-642-41010-9_4","volume-title":"Formal Methods for Industrial Critical Systems","author":"C Zengler","year":"2013","unstructured":"Zengler, C., K\u00fcchlin, W.: Boolean quantifier elimination for automotive configuration \u2013 a case study. In: Pecheur, C., Dierkes, M. (eds.) FMICS 2013. LNCS, vol. 8187, pp. 48\u201362. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing -- SAT 2015"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24318-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T19:12:31Z","timestamp":1559243551000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24318-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243177","9783319243184"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24318-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}