{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T05:06:51Z","timestamp":1748668011064},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642410093"},{"type":"electronic","value":"9783642410109"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41010-9_4","type":"book-chapter","created":{"date-parts":[[2013,9,16]],"date-time":"2013-09-16T05:31:39Z","timestamp":1379309499000},"page":"48-62","source":"Crossref","is-referenced-by-count":7,"title":["Boolean Quantifier Elimination for Automotive Configuration \u2013 A Case Study"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Zengler","sequence":"first","affiliation":[]},{"given":"Wolfgang","family":"K\u00fcchlin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/5254.708432","volume":"13","author":"D. Sabin","year":"1998","unstructured":"Sabin, D., Weigel, R.: Product configuration frameworks-a survey. IEEE Intelligent Systems\u00a013, 42\u201349 (1998)","journal-title":"IEEE Intelligent Systems"},{"key":"4_CR2","unstructured":"Astesana, J.M., Bossu, Y., Cosserat, L., Fargier, H.: Constraint-based modeling and exploitation of a vehicle range at Renault\u2019s: Requirement analysis and complexity study. In: Proceedings of the ConfWS 2010, pp. 33\u201339 (2010)"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1023\/A:1006370506164","volume":"24","author":"W. K\u00fcchlin","year":"2000","unstructured":"K\u00fcchlin, W., Sinz, C.: Proving consistency assertions for automotive product data management. Journal of Automated Reasoning\u00a024, 145\u2013163 (2000)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR4","first-page":"329","volume-title":"Proceedings of the CASC 2003","author":"A.M. Seidl","year":"2003","unstructured":"Seidl, A.M., Sturm, T.: Boolean quantification in a first-order context. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) Proceedings of the CASC 2003, pp. 329\u2013345. Institut f\u00fcr Informatik, TU M\u00fcnchen (2003)"},{"key":"4_CR5","first-page":"133","volume":"5","author":"M. Benedetti","year":"2008","unstructured":"Benedetti, M., Mangassarian, H.: QBF-based formal verification: Experience and perspectives. JSAT\u00a05, 133\u2013191 (2008)","journal-title":"JSAT"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Sturm, T., Zengler, C.: Parametric quantified SAT solving. In: Proceedings of the ISSAC 2010. ACM, New York (2010)","DOI":"10.1145\/1837934.1837954"},{"key":"4_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Norwell (1993)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2002","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 250. Springer, Heidelberg (2002)"},{"key":"4_CR9","first-page":"149","volume-title":"Proceedings of the IJCAI 2007","author":"N. Narodytska","year":"2007","unstructured":"Narodytska, N., Walsh, T.: Constraint and variable ordering heuristics for compiling configuration problems. In: Proceedings of the IJCAI 2007, pp. 149\u2013154. Morgan Kaufmann Publishers Inc., San Francisco (2007)"},{"key":"4_CR10","unstructured":"Matthes, B., Zengler, C., K\u00fcchlin, W.: An improved constraint ordering heuristics for compiling configuration problems. In: Mayer, W., Albert, P. (eds.) Proceedings of the ConfWS, pp. 36\u201340 (2012)"},{"key":"4_CR11","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. Journal of the ACM\u00a048, 608\u2013647 (2001)","journal-title":"Journal of the ACM"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-540-30494-4_20","volume-title":"Formal Methods in Computer-Aided Design","author":"O. Grumberg","year":"2004","unstructured":"Grumberg, O., Schuster, A., Yadgar, A.: Memory efficient all-solutions SAT solver and its application for reachability analysis. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 275\u2013289. Springer, Heidelberg (2004)"},{"key":"4_CR13","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.\u00a05547, pp. 71\u201386. Springer, Heidelberg (2009)"},{"key":"4_CR14","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.\u00a06806, pp. 191\u2013207. Springer, Heidelberg (2011)"},{"key":"4_CR15","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. Journal of the ACM\u00a07, 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/11527695_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Biere","year":"2005","unstructured":"Biere, A.: Resolve and expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"key":"4_CR17","unstructured":"Goldberg, E., Manolios, P.: Quantifier elimination by dependency sequents. In: Proceedings of the FMCAD 2012, pp. 34\u201343. IEEE Computer Society (2012)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"K\u00fcbler, A., Zengler, C., K\u00fcchlin, W.: Model counting in product configuration. In: Proceedings of the LoCoCo 2010. EPTCS, vol.\u00a029, pp. 44\u201353 (2010)","DOI":"10.4204\/EPTCS.29.5"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-36126-X_12","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Ayari","year":"2002","unstructured":"Ayari, A., Basin, D.: Qubos: Deciding quantified Boolean logic using propositional satisfiability solvers. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 187\u2013201. Springer, Heidelberg (2002)"},{"key":"4_CR20","unstructured":"Darwiche, A.: New advances in compiling CNF to decomposable negational normal form. In: Proceedings of the ECAI 2004. IOS Press (2004)"},{"key":"4_CR21","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1145\/2016567.2016595","volume":"45","author":"C. Zengler","year":"2011","unstructured":"Zengler, C., K\u00fcbler, A., K\u00fcchlin, W.: New approaches to boolean quantifier elimination. ACM Communications in Computer Algebra\u00a045, 139\u2013140 (2011)","journal-title":"ACM Communications in Computer Algebra"},{"key":"4_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/3-540-44652-4_17","volume-title":"Symbolic and Quantitative Approaches to Reasoning with Uncertainty","author":"A. Darwiche","year":"2001","unstructured":"Darwiche, A., Hopkins, M.: Using recursive decomposition to construct elimination orders, jointrees, and dtrees. In: Benferhat, S., Besnard, P. (eds.) ECSQARU 2001. LNCS (LNAI), vol.\u00a02143, pp. 180\u2013191. Springer, Heidelberg (2001)"},{"key":"4_CR23","unstructured":"Pipatsrisawat, K., Darwiche, A.: New compilation languages based on structured decomposability. In: Proceedings of the AAAI 2008, pp. 517\u2013522. AAAI Press (2008)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41010-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T06:28:47Z","timestamp":1558074527000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41010-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642410093","9783642410109"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41010-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}