{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T05:59:34Z","timestamp":1775714374422,"version":"3.50.1"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,7,12]],"date-time":"2016-07-12T00:00:00Z","timestamp":1468281600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Intell Inf Syst"],"published-print":{"date-parts":[[2017,8]]},"DOI":"10.1007\/s10844-016-0422-7","type":"journal-article","created":{"date-parts":[[2016,7,12]],"date-time":"2016-07-12T03:19:47Z","timestamp":1468293587000},"page":"87-118","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Constraint-based and SAT-based diagnosis of automotive configuration problems"],"prefix":"10.1007","volume":"49","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5626-6615","authenticated-orcid":false,"given":"Rouven","family":"Walter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Felfernig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"K\u00fcchlin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,7,12]]},"reference":[{"key":"422_CR1","doi-asserted-by":"crossref","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., & Levy, J. (2009). Solving (weighted) partial MaxSAT through satisfiability testing, In Kullmann, O. (Ed.) SAT 2009, LNCS, vol. 5584, pp. 427\u2013440. Springer Berlin Heidelberg.","DOI":"10.1007\/978-3-642-02777-2_39"},{"key":"422_CR2","unstructured":"Ans\u00f3tegui, C., & Gab\u00e0s, J. (2013). Solving (weighted) partial MaxSAT with ILP, In Gomes, C.P., & Sellmann, M. (Eds.) CPAIOR 2013, LNCS, vol. 7874, pp. 403\u2013409. Springer."},{"key":"422_CR3","unstructured":"Argelich, J., Lynce, I., & Marques-Silva, J. (2009). On solving boolean multilevel optimization problems, In Boutilier, C. (Ed.) IJCAI 2009, pp. 393\u2013398."},{"issue":"4\u20135","key":"422_CR4","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/s10732-006-7234-9","volume":"12","author":"J Argelich","year":"2006","unstructured":"Argelich, J., & Many\u00e0, F. (2006). Exact Max-SAT solvers for over-constrained problems. J Heuristics, 12(4\u20135), 375\u2013392.","journal-title":"J Heuristics"},{"key":"422_CR5","doi-asserted-by":"crossref","unstructured":"Audemard, G., Lagniez, J., & Simon, L. (2013). Improving glucose for incremental SAT solving with assumptions: Application to MUS extraction, In J\u00e4rvisalo, M., & Gelder, A.V. (Eds.) SAT 2013, LNCS, vol. 7962, pp. 309\u2013317. Springer.","DOI":"10.1007\/978-3-642-39071-5_23"},{"issue":"6","key":"422_CR6","doi-asserted-by":"crossref","first-page":"615","DOI":"10.1016\/j.is.2010.01.001","volume":"35","author":"D Benavides","year":"2010","unstructured":"Benavides, D., Segura, S., & Ruiz-Cort\u00e9s, A. (2010). Automated analysis of feature models 20 years later: A literature review. Information Systems, 35(6), 615\u2013636.","journal-title":"Information Systems"},{"issue":"2\u20134","key":"422_CR7","first-page":"75","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A. (2008). PicoSAT essentials. JSAT, 4(2\u20134), 75\u201397.","journal-title":"JSAT"},{"issue":"2","key":"422_CR8","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1006\/inco.1995.1087","volume":"119","author":"Z Chen","year":"1995","unstructured":"Chen, Z., & Toda, S. (1995). The complexity of selecting maximal solutions. Inform. Comput, 119(2), 231\u2013239.","journal-title":"Inform. Comput"},{"key":"422_CR9","doi-asserted-by":"crossref","unstructured":"Cook, S.A. (1971). The complexity of theorem-proving procedures, In Harrison, M.A., Banerji, R.B., & Ullman, J.D. (Eds.) STOC, pp. 151\u2013158. ACM.","DOI":"10.1145\/800157.805047"},{"key":"422_CR10","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., & S\u00f6rensson, N. (2004). An extensible SAT-solver, In Giunchiglia, E., & Tacchella, A. (Eds.) SAT 2003, LNCS, vol. 2919, pp. 502\u2013518. Springer Berlin Heidelberg.","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"422_CR11","first-page":"1","volume":"2","author":"N E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., & S\u00f6rensson, N. (2006). Translating pseudo-boolean constraints into SAT. JSAT, 2, 1\u201326.","journal-title":"JSAT"},{"issue":"1","key":"422_CR12","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1017\/S0890060411000011","volume":"26","author":"A Felfernig","year":"2012","unstructured":"Felfernig, A., Schubert, M., & Zehentner, C. (2012). An efficient diagnosis algorithm for inconsistent constraint sets. AIEDAM, 26(1), 53\u201362.","journal-title":"AIEDAM"},{"key":"422_CR13","unstructured":"Franco, J., & Martin, J. (2009). A history of satisfiability, In Biere, A., Heule, M., van Maaren, H., & Walsh, T. (Eds.) Handproceedings of Satisfiability, FAIA, vol. 185, chap. 1, pp. 3\u201374. IOS Press."},{"key":"422_CR14","doi-asserted-by":"crossref","unstructured":"Fu, Z., & Malik, S. (2006). On solving the partial MAX-SAT problem, In Biere, A., & Gomes, C.P. (Eds.) SAT 2006, LNCS, vol. 4121, pp. 252\u2013265. Springer.","DOI":"10.1007\/11814948_25"},{"issue":"2","key":"422_CR15","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/0004-3702(93)90069-N","volume":"61","author":"G Gottlob","year":"1993","unstructured":"Gottlob, G., & Ferm\u00fcller, C.G. (1993). Removing redundancy from a clause. Artif. Intell, 61(2), 263\u2013289.","journal-title":"Artif. Intell"},{"key":"422_CR16","doi-asserted-by":"crossref","unstructured":"Heras, F., Morgado, A., & Marques-Silva, J. (2011). Core-guided binary search algorithms for maximum satisfiability. In Burgard, W., & Roth, D. (Eds.) AAAI, pp. 36\u201341. AAAI Press.","DOI":"10.1609\/aaai.v25i1.7822"},{"key":"422_CR17","doi-asserted-by":"crossref","unstructured":"Heras, F., Morgado, A., & Marques-Silva, J. (2012). An empirical study of encodings for group MaxSAT. In Kosseim, L., & Inkpen, D. (Eds.) Canadian Conf. on AI, LNCS, vol. 7310, pp. 85\u201396. Springer.","DOI":"10.1007\/978-3-642-30353-1_8"},{"key":"422_CR18","doi-asserted-by":"crossref","unstructured":"Heras, F., Morgado, A., & Marques-Silva, J. (2012). Lower bounds and upper bounds for MaxSAT. In Hamadi, Y., & Schoenauer, M. (Eds.) LION 6, LNCS, vol. 7219, pp. 402\u2013407. Springer Berlin Heidelberg.","DOI":"10.1007\/978-3-642-34413-8_35"},{"issue":"1\u20132","key":"422_CR19","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/0304-3975(94)00080-3","volume":"141","author":"B Jenner","year":"1995","unstructured":"Jenner, B., & Tor\u00e1n, J. (1995). Computing functions with parallel queries to NP. Theoretical Computer Science, 141(1\u20132), 175\u2013193.","journal-title":"Theoretical Computer Science"},{"key":"422_CR20","unstructured":"Junker, U. (2004). QUICKXPLAIN: Preferred explanations and relaxations for over-constrained problems, In AAAI, pp. 167\u2013172. AAAI Press \/ The MIT Press."},{"issue":"3","key":"422_CR21","doi-asserted-by":"crossref","first-page":"490","DOI":"10.1016\/0022-0000(88)90039-6","volume":"36","author":"MW Krentel","year":"1988","unstructured":"Krentel, M.W. (1988). The complexity of optimization problems. J. Comput. System Sci, 36(3), 490\u2013509.","journal-title":"J. Comput. System Sci"},{"issue":"1\u20132","key":"422_CR22","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1023\/A:1006370506164","volume":"24","author":"W K\u00fcchlin","year":"2000","unstructured":"K\u00fcchlin, W., & Sinz, C. (2000). Proving consistency assertions for automotive product data management. J. Automat. Reason, 24(1\u20132), 145\u2013163.","journal-title":"J. Automat. Reason"},{"key":"422_CR23","unstructured":"K\u00fcgel, A. (2012). Improved exact solver for the weighted MAX-SAT problem, In Berre, D.L. (Ed.) POS-10. Pragmatics of SAT, EasyChair Proceedings in Computing, vol. 8, pp. 15\u201327. EasyChair."},{"issue":"2\u20133","key":"422_CR24","first-page":"59","volume":"7","author":"D Le Berre","year":"2010","unstructured":"Le Berre, D., & Parrain, A. (2010). The Sat4j library, release 2.2. JSAT, 7(2\u20133), 59\u20136.","journal-title":"JSAT"},{"key":"422_CR25","unstructured":"Li, C.M., & Many\u00e0, F. (2009). MaxSAT, hard and soft constraints, In Biere, A., Heule, M., van Maaren, H., & Walsh, T. (Eds.) Handproceedings of Satisfiability, FAIA, vol. 185, chap. 19, pp. 613\u2013631. IOS Press."},{"issue":"1","key":"422_CR26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton, M.H., & Sakallah, K.A. (2008). Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning, 40(1), 1\u201333.","journal-title":"J. Autom. Reasoning"},{"key":"422_CR27","unstructured":"Marques-Silva, J., Heras, F., Janota, M., Previti, A., & Belov, A. (2013). On computing minimal correction subsets, In Rossi, F. (Ed.) IJCAI, pp. 615\u2013622, IJCAI\/AAAI."},{"key":"422_CR28","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., & Previti, A. (2014). On computing preferred MUSes and MCSes, In Sinz, C., & Egly, U. (Eds.) SAT 2014, LNCS, vol. 8561, pp. 58\u201374. Springer.","DOI":"10.1007\/978-3-319-09284-3_6"},{"key":"422_CR29","doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V.M., & Lynce, I. (2014). Open-WBO: A modular MaxSAT solver, In Sinz, C., & Egly, U. (Eds.) SAT 2014, LNCS, vol. 8561, pp. 438\u2013445. Springer Int. Publishing.","DOI":"10.1007\/978-3-319-09284-3_33"},{"key":"422_CR30","doi-asserted-by":"crossref","unstructured":"Menc\u00eda, C., & Marques-Silva, J. (2014). Efficient relaxations of over-constrained CSPs, In ICTAI 2014, pp. 725\u2013732. IEEE.","DOI":"10.1109\/ICTAI.2014.113"},{"issue":"4","key":"422_CR31","doi-asserted-by":"crossref","first-page":"478","DOI":"10.1007\/s10601-013-9146-2","volume":"18","author":"A Morgado","year":"2013","unstructured":"Morgado, A., Heras, F., Liffiton, M.H., Planes, J., & Marques-Silva, J. (2013). Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints, 18 (4), 478\u2013534.","journal-title":"Constraints"},{"key":"422_CR32","unstructured":"Narodytska, N., & Bacchus, F. (2014). Maximum satisfiability using core-guided maxsat resolution, In Brodley, C.E., & Stone, P. (Eds.) AAAI, pp. 2717\u20132723. AAAI Press."},{"key":"422_CR33","unstructured":"O\u2019Callaghan, B., O\u2019Sullivan, B., & Freuder, E.C. (2005). Generating corrective explanations for interactive constraint satisfaction, In van Beek, P. (Ed.) CP 2005, LNCS, vol. 3709, pp. 445\u2013459. Springer."},{"key":"422_CR34","unstructured":"Papadimitriou, C.M. (1994). Computational complexity. Addison-Wesley. Massachusetts: Reading."},{"issue":"3","key":"422_CR35","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"DA Plaisted","year":"1986","unstructured":"Plaisted, D.A., & Greenbaum, S. (1986). A structure-preserving clause form translation. J. Symbolic Comput, 2(3), 293\u2013304.","journal-title":"J. Symbolic Comput"},{"key":"422_CR36","unstructured":"Schrijver, A. (1998). Theory of linear and integer programming: Wiley-Interscience."},{"issue":"2","key":"422_CR37","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1016\/S0022-0000(05)80009-1","volume":"48","author":"AL Selman","year":"1994","unstructured":"Selman, A.L. (1994). A taxonomy of complexity classes of functions. J. Comput. Syst. Sci, 48(2), 357\u2013381.","journal-title":"J. Comput. Syst. Sci"},{"key":"422_CR38","unstructured":"Sinz, C. (2005). Towards an optimal CNF encoding of boolean cardinality constraints, In van Beek, P. (Ed.) CP 2005, LNCS, vol. 3709, pp. 827\u2013831. Springer."},{"issue":"1","key":"422_CR39","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1017\/S0890060403171065","volume":"17","author":"C Sinz","year":"2003","unstructured":"Sinz, C., Kaiser, A., & K\u00fcchlin, W. (2003). Formal methods for the validation of automotive product configuration data. AIEDAM, 17(1), 75\u201397.","journal-title":"AIEDAM"},{"key":"422_CR40","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S. (1970). On the complexity of derivations in the propositional calculus. Studies in Constructive Mathematics and Mathematical Logic Part II, 115\u2013125.","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"422_CR41","unstructured":"Walter, R., Felfernig, A., & K\u00fcchlin, W. (2015). Inverse QuickXPlain vs. MaxSAT \u2014 a comparison in theory and practice. In Tiihonen, J., Falkner, A., & Axling, T. (Eds.) Proc. of the 17th Int. Config. Workshop, pp. 97\u2013104. Vienna, Austria."},{"key":"422_CR42","unstructured":"Walter, R., & K\u00fcchlin, W. (2014). ReMax \u2013 a MaxSAT aided product configurator, In Felfernig, A., Forza, C., & Haag, A. (Eds.) Proc. of the 16th Int. Config. Workshop, pp. 59\u201366. Novi Sad, Serbia."},{"key":"422_CR43","unstructured":"Walter, R., Zengler, C., & K\u00fcchlin, W. (2013). Applications of MaxSAT in automotive configuration, In Aldanondo, M., & Falkner, A. (Eds.) Proc. of the 15th Int. Config. Workshop, pp. 21\u201328. Vienna, Austria."},{"issue":"2","key":"422_CR44","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0020-0190(98)00144-6","volume":"68","author":"JP Warners","year":"1998","unstructured":"Warners, J.P. (1998). A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters, 68(2), 63\u201369.","journal-title":"Information Processing Letters"}],"container-title":["Journal of Intelligent Information Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10844-016-0422-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10844-016-0422-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10844-016-0422-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10844-016-0422-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,19]],"date-time":"2023-08-19T05:32:57Z","timestamp":1692423177000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10844-016-0422-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,7,12]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,8]]}},"alternative-id":["422"],"URL":"https:\/\/doi.org\/10.1007\/s10844-016-0422-7","relation":{},"ISSN":["0925-9902","1573-7675"],"issn-type":[{"value":"0925-9902","type":"print"},{"value":"1573-7675","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,7,12]]}}}