{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T13:14:13Z","timestamp":1725974053583},"publisher-location":"Cham","reference-count":83,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319635156"},{"type":"electronic","value":"9783319635163"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-63516-3_3","type":"book-chapter","created":{"date-parts":[[2018,4,5]],"date-time":"2018-04-05T03:43:39Z","timestamp":1522899819000},"page":"61-99","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Parallel Maximum Satisfiability"],"prefix":"10.1007","author":[{"given":"In\u00eas","family":"Lynce","sequence":"first","affiliation":[]},{"given":"Vasco","family":"Manquinho","sequence":"additional","affiliation":[]},{"given":"Ruben","family":"Martins","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,4,6]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Ach\u00e1, R.J.A., Nieuwenhuis, R.: Curriculum-based course timetabling with SAT and MaxSAT. Annals of Operations Research 218(1), 71\u201391 (2014)","DOI":"10.1007\/s10479-012-1081-x"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"An, X., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: A Partial Max-SAT Solver. Journal on Satisfiability, Boolean Modeling and Computation 8, 95\u2013100 (2012)","DOI":"10.3233\/SAT190091"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Gab\u00e0s, J., Levy, J.: Improving WPM2 for (Weighted) Partial MaxSAT. In: Proc. International Conference on Principles and Practice of Constraint Programming, pp. 117\u2013132. Springer (2013)","DOI":"10.1007\/978-3-642-40627-0_12"},{"key":"3_CR4","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: On Solving MaxSAT Through SAT. In: Proc. International Conference of the Catalan Association for Artificial Intelligence, pp. 284\u2013292. IOS Press (2009)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: Solving (Weighted) Partial MaxSAT through Satisfiability Testing. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 427\u2013440. Springer (2009)","DOI":"10.1007\/978-3-642-02777-2_39"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: A New Algorithm for Weighted Partial MaxSAT. In: Proc. AAAI Conference on Artificial Intelligence, pp. 3\u20138. AAAI Press (2010)","DOI":"10.1609\/aaai.v24i1.7545"},{"key":"3_CR7","unstructured":"Ans\u00f3tegui, C., Gab\u00e0s, J.: Solving (Weighted) Partial MaxSAT with ILP. In: Proc. International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, pp. 403\u2013409. Springer (2013)"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Ans\u00f3tegui, C., Many\u00e0, F.: Mapping problems with finite-domain variables into problems with Boolean variables. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 1\u201315. Springer (2004)","DOI":"10.1007\/11527695_1"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Argelich, J., Berre, D.L., Lynce, I., Marques-Silva, J., Rapicault, P.: Solving Linux Upgradeability Problems Using Boolean Optimization. In: Workshop on Logics for Component Configuration, pp. 11\u201322. Conference Proceedings (2010)","DOI":"10.4204\/EPTCS.29.2"},{"key":"3_CR10","unstructured":"Argelich, J., Li, C.M., Many\u00e0, F.: An improved exact solver for Partial Max-SAT. In: Proc. of the International Conference on Nonconvex Programming: Local and Global Approaches, pp. 230\u2013231. Conference Proceedings (2007)"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Argelich, J., Many\u00e0, F.: Partial Max-SAT Solvers with Clause Learning. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 28\u201340. Springer (2007)","DOI":"10.1007\/978-3-540-72788-0_7"},{"key":"3_CR12","doi-asserted-by":"crossref","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)","DOI":"10.1007\/s10601-010-9105-0"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Audemard, G., Hoessen, B., Jabbour, S., Lagniez, J.M., Piette, C.: Revisiting Clause Exchange in Parallel SAT Solving. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 200\u2013213. Springer (2012)","DOI":"10.1007\/978-3-642-31612-8_16"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Audemard, G., Lagniez, J.M., Mazure, B., Sais, L.: On Freezing and Reactivating Learnt Clauses. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 188\u2013200. Springer (2011)","DOI":"10.1007\/978-3-642-21581-0_16"},{"key":"3_CR15","unstructured":"Audemard, G., Simon, L.: Predicting Learnt Clauses Quality in Modern SAT Solvers. In: Proc. International Joint Conferences on Artificial Intelligence, pp. 399\u2013404. IJCAI\/AAAI Press (2009)"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient CNF Encoding of Boolean Cardinality Constraints. In: Proc. International Conference on Principles and Practice of Constraint Programming, pp. 108\u2013122. Springer (2003)","DOI":"10.1007\/978-3-540-45193-8_8"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Bailleux, O., Boufkhad, Y., Roussel, O.: New Encodings of Pseudo-Boolean Constraints into CNF. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 181\u2013194. Springer (2009)","DOI":"10.1007\/978-3-642-02777-2_19"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Berre, D.L., Parrain, A.: The Sat4j library, release 2.2. JSAT 7(2-3), 59\u20136 (2010)","DOI":"10.3233\/SAT190075"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Phan, A., Fleckenstein, L.: $$ {\\nu Z} $$ - An Optimizing SMT Solver. In: Proc. Tools and Algorithms for Construction and Analysis of Systems, pp. 194\u2013199. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_14"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"B\u00f6hm, M., Speckenmeyer, E.: A Fast Parallel SAT-Solver - Efficient Workload Balancing. Annals of Mathematics and Artificial Intelligence 17, 381\u2013400 (1996)","DOI":"10.1007\/BF02127976"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Bonet, M.L., Levy, J., Many\u00e0, F.: Resolution for Max-SAT. Artificial Intelligence 171(8\u20139), 606\u2013618 (2007)","DOI":"10.1016\/j.artint.2007.03.001"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Chen, Y., Safarpour, S., Marques-Silva, J., Veneris, A.G.: Automated Design Debugging With Maximum Satisfiability. IEEE Transactions on CAD of Integrated Circuits and Systems 29(11), 1804\u20131817 (2010)","DOI":"10.1109\/TCAD.2010.2061270"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Darras, S., Dequen, G., Devendevill, L., Li, C.M.: On Inconsistent Clause-Subsets for Max-SAT Solving. In: Proc. International Conference on Principles and Practice of Constraint Programming, pp. 225\u2013240. Springer (2007)","DOI":"10.1007\/978-3-540-74970-7_18"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Davies, J., Bacchus, F.: Solving MAXSAT by Solving a Sequence of Simpler SAT Instances. In: Proc. International Conference on Principles and Practice of Constraint Programming, pp. 225\u2013239. Springer (2011)","DOI":"10.1007\/978-3-642-23786-7_19"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Davies, J., Bacchus, F.: Postponing optimization to speed up MAXSAT solving. In: Proc. International Conference on Principles and Practice of Constraint Programming, pp. 247\u2013262. Springer (2013)","DOI":"10.1007\/978-3-642-40627-0_21"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 502\u2013518. Springer (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science 89(4), 543\u2013560 (2003)","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation 2, 1\u201326 (2006)","DOI":"10.3233\/SAT190014"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Feng, Y., Bastani, O., Martins, R., Dillig, I., Anand, S.: Automated Synthesis of Semantic Malware Signatures using Maximum Satisfiability. In: Network and Distributed System Security Symposium. The Internet Society (2017)","DOI":"10.14722\/ndss.2017.23379"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Frisch, A.M., Peugniez, T.J., Doggett, A.J., Nightingale, P.: Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings. Journal of Automated Reasoning 35(1-3), 143\u2013179 (2005)","DOI":"10.1007\/s10817-005-9011-0"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 252\u2013265. Springer (2006)","DOI":"10.1007\/11814948_25"},{"key":"3_CR32","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman (1979)"},{"key":"3_CR33","unstructured":"Gent, I.P., Nightingale, P.: A new encoding of All Different into SAT. In: International Workshop on Modelling and Reformulating Constraint Satisfaction Problems. Conference Proceedings (2004)"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Gra\u00e7a, A., Lynce, I., Marques-Silva, J., Oliveira, A.L.: Efficient and Accurate Haplotype Inference by Combining Parsimony and Pedigree Information. In: Algebraic and Numeric Biology, pp. 38\u201356. Springer (2010)","DOI":"10.1007\/978-3-642-28067-2_3"},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"Hamadi, Y., Jabbour, S., Piette, C., Sais, L.: Deterministic Parallel DPLL. Journal on Satisfiability, Boolean Modeling and Computation 7(4), 127\u2013132 (2011)","DOI":"10.3233\/SAT190081"},{"key":"3_CR36","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: Control-Based Clause Sharing in Parallel SAT Solving. In: Proc. International Joint Conferences on Artificial Intelligence, pp. 499\u2013504. IJCAI\/AAAI Press (2009)"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a Parallel SAT Solver. Journal on Satisfiability, Boolean Modeling and Computation 6(4), 245\u2013262 (2009)","DOI":"10.3233\/SAT190070"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"Heras, F., Morgado, A., Marques-Silva, J.: Core-Guided Binary Search Algorithms for Maximum Satisfiability. In: Proc. AAAI Conference on Artificial Intelligence, pp. 36\u201341. AAAI Press (2011)","DOI":"10.1609\/aaai.v25i1.7822"},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Heule, M.J., Kullmann, O.,Wieringa, S., Biere, A.: Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. In: Hardware and Software: Verification and Testing, pp. 50\u201365. Springer (2012)","DOI":"10.1007\/978-3-642-34188-5_8"},{"key":"3_CR40","doi-asserted-by":"crossref","unstructured":"H\u00f6lldobler, S., Manthey, N., Steinke, P.: A compact encoding of pseudo-Boolean constraints into SAT. In: KI 2013: Advances in Artificial Intelligence, pp. 107\u2013118. Springer (2012)","DOI":"10.1007\/978-3-642-33347-7_10"},{"key":"3_CR41","doi-asserted-by":"crossref","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: Proc. Conference on Programming Language Design and Implementation, pp. 437\u2013446. ACM Press (2011)","DOI":"10.1145\/1993498.1993550"},{"key":"3_CR42","doi-asserted-by":"crossref","unstructured":"Joshi, S., Martins, R., Manquinho, V.: Generalized Totalizer Encoding for Pseudo-Boolean Constraints. In: International Conference on Principles and Practice of Constraint Programming, pp. 200\u2013209. Springer (2015)","DOI":"10.1007\/978-3-319-23219-5_15"},{"key":"3_CR43","unstructured":"Klieber, W., Kwon, G.: Efficient CNF Encoding for Selecting 1 from N Objects. In: International Workshop on Constraints in Formal Verification. Conference Proceedings (2007)"},{"key":"3_CR44","unstructured":"Li, C.M., Many\u00e0, F.: MaxSAT, Hard and Soft Constraints. In: Handbook of Satisfiability, pp. 613\u2013631. IOS Press (2009)"},{"key":"3_CR45","doi-asserted-by":"crossref","unstructured":"Li, C.M., Many\u00e0, F., Planes, J.: Exploiting unit propagation to compute lower bounds in branch and bound Max-SAT solvers. In: Proc. International Conference on Principles and Practice of Constraint Programming, pp. 403\u2013414. Springer (2005)","DOI":"10.1007\/11564751_31"},{"key":"3_CR46","doi-asserted-by":"crossref","unstructured":"Li, C.M., Many\u00e0, F., Planes, J.: New inference rules for Max-SAT. Journal of Artificial Intelligence Research 30, 321\u2013359 (2007)","DOI":"10.1613\/jair.2215"},{"key":"3_CR47","unstructured":"Lin, H., Su, K.: Exploiting inference rules to compute lower bounds for MAXSAT solving. In: Proc. International Joint Conferences on Artificial Intelligence, pp. 2334\u20132339. IJCAI\/AAAI Press (2007)"},{"key":"3_CR48","unstructured":"Lin, H., Su, K., Li, C.M.: Within-problem Learning for Efficient Lower Bound Computation in Max-SAT Solving. In: Proc. AAAI Conference on Artificial Intelligence, pp. 351\u2013356. AAAI Press (2008)"},{"key":"3_CR49","doi-asserted-by":"crossref","unstructured":"Mancinelli, F., Boender, J., Cosmo, R.D., Vouillon, J., Durak, B., Leroy, X., Treinen, R.: Managing the Complexity of Large Free and Open Source Package-Based Software Distributions. In: Proc. International Conference on Automated Software Engineering, pp. 199\u2013208. IEEE Computer Society Press (2006)","DOI":"10.1109\/ASE.2006.49"},{"key":"3_CR50","doi-asserted-by":"crossref","unstructured":"Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for Weighted Boolean Optimization. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 495\u2013508. Springer (2009)","DOI":"10.1007\/978-3-642-02777-2_45"},{"key":"3_CR51","doi-asserted-by":"crossref","unstructured":"Manquinho, V., Martins, R., Lynce, I.: Improving Unsatisfiability-Based Algorithms for Boolean Optimization. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 181\u2013193. Springer (2010)","DOI":"10.1007\/978-3-642-14186-7_16"},{"key":"3_CR52","unstructured":"Marques-Silva, J., Planes, J.: On using unsatisfiability for solving maximum satisfiability. CoRR. http:\/\/arXiv.org\/abs\/0712.1097 (2007)"},{"key":"3_CR53","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Sakallah, K.: GRASP: A New Search Algorithm for Satisfiability. In: Proc. International Conference on Computer-Aided Design, pp. 220\u2013227. IEEE Computer Society Press (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"3_CR54","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Sakallah, K.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions on Computers 48(5), 506\u2013521 (1999)","DOI":"10.1109\/12.769433"},{"key":"3_CR55","doi-asserted-by":"crossref","unstructured":"Martins, R., Joshi, S., Manquinho, V., Lynce, I.: Incremental Cardinality Constraints for MaxSAT. In: Proc. International Conference on Principles and Practice of Constraint Programming, pp. 531\u2013548. Springer (2014)","DOI":"10.1007\/978-3-319-10428-7_39"},{"key":"3_CR56","doi-asserted-by":"crossref","unstructured":"Martins, R., Joshi, S., Manquinho, V., Lynce, I.: On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving. Journal on Satisfiability, Boolean Modeling and Computation 9, 59\u201381 (2015)","DOI":"10.3233\/SAT190102"},{"key":"3_CR57","doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V., Lynce, I.: Exploiting Cardinality Encodings in Parallel Maximum Satisfiability. In: Proc. International Conference on Tools with Artificial Intelligence, pp. 313\u2013320. IEEE Computer Society Press (2011)","DOI":"10.1109\/ICTAI.2011.54"},{"key":"3_CR58","doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V., Lynce, I.: Clause Sharing in Deterministic Parallel Maximum Satisfiability. In: RCRA International Workshop on Experimental Evaluation of Algorithms for solving problems with combinatorial explosion. Conference Proceedings (2012)","DOI":"10.3233\/AIC-2012-0517"},{"key":"3_CR59","doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V., Lynce, I.: Clause Sharing in Parallel MaxSAT. In: Proc. Learning and Intelligent Optimization Conference, pp. 455\u2013460. Springer (2012)","DOI":"10.1007\/978-3-642-34413-8_44"},{"key":"3_CR60","unstructured":"Martins, R., Manquinho, V., Lynce, I.: On Partitioning for Maximum Satisfiability. In: Proc. European Conference on Artificial Intelligence, pp. 913\u2013914. IOS Press (2012)"},{"key":"3_CR61","doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V., Lynce, I.: Parallel Search for Maximum Satisfiability. AI Communications 25(2), 75\u201395 (2012)","DOI":"10.3233\/AIC-2012-0517"},{"key":"3_CR62","doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V., Lynce, I.: Community-based Partitioning for MaxSAT Solving. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 182\u2013191. Springer (2013)","DOI":"10.1007\/978-3-642-39071-5_14"},{"key":"3_CR63","doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V., Lynce, I.: Deterministic Parallel MaxSAT Solving. International Journal on Artificial Intelligence Tools 24(3) (2015)","DOI":"10.1142\/s0218213015500050"},{"key":"3_CR64","doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V.M., Lynce, I.: Open-WBO: A Modular MaxSAT Solver. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 438\u2013445. Springer (2014)","DOI":"10.1007\/978-3-319-09284-3_33"},{"key":"3_CR65","doi-asserted-by":"crossref","unstructured":"Morgado, A., Heras, F., Liffiton, M.H., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints 18(4), 478\u2013534 (2013)","DOI":"10.1007\/s10601-013-9146-2"},{"key":"3_CR66","doi-asserted-by":"crossref","unstructured":"Morgado, A., Ignatiev, A., Marques-Silva, J.: MSCG: Robust Core-Guided MaxSAT Solving. Journal on Satisfiability, Boolean Modeling and Computation 9, 129\u2013134 (2015)","DOI":"10.3233\/SAT190105"},{"key":"3_CR67","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Design Automation Conference, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"3_CR68","doi-asserted-by":"crossref","unstructured":"Narodytska, N., Bacchus, F.: Maximum Satisfiability Using Core-Guided MaxSAT Resolution. In: Proc. AAAI Conference on Artificial Intelligence, pp. 2717\u20132723. AAAI Press (2014)","DOI":"10.1609\/aaai.v28i1.9124"},{"key":"3_CR69","unstructured":"Neves, M., Lynce, I., Manquinho, V.: DistMS: A Non-Portfolio Distributed Solver for Maximum Satisfiability. In: Proc. International Conference on Tools with Artificial Intelligence. IEEE Computer Society Press (2016)"},{"key":"3_CR70","doi-asserted-by":"crossref","unstructured":"Neves, M., Martins, R., Janota, M., Lynce, I., Manquinho, V.M.: Exploiting resolution-based representations for MaxSAT solving. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 272\u2013286. Springer (2015)","DOI":"10.1007\/978-3-319-24318-4_20"},{"key":"3_CR71","doi-asserted-by":"crossref","unstructured":"Ogawa, T., Liu, Y., Hasegawa, R., Koshimura, M., Fujita, H.: Modulo Based CNF Encoding of Cardinality Constraints and Its Application to MaxSAT Solvers. In: Proc. International Conference on Tools with Artificial Intelligence, pp. 9\u201317. IEEE Computer Society (2013)","DOI":"10.1109\/ICTAI.2013.13"},{"key":"3_CR72","unstructured":"Papadimitriou, C.M.: Computational complexity. Addison-Wesley, Reading, Massachusetts (1994)"},{"key":"3_CR73","unstructured":"Plaza, S., Kountanis, I., Andraus, Z., Bertacco, V., Mudge, T.: Advances and Insights into Parallel SAT Solving. In: Internacional Workshop on Logic & Synthesis, pp. 188\u2013194. Conference Proceedings (2006)"},{"key":"3_CR74","doi-asserted-by":"crossref","unstructured":"Prestwich, S.: Variable Dependency in Local Search: Prevention is Better than Cure. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 107\u2013120. Springer (2007)","DOI":"10.1007\/978-3-540-72788-0_14"},{"key":"3_CR75","doi-asserted-by":"crossref","unstructured":"Saikko, P., Berg, J., J\u00e4rvisalo, M.: LMHS: A SAT-IP Hybrid MaxSAT Solver. In: Proc. International Conference on Theory and Applications of Satisfiability Testing, pp. 539\u2013546. Springer (2016)","DOI":"10.1007\/978-3-319-40970-2_34"},{"key":"3_CR76","doi-asserted-by":"crossref","unstructured":"Schubert, T., Lewis, M., Becker, B.: PaMira - A Parallel SAT Solver with Knowledge Sharing. In: Workshop on Microprocessor Test and Verification, pp. 29\u201336. Conference Proceedings (2005)","DOI":"10.1109\/MTV.2005.17"},{"key":"3_CR77","doi-asserted-by":"crossref","unstructured":"Schubert, T., Lewis, M., Becker, B.: PaMiraXT: Parallel SAT Solving with Threads and Message Passing. Journal on Satisfiability, Boolean Modeling and Computation 6, 203\u2013222 (2009)","DOI":"10.3233\/SAT190068"},{"key":"3_CR78","doi-asserted-by":"crossref","unstructured":"Singer, D., Monnet, A.: JaCk-SAT: A New Parallel Scheme to Solve the Satisfiability Problem (SAT) Based on Join-and-Check. In: Proc. Parallel Processing and Applied Mathematics, pp. 249\u2013258. Springer (2008)","DOI":"10.1007\/978-3-540-68111-3_27"},{"key":"3_CR79","doi-asserted-by":"crossref","unstructured":"Sinz, C.: Towards an Optimal CNF Encoding of Boolean Cardinality Constraints. In: Proc. International Conference on Principles and Practice of Constraint Programming, pp. 827\u2013831. Springer (2005)","DOI":"10.1007\/11564751_73"},{"key":"3_CR80","doi-asserted-by":"crossref","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: A Cross-Community Infrastructure for Logic Solving. In: Proc. International Joint Conference on Automated Reasoning, pp. 367\u2013373. Springer (2014)","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"3_CR81","doi-asserted-by":"crossref","unstructured":"Warners, J.P.: A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters 68(2), 63\u201369 (1998)","DOI":"10.1016\/S0020-0190(98)00144-6"},{"key":"3_CR82","doi-asserted-by":"crossref","unstructured":"Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: a Distributed Propositional Prover and Its Application to Quasigroup Problems. Journal of Symbolic Computation 21, 543\u2013560 (1996)","DOI":"10.1006\/jsco.1996.0030"},{"key":"3_CR83","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient Conflict Driven Learning in Boolean Satisfiability Solver. In: Proc. International Conference on Computer-Aided Design, pp. 279\u2013285. IEEE Computer Society Press (2001)"}],"container-title":["Handbook of Parallel Constraint Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63516-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T22:58:24Z","timestamp":1693609104000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63516-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319635156","9783319635163"],"references-count":83,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63516-3_3","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}