{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T09:12:24Z","timestamp":1783674744952,"version":"3.55.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030518240","type":"print"},{"value":"9783030518257","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-51825-7_36","type":"book-chapter","created":{"date-parts":[[2020,6,30]],"date-time":"2020-06-30T23:00:13Z","timestamp":1593558013000},"page":"519-535","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Incremental Encoding of Pseudo-Boolean Goal Functions Based on Comparator Networks"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4190-3033","authenticated-orcid":false,"given":"Micha\u0142","family":"Karpi\u0144ski","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4734-1721","authenticated-orcid":false,"given":"Marek","family":"Piotr\u00f3w","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,6,26]]},"reference":[{"key":"36_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-40627-0_9","volume-title":"Principles and Practice of Constraint Programming","author":"I Ab\u00edo","year":"2013","unstructured":"Ab\u00edo, I., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: A parametric approach for smaller and better encodings of cardinality constraints. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 80\u201396. Springer, Heidelberg (2013). \n                  https:\/\/doi.org\/10.1007\/978-3-642-40627-0_9"},{"key":"36_CR2","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1613\/jair.3653","volume":"45","author":"I Ab\u00edo","year":"2012","unstructured":"Ab\u00edo, I., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Mayer-Eichberger, V.: A new look at bdds for pseudo-boolean constraints. J. Artif. Intell. Res. 45, 443\u2013480 (2012)","journal-title":"J. Artif. Intell. Res."},{"key":"36_CR3","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Generic ILP versus specialized 0\u20131 ILP: an update. In: Proceedings of the 2002 IEEE\/ACM International Conference on Computer-aided Design, pp. 450\u2013457. ACM (2002)","DOI":"10.1145\/774572.774638"},{"key":"36_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-02777-2_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"R As\u00edn","year":"2009","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Cardinality networks and their applications. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 167\u2013180. Springer, Heidelberg (2009). \n                  https:\/\/doi.org\/10.1007\/978-3-642-02777-2_18"},{"issue":"2","key":"36_CR5","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10601-010-9105-0","volume":"16","author":"R As\u00edn","year":"2011","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Cardinality networks: a theoretical and empirical study. Constraints 16(2), 195\u2013221 (2011)","journal-title":"Constraints"},{"key":"36_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-642-39071-5_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"G Audemard","year":"2013","unstructured":"Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309\u2013317. Springer, Heidelberg (2013). \n                  https:\/\/doi.org\/10.1007\/978-3-642-39071-5_23"},{"key":"36_CR7","doi-asserted-by":"publisher","first-page":"191","DOI":"10.3233\/SAT190021","volume":"2","author":"O Bailleux","year":"2006","unstructured":"Bailleux, O., Boufkhad, Y., Roussel, O.: A translation of pseudo-boolean constraints to SAT. J. Satisfiability Boolean Model. Comput. 2, 191\u2013200 (2006)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"36_CR8","doi-asserted-by":"crossref","unstructured":"Batcher, K.E.: Sorting networks and their applications. In: Proceedings of the 30 April\u20132 May 1968, Spring Joint Computer Conference, pp. 307\u2013314. ACM (1968)","DOI":"10.1145\/1468075.1468121"},{"key":"36_CR9","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Deciding CLU logic formulas via boolean and pseudo-boolean encodings. In: Proceedings of the International Workshop on Constraints in Formal Verification (CFV 2002). Citeseer (2002)"},{"key":"36_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-17511-4_10","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Codish","year":"2010","unstructured":"Codish, M., Zazon-Ivry, M.: Pairwise cardinality networks. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 154\u2013172. Springer, Heidelberg (2010). \n                  https:\/\/doi.org\/10.1007\/978-3-642-17511-4_10"},{"key":"36_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). \n                  https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"issue":"4","key":"36_CR12","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electron. Notes Theor. Comput. Sci. 89(4), 543\u2013560 (2003)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"36_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3233\/SAT190014","volume":"2","author":"N E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-boolean constraints into SAT. J. Satisfiability Boolean Model. Comput. 2, 1\u201326 (2006)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"36_CR14","doi-asserted-by":"crossref","unstructured":"Elffers, J., Nordstr\u00f6m, J.: Divide and conquer: towards faster pseudo-boolean solving. In: IJCAI, pp. 1291\u20131299 (2018)","DOI":"10.24963\/ijcai.2018\/180"},{"key":"36_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-030-24258-9_11","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","author":"R Hickey","year":"2019","unstructured":"Hickey, R., Bacchus, F.: Speeding up assumption-based SAT. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 164\u2013182. Springer, Cham (2019). \n                  https:\/\/doi.org\/10.1007\/978-3-030-24258-9_11"},{"key":"36_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-319-23219-5_16","volume-title":"Principles and Practice of Constraint Programming","author":"M Karpi\u0144ski","year":"2015","unstructured":"Karpi\u0144ski, M., Piotr\u00f3w, M.: Smaller selection networks for cardinality constraints encoding. In: Pesant, G. (ed.) CP 2015. LNCS, vol. 9255, pp. 210\u2013225. Springer, Cham (2015). \n                  https:\/\/doi.org\/10.1007\/978-3-319-23219-5_16"},{"key":"36_CR17","doi-asserted-by":"publisher","unstructured":"Karpi\u0144ski, M., Piotr\u00f3w, M.: Competitive sorter-based encoding of PB-constraints into SAT. In: Berre, D.L., J\u00e4rvisalo, M. (eds.) Proceedings of Pragmatics of SAT 2015 and 2018. EPiC Series in Computing, vol. 59, pp. 65\u201378. EasyChair (2019). \n                  https:\/\/doi.org\/10.29007\/hh3v\n                  \n                . \n                  https:\/\/easychair.org\/publications\/paper\/tsHw","DOI":"10.29007\/hh3v"},{"issue":"3\u20134","key":"36_CR18","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/s10601-019-09302-0","volume":"24","author":"M Karpi\u0144ski","year":"2019","unstructured":"Karpi\u0144ski, M., Piotr\u00f3w, M.: Encoding cardinality constraints using multiway merge selection networks. Constraints 24(3\u20134), 234\u2013251 (2019). \n                  https:\/\/doi.org\/10.1007\/s10601-019-09302-0","journal-title":"Constraints"},{"key":"36_CR19","unstructured":"Knuth, D.E.: The art of computer programming. In: Sorting and Searching, 2nd edn, vol. 3. Addison Wesley Longman Publishing Co., Inc., Redwood City (1998)"},{"key":"36_CR20","doi-asserted-by":"publisher","first-page":"95","DOI":"10.3233\/SAT190091","volume":"8","author":"M Koshimura","year":"2012","unstructured":"Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: a partial Max-SAT solver. J. Satisfiability Boolean Model. Comput. 8, 95\u2013100 (2012)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"issue":"2\u20133","key":"36_CR21","doi-asserted-by":"publisher","first-page":"59","DOI":"10.3233\/SAT190075","volume":"7","author":"D Le Berre","year":"2010","unstructured":"Le Berre, D., Parrain, A.: The sat4j library, release 2.2. J. Satisfiability Boolean Model. Comput. 7(2\u20133), 59\u201364 (2010)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"36_CR22","unstructured":"Manolios, P., Papavasileiou, V.: Pseudo-boolean solving by incremental translation to SAT. In: 2011 Formal Methods in Computer-Aided Design (FMCAD), pp. 41\u201345. IEEE (2011)"},{"key":"36_CR23","doi-asserted-by":"publisher","first-page":"103","DOI":"10.3233\/SAT190018","volume":"2","author":"VM Manquinho","year":"2006","unstructured":"Manquinho, V.M., Roussel, O.: The first evaluation of pseudo-boolean solvers (PB\u201905). J. Satisfiability Boolean Model. Comput. 2, 103\u2013143 (2006)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"issue":"1","key":"36_CR24","doi-asserted-by":"publisher","first-page":"59","DOI":"10.3233\/SAT190102","volume":"9","author":"R Martins","year":"2014","unstructured":"Martins, R., Joshi, S., Manquinho, V., Lynce, I.: On using incremental encodings in unsatisfiability-based MaxSAT solving. J. Satisfiability Boolean Model. Comput. 9(1), 59\u201381 (2014)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"36_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-31612-8_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A Nadel","year":"2012","unstructured":"Nadel, A., Ryvchin, V.: Efficient SAT solving under assumptions. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 242\u2013255. Springer, Heidelberg (2012). \n                  https:\/\/doi.org\/10.1007\/978-3-642-31612-8_19"},{"key":"36_CR26","unstructured":"Oh, C.: Improving SAT Solvers by Exploiting Empirical Characteristics of CDCL. Ph.D. thesis, New York University (2016)"},{"key":"36_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-319-94144-8_3","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"T Paxian","year":"2018","unstructured":"Paxian, T., Reimer, S., Becker, B.: Dynamic polynomial watchdog encoding for solving weighted MaxSAT. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 37\u201353. Springer, Cham (2018). \n                  https:\/\/doi.org\/10.1007\/978-3-319-94144-8_3"},{"key":"36_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/978-3-319-24318-4_2","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"T Philipp","year":"2015","unstructured":"Philipp, T., Steinke, P.: PBLib \u2013 a library for encoding pseudo-boolean constraints into CNF. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 9\u201316. Springer, Cham (2015). \n                  https:\/\/doi.org\/10.1007\/978-3-319-24318-4_2"},{"key":"36_CR29","first-page":"11","volume":"2019","author":"M Piotr\u00f3w","year":"2019","unstructured":"Piotr\u00f3w, M.: UWrMaxSAT-a new minisat+-based solver in maxsat evaluation 2019. MaxSAT Eval. 2019, 11 (2019)","journal-title":"MaxSAT Eval."},{"issue":"6","key":"36_CR30","doi-asserted-by":"publisher","first-page":"1121","DOI":"10.1587\/transinf.2014FOP0007","volume":"98","author":"M Sakai","year":"2015","unstructured":"Sakai, M., Nabeshima, H.: Construction of an ROBDD for a PB-constraint in band form and related techniques for PB-solvers. IEICE Trans. Inf. Syst. 98(6), 1121\u20131127 (2015)","journal-title":"IEICE Trans. Inf. Syst."},{"key":"36_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"746","DOI":"10.1007\/978-3-642-04244-7_58","volume-title":"Principles and Practice of Constraint Programming - CP 2009","author":"A Schutt","year":"2009","unstructured":"Schutt, A., Feydy, T., Stuckey, P.J., Wallace, M.G.: Why decomposition is not as bad as it sounds. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 746\u2013761. Springer, Heidelberg (2009). \n                  https:\/\/doi.org\/10.1007\/978-3-642-04244-7_58"},{"key":"36_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/3-540-44798-9_4","volume-title":"Correct Hardware Design and Verification Methods","author":"O Shtrichman","year":"2001","unstructured":"Shtrichman, O.: Pruning techniques for the SAT-based bounded model checking problem. In: Margaria, T., Melham, T. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 58\u201370. Springer, Heidelberg (2001). \n                  https:\/\/doi.org\/10.1007\/3-540-44798-9_4"},{"key":"36_CR33","doi-asserted-by":"crossref","unstructured":"Whittemore, J., Kim, J., Sakallah, K.: Satire: a new incremental satisfiability engine. In: Proceedings of the 38th annual Design Automation Conference, pp. 542\u2013545. ACM (2001)","DOI":"10.1145\/378239.379019"},{"issue":"2","key":"36_CR34","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s10601-018-9299-0","volume":"24","author":"A Zha","year":"2019","unstructured":"Zha, A., Koshimura, M., Fujita, H.: N-level modulo-based CNF encodings of pseudo-boolean constraints for MaxSAT. Constraints 24(2), 133\u2013161 (2019)","journal-title":"Constraints"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2020"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-51825-7_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,7]],"date-time":"2020-08-07T23:09:05Z","timestamp":1596841745000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-51825-7_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030518240","9783030518257"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-51825-7_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"26 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Alghero","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sat2020.idea-researchlab.org\/","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":"69","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":"25","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":"9","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":"36% - 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)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}