{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:15:31Z","timestamp":1762100131909},"reference-count":38,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2003,8,7]],"date-time":"2003-08-07T00:00:00Z","timestamp":1060214400000},"content-version":"unspecified","delay-in-days":187,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIEDAM"],"published-print":{"date-parts":[[2003,2]]},"abstract":"<jats:p>In the automotive industry, the compilation and maintenance of correct product configuration data is a complex task. Our work shows how formal methods can be applied to the validation of such business critical data. Our consistency support tool BIS works on an existing database of Boolean constraints expressing valid configurations and their transformation into manufacturable products. Using a specially modified satisfiability checker with an explanation component, BIS can detect inconsistencies in the constraints set and thus help increase the quality of the product data. BIS also supports manufacturing decisions by calculating the implications of product or production environment changes on the set of required parts. In this paper, we give a comprehensive account of BIS: the formalization of the business processes underlying its construction, the modifications of satisfiability-checking technology we found necessary in this context, and the software technology used to package the product as a client\u2013server information system.<\/jats:p>","DOI":"10.1017\/s0890060403171065","type":"journal-article","created":{"date-parts":[[2003,11,3]],"date-time":"2003-11-03T15:07:27Z","timestamp":1067872047000},"page":"75-97","source":"Crossref","is-referenced-by-count":54,"title":["Formal methods for the validation of automotive product configuration data"],"prefix":"10.1017","volume":"17","author":[{"given":"CARSTEN","family":"SINZ","sequence":"first","affiliation":[]},{"given":"ANDREAS","family":"KAISER","sequence":"additional","affiliation":[]},{"given":"WOLFGANG","family":"K\u00dcCHLIN","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2003,8,7]]},"reference":[{"key":"S0890060403171065_ref007","doi-asserted-by":"crossref","unstructured":"Davis, M. & Putnam, H. (1960).A computing procedure for quantification theory.Journal of the ACM 7,201\u2013215.","DOI":"10.1145\/321033.321034"},{"key":"S0890060403171065_ref021","doi-asserted-by":"crossref","unstructured":"McDermott, J. (1982).R1: A rule-based configurer of computer systems.Artificial Intelligence 19(1),39\u201388.","DOI":"10.1016\/0004-3702(82)90021-2"},{"key":"S0890060403171065_ref020","doi-asserted-by":"crossref","unstructured":"Kullmann, O. (2000).An application of matroid theory to the SAT problem.Proc. 15th IEEE Conf. Computational Complexity\u2014CCC 2000, pp.116\u2013124,Florence, Italy.","DOI":"10.1109\/CCC.2000.856741"},{"key":"S0890060403171065_ref003","unstructured":"Blochinger, W. , Sinz, C. , & K\u00fcchlin, W. (2001).Parallel consistency checking of automotive product data.Proc. Int. Conf. Parallel Computing (ParCo 2001),Naples, Italy."},{"key":"S0890060403171065_ref016","unstructured":"Kaiser, A. & K\u00fcchlin, W. (2001a).Detecting inadmissible and necessary variables in largepropositional formulae.Proc. Intl. Joint Conf. Automated Reasoning: IJCAR 2001\u2014ShortPapers, pp.96\u2013102.Technical Report DII, 11\/01.University of Siena."},{"key":"S0890060403171065_ref005","doi-asserted-by":"crossref","unstructured":"Craigen, D. , Gerhart, S. , & Ralston, T. (1995).Formal methods reality check: Industrial usage.IEEE Transaction on Software Engineering 21(2),90\u201398.","DOI":"10.1109\/32.345825"},{"key":"S0890060403171065_ref014","doi-asserted-by":"crossref","unstructured":"Hooker, J. & Vinay, V. (1995).Branching rules for satisfiability.Journal of Automated Reasoning 15(3),359\u2013383.","DOI":"10.1007\/BF00881805"},{"key":"S0890060403171065_ref034","doi-asserted-by":"crossref","unstructured":"Waldinger, R.J. & Stickel, M.E. (1992).Proving properties of rule based systems.International Journal of Software Engineering and KnowledgeEngineering 2(1),121\u2013144.","DOI":"10.1142\/S0218194092000075"},{"key":"S0890060403171065_ref033","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S. (1970).On the complexity of derivation in propositional calculus. InStudies in Constructive Mathematics and Mathematical Logic( Silenko, A.O. , Ed.), pp.115\u2013125.Leningrad:V.A. Steklov Mathematical Institute.","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"S0890060403171065_ref028","unstructured":"Sinz, C. (1997).Baubarkeitspr\u00fcfung von Kraftfahrzeugen durch automatischesBeweisen.Diplomarbeit,Universit\u00e4t T\u00fcbingen."},{"key":"S0890060403171065_ref008","doi-asserted-by":"crossref","unstructured":"Davydov, D. , Davydova, I. , & Kleine B\u00fcning, H. (1998).An efficient algorithm for the minimal unsatisfiability problem fora subclass of CNF.Annals of Mathematics and Artificial Intelligence 23,229\u2013245.","DOI":"10.1023\/A:1018924526592"},{"key":"S0890060403171065_ref032","unstructured":"Timmermans, P. (1999).The business challenge of configuration. InConfiguration( Faltings, B. , Freuder, E. , Friedrich, G. & Felfernig, A. , Eds.), pp.119\u2013122.Workshop Technical Report WS-99-05. Menlo Park, CA:AAAI Press."},{"key":"S0890060403171065_ref026","doi-asserted-by":"crossref","unstructured":"Saiedian, H. (1996).An invitation to formal methods.IEEE Computer 29(4),16\u201317.","DOI":"10.1109\/MC.1996.488298"},{"key":"S0890060403171065_ref031","unstructured":"Somenzi, F. (1998).CUDD: CU Decision Diagram Package, Release 2.3.0.University of Colorado,Boulder.Available online athttp:\/\/vlsi.colorado.edu\/\u223cfabio."},{"key":"S0890060403171065_ref025","doi-asserted-by":"crossref","unstructured":"Sabin, D. & Weigel, R. (1998).Product configuration frameworks\u2014A survey.IEEE Intelligent Systems 13(4),42\u201349.","DOI":"10.1109\/5254.708432"},{"key":"S0890060403171065_ref022","doi-asserted-by":"crossref","unstructured":"Moskewicz, M. , Madigan, C. , Zhao, Y. , Zhang, L. , & Malik, S. (2001).Chaff: Engineering an efficient SAT solver.Proc. 38th Design Automation Conf. (DAC 2001), pp.530\u2013535.New York:ACM.","DOI":"10.1145\/378239.379017"},{"key":"S0890060403171065_ref038","doi-asserted-by":"crossref","unstructured":"Zhang, H. (1997).SATO: An efficient propositional prover.Proc. 14th Int. Conf. on Automated Deduction (CADE-97), pp.272\u2013275.Lecture Notes in Computer Science, No. 1249. New York:Springer\u2013Verlag.","DOI":"10.1007\/3-540-63104-6_28"},{"key":"S0890060403171065_ref011","doi-asserted-by":"crossref","unstructured":"G\u00fcnter, A. & K\u00fchn, C. (1999).Knowledge-based configuration: Survey and future directions.LNAI 1570,47\u201366.","DOI":"10.1007\/10703016_3"},{"key":"S0890060403171065_ref002","unstructured":"Bayardo, R.J. & Schrag, R.C. (1997).Using CSP look-back techniques to solve real-world SAT instances.AAAI'97: Proc. Fourteenth National Conf. ArtificialIntelligence."},{"key":"S0890060403171065_ref004","unstructured":"CORBA .(1995).The Common Object Request Broker: Architecture and Specification.Needham, MA:Object Management Group."},{"key":"S0890060403171065_ref027","doi-asserted-by":"crossref","unstructured":"Silva, J.P.M. & Sakallah, K.A. (1999).GRASP\u2014A new search algorithm for satisfiability.IEEE Transactions on Computers 48(5),506\u2013521.","DOI":"10.1109\/12.769433"},{"key":"S0890060403171065_ref017","unstructured":"Kaiser, A. & K\u00fcchlin, W. (2001b).Explaining inconsistencies in combinatorial automotive productdata.Proc. 2nd Int. Conf. Intelligent Technologies (InTech 2001), pp.198\u2013204.Assumption University,Bangkok, Thailand."},{"key":"S0890060403171065_ref001","doi-asserted-by":"crossref","unstructured":"Barker, V. & O'Connor, D. (1989).Expert systems for configuration at Digital: XCON and beyond.Communications of the ACM 32(3),298\u2013318.","DOI":"10.1145\/62065.62067"},{"key":"S0890060403171065_ref024","doi-asserted-by":"crossref","unstructured":"Robinson, J.A. (1965).A machine-oriented logic based on the resolution principle.Journal of the ACM 12,23\u201341.","DOI":"10.1145\/321250.321253"},{"key":"S0890060403171065_ref037","unstructured":"Wright, J.R. , Weixelbaum, E. , Vesonder, G.T. , Brown, K.E. , Palmer, S.R. , Berman, J.I. , & Moore, H.H. (1993).A knowledge-based configurator that supports sales, engineering,and manufacturing at AT&T Network Systems.AI Magazine 14(3),69\u201380."},{"key":"S0890060403171065_ref018","unstructured":"Kleine B\u00fcning, H. & Xishun, Z. (1998).On the structure of some classes of minimal unsatisfiableformulas.Proc. 5th Int. Symp. Artificial Intelligence and Mathematics,Fort Lauderdale, FL."},{"key":"S0890060403171065_ref035","doi-asserted-by":"crossref","unstructured":"Wing, J. (1990).A specifier's introduction to formal methods.IEEE Computer 23(9),8\u201324.","DOI":"10.1109\/2.58215"},{"key":"S0890060403171065_ref010","unstructured":"Gerhart, S. (1990).Applications of formal methods: Developing virtuoso software.IEEE Software 7(5),7\u201310."},{"key":"S0890060403171065_ref015","unstructured":"Kaiser, A. (2001).A SAT-based Propositional Prover for Consistency Checking ofAutomotive Product Data.Technical Report WSI-2001-16.T\u00fcbingen, Germany:Wilhelm-Schickard-Institut f\u00fcr Informatik,Eberhard-Karls-Universit\u00e4t T\u00fcbingen."},{"key":"S0890060403171065_ref029","unstructured":"Sinz, C. & K\u00fcchlin, W. (2001).Dealing with temporal change in product documentation formanufacturing.Configuration Workshop Proc., 17th Int. Joint Conf. ArtificialIntelligence (IJCAI-2001), pp.71\u201377,Seattle, WA."},{"key":"S0890060403171065_ref019","doi-asserted-by":"crossref","unstructured":"K\u00fcchlin, W. & Sinz, C. (2000).Proving consistency assertions for automotive product datamanagement.Journal of Automated Reasoning 24(1\u20132),145\u2013163.","DOI":"10.1023\/A:1006370506164"},{"key":"S0890060403171065_ref030","unstructured":"Soininen, T. , Niemel\u00e4, I. , Tiihonen, J. , & Sulonen, R. (2001).Representing configuration knowledge with weight constraint rules.Answer Set Programming: Towards Efficient and Scalable KnowledgeRepresentation and Reasoning, 2001 AAAI Spring Symposium, pp.195\u2013201.Menlo Park, CA:AAAI Press."},{"key":"S0890060403171065_ref023","doi-asserted-by":"crossref","unstructured":"Papadimitriou, C.H. & Wolfe, D. (1988).The complexity of facets resolved.Journal of Computer and System Sciences 37,2\u201313.","DOI":"10.1016\/0022-0000(88)90042-6"},{"key":"S0890060403171065_ref012","doi-asserted-by":"crossref","unstructured":"Haag, A. (1998).Sales configuration in business processes.IEEE Intelligent Systems 13(4),78\u201385.","DOI":"10.1109\/5254.708436"},{"key":"S0890060403171065_ref013","doi-asserted-by":"crossref","unstructured":"Hall, A. (1990).Seven myths of formal methods.IEEE Software 7(5),11\u201319.","DOI":"10.1109\/52.57887"},{"key":"S0890060403171065_ref009","doi-asserted-by":"crossref","unstructured":"Freuder, E. (1998).The role of configuration knowledge in the business process.IEEE Intelligent Systems 13(4),29\u201331.","DOI":"10.1109\/MIS.1998.708429"},{"key":"S0890060403171065_ref006","doi-asserted-by":"crossref","unstructured":"Davis, M. , Logemann, G. , & Loveland, D. (1962).A machine program for theorem-proving.Communications of the ACM 5,394\u2013397.","DOI":"10.1145\/368273.368557"},{"key":"S0890060403171065_ref036","doi-asserted-by":"crossref","unstructured":"Wing, J. & Woodcock, J. (2000).Special issues for FM'99: The First World Congress on FormalMethods in the Development of Computing Systems.IEEE Transactions in Software Engineering 26(8),673\u2013674.","DOI":"10.1109\/TSE.2000.879806"}],"container-title":["Artificial Intelligence for Engineering Design, Analysis and Manufacturing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0890060403171065","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,26]],"date-time":"2020-03-26T14:17:19Z","timestamp":1585232239000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0890060403171065\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,2]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,2]]}},"alternative-id":["S0890060403171065"],"URL":"https:\/\/doi.org\/10.1017\/s0890060403171065","relation":{},"ISSN":["0890-0604","1469-1760"],"issn-type":[{"value":"0890-0604","type":"print"},{"value":"1469-1760","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,2]]}}}