{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T08:39:18Z","timestamp":1726043958952},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030304454"},{"type":"electronic","value":"9783030304461"}],"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-30446-1_7","type":"book-chapter","created":{"date-parts":[[2019,9,8]],"date-time":"2019-09-08T19:03:18Z","timestamp":1567969398000},"page":"127-144","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["SAT Encodings of the At-Most-k Constraint"],"prefix":"10.1007","author":[{"ORCID":"http:\/\/orcid.org\/0000-0001-9388-0649","authenticated-orcid":false,"given":"Paul Maximilian","family":"Bittner","sequence":"first","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0001-8069-9584","authenticated-orcid":false,"given":"Thomas","family":"Th\u00fcm","sequence":"additional","affiliation":[]},{"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,9,9]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Apel, S., Batory, D., K\u00e4stner, C., Saake, G.: Feature-Oriented Software Product Lines (2013)","DOI":"10.1007\/978-3-642-37521-7"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-45193-8_8","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"O Bailleux","year":"2003","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of boolean cardinality constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 108\u2013122. Springer, Heidelberg (2003). \n https:\/\/doi.org\/10.1007\/978-3-540-45193-8_8"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/11554844_3","volume-title":"Software Product Lines","author":"D Batory","year":"2005","unstructured":"Batory, D.: Feature models, grammars, and propositional formulas. In: Obbink, H., Pohl, K. (eds.) SPLC 2005. LNCS, vol. 3714, pp. 7\u201320. Springer, Heidelberg (2005). \n https:\/\/doi.org\/10.1007\/11554844_3"},{"issue":"6","key":"7_CR4","doi-asserted-by":"publisher","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.: Automated analysis of feature models 20 years later: a literature review. Inf. Syst. 35(6), 615\u2013708 (2010)","journal-title":"Inf. Syst."},{"key":"7_CR5","unstructured":"Chen, J.: A new SAT encoding of the at-most-one constraint. In: Proceedings of the Constraint Modelling and Reformulation (2010)"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1002\/spip.213","volume":"10","author":"K Czarnecki","year":"2005","unstructured":"Czarnecki, K., Helsen, S., Eisenecker, U.: Formalizing cardinality-based feature models and their specialization. Softw. Process: Improv. Pract. 10, 7\u201329 (2005)","journal-title":"Softw. Process: Improv. Pract."},{"key":"7_CR7","unstructured":"Czarnecki, K., Kim, C.H.P.: Cardinality-based feature modeling and constraints: a progress report, pp. 16\u201320 (2005)"},{"key":"7_CR8","unstructured":"Frisch, A.M., Giannaros, P.A.: SAT encodings of the at-most-k constraint. some old, some new, some fast, some slow. In: Proceedings of the Ninth International Workshop of Constraint Modelling and Reformulation (2010)"},{"key":"7_CR9","unstructured":"Frisch, A.M., Peugniez, T.J.: Solving non-boolean satisfiability problems with stochastic local search. In: IJCAI, vol. 2001, pp. 282\u2013290 (2001)"},{"issue":"1\u20133","key":"7_CR10","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-005-9011-0","volume":"35","author":"AM Frisch","year":"2005","unstructured":"Frisch, A.M., Peugniez, T.J., Doggett, A.J., Nightingale, P.W.: Solving non-boolean satisfiability problems with stochastic local search: a comparison of encodings. J. Autom. Reason. 35(1\u20133), 143\u2013179 (2005). \n https:\/\/doi.org\/10.1007\/s10817-005-9011-0","journal-title":"J. Autom. Reason."},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"G\u00fcnther, T.: Explaining satisfiability queries for software product lines. Master\u2019s thesis, Braunschweig (2017). \n https:\/\/doi.org\/10.24355\/dbbs.084-201711171100\n \n . \n https:\/\/publikationsserver.tu-braunschweig.de\/receive\/dbbs_mods_00065308","DOI":"10.24355\/dbbs.084-201711171100"},{"key":"7_CR12","unstructured":"Klieber, W., Kwon, G.: Efficient CNF encoding for selecting 1 from n objects. In: Proceedings of the International Workshop on Constraints in Formal Verification (2007)"},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Krieter, S., et al.: FeatureIDE: empowering third-party developers, pp. 42\u201345 (2017). \n https:\/\/doi.org\/10.1145\/3109729.3109751","DOI":"10.1145\/3109729.3109751"},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"Krieter, S., Th\u00fcm, T., Schulze, S., Schr\u00f6ter, R., Saake, G.: Propagating configuration decisions with modal implication graphs, pp. 898\u2013909, May 2018. \n https:\/\/doi.org\/10.1145\/3180155.3180159","DOI":"10.1145\/3180155.3180159"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-319-66263-3_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"P Ku\u010dera","year":"2017","unstructured":"Ku\u010dera, P., Savick\u00fd, P., Vorel, V.: A lower bound on CNF encodings of the at-most-one constraint. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 412\u2013428. Springer, Cham (2017). \n https:\/\/doi.org\/10.1007\/978-3-319-66263-3_26"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Mannion, M.: Using first-order logic for product line model validation, pp. 176\u2013187 (2002)","DOI":"10.1007\/3-540-45652-X_11"},{"key":"7_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-61443-4","volume-title":"Mastering Software Variability with FeatureIDE","author":"J Meinicke","year":"2017","unstructured":"Meinicke, J., Th\u00fcm, T., Schr\u00f6ter, R., Benduhn, F., Leich, T., Saake, G.: Mastering Software Variability with FeatureIDE. Springer, Cham (2017). \n https:\/\/doi.org\/10.1007\/978-3-319-61443-4"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Mendon\u00e7a, M.: Efficient reasoning techniques for large scale feature models. Ph.D. thesis, University of Waterloo, Canada (2009)","DOI":"10.1145\/1449913.1449918"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/11564751_73","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"C Sinz","year":"2005","unstructured":"Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827\u2013831. Springer, Heidelberg (2005). \n https:\/\/doi.org\/10.1007\/11564751_73"},{"key":"7_CR20","unstructured":"Th\u00fcm, T., Apel, S., K\u00e4stner, C., Schaefer, I., Saake, G.: Analysis strategies for software product lines: a classification and survey, pp. 57\u201358, Gesellschaft f\u00fcr Informatik (GI), Bonn, Germany, March 2015"},{"issue":"2","key":"7_CR21","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1147\/sj.432.0371","volume":"43","author":"J Wiegand","year":"2004","unstructured":"Wiegand, J., et al.: Eclipse: a platform for integrating development tools. IBM Syst. J. 43(2), 371\u2013383 (2004)","journal-title":"IBM Syst. J."}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30446-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,8]],"date-time":"2019-09-08T19:41:22Z","timestamp":1567971682000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30446-1_7"}},"subtitle":["A Case Study on Configuring University Courses"],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030304454","9783030304461"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30446-1_7","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":"9 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oslo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Norway","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":"18 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 September 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sefm2019.inria.fr\/","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":"89","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":"27","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":"0","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)"}}]}}