{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,31]],"date-time":"2026-01-31T17:44:37Z","timestamp":1769881477624,"version":"3.49.0"},"publisher-location":"Cham","reference-count":72,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319633862","type":"print"},{"value":"9783319633879","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63387-9_4","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:43Z","timestamp":1499849623000},"page":"68-94","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Maximum Satisfiability in Software Analysis: Applications and Techniques"],"prefix":"10.1007","author":[{"given":"Xujie","family":"Si","sequence":"first","affiliation":[]},{"given":"Xin","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Radu","family":"Grigore","sequence":"additional","affiliation":[]},{"given":"Mayur","family":"Naik","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"4_CR1","unstructured":"MaxSAT evaluations. http:\/\/www.maxsat.udl.cat\/"},{"key":"4_CR2","volume-title":"Foundations of Databases: The Logical Level","author":"S Abiteboul","year":"1995","unstructured":"Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases: The Logical Level. Addison-Wesley Longman Publishing Co., Inc., Boston (1995)"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Aiken, A.: Introduction to set constraint-based program analysis. Sci. Comput. Program. (1999)","DOI":"10.1016\/S0167-6423(99)00007-6"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-02777-2_39","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"C Ans\u00f3tegui","year":"2009","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial MaxSAT through satisfiability testing. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 427\u2013440. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-02777-2_39"},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/j.artint.2013.01.002","volume":"196","author":"C Ans\u00f3Tegui","year":"2013","unstructured":"Ans\u00f3Tegui, C., Bonet, M.L., Levy, J.: SAT-based MaxSAT algorithms. Artif. Intell. 196, 77\u2013105 (2013)","journal-title":"Artif. Intell."},{"key":"4_CR6","unstructured":"Berg, J., Hyttinen, A., J\u00e4rvisalo, M.: Applications of MaxSAT in data analysis. In: Pragmatics of SAT (2015)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). doi:10.1007\/978-3-319-23534-9_2"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Bjorner, N., Narodytska, N.: Maximum satisfiability using cores and correction sets. In: IJCAI (2015)","DOI":"10.1609\/aaai.v28i1.9124"},{"key":"4_CR9","unstructured":"Bj\u00f8rner, N., Phan, A.D.: $$\\nu $$Z: maximal satisfaction with Z3. In: Proceedings of International Symposium on Symbolic Computation in Software Science (SCSS) (2014)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-662-46681-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Phan, A.-D., Fleckenstein, L.: $$\\nu $$Z - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194\u2013199. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46681-0_14"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Bravenboer, M., Smaragdakis, Y.: Strictly declarative specification of sophisticated points-to analyses. In: OOPSLA (2009)","DOI":"10.1145\/1640089.1640108"},{"key":"4_CR12","unstructured":"den Broeck, G.V., Taghipour, N., Meert, W., Davis, J., Raedt, L.D.: Lifted probabilistic inference by first-order knowledge compilation. In: IJCAI (2011)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Bunte, K., J\u00e4rvisalo, M., Berg, J., Myllym\u00e4ki, P., Peltonen, J., Kaski, S.: Optimal neighborhood preserving visualization by maximum satisfiability. In: AAAI (2014)","DOI":"10.1609\/aaai.v28i1.8974"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-642-39799-8_30","volume-title":"Computer Aided Verification","author":"A Chaganty","year":"2013","unstructured":"Chaganty, A., Lal, A., Nori, A.V., Rajamani, S.K.: Combining relational learning with SMT solvers using CEGAR. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 447\u2013462. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39799-8_30"},{"issue":"11","key":"4_CR15","doi-asserted-by":"publisher","first-page":"1804","DOI":"10.1109\/TCAD.2010.2061270","volume":"29","author":"Y Chen","year":"2010","unstructured":"Chen, Y., Safarpour, S., Marques-Silva, J., Veneris, A.: Automated design debugging with maximum satisfiability. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 29(11), 1804\u20131817 (2010)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-12002-2_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2010","unstructured":"Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability modulo the theory of costs: foundations and applications. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 99\u2013113. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-12002-2_8"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). doi:10.1007\/10722167_15"},{"key":"4_CR18","series-title":"Synthesis Lectures on Artificial Intelligence and Machine Learning","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-01549-6","volume-title":"Markov Logic: An Interface Layer for Artificial Intelligence","author":"P Domingos","year":"2009","unstructured":"Domingos, P., Lowd, D.: Markov Logic: An Interface Layer for Artificial Intelligence. Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers, San Rafael (2009)"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Dubois, D., Prade, H.: Possibilistic logic - an overview. In: Computational Logic. Handbook of the History of Logic, vol. 7. Newnes (2014)","DOI":"10.1016\/B978-0-444-51624-4.50007-1"},{"issue":"4","key":"4_CR20","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). http:\/\/www.sciencedirect.com\/science\/article\/pii\/S1571066105825423","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-boolean constraints into SAT. JSAT (2006)","DOI":"10.3233\/SAT190014"},{"key":"4_CR22","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: NDSS (2017)","DOI":"10.14722\/ndss.2017.23379"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11814948_25","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"Z Fu","year":"2006","unstructured":"Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252\u2013265. Springer, Heidelberg (2006). doi:10.1007\/11814948_25"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Grigore, R., Yang, H.: Abstraction refinement guided by a learnt probabilistic model. In: POPL (2016)","DOI":"10.1145\/2837614.2837663"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"941","DOI":"10.1007\/978-3-642-33558-7_67","volume-title":"Principles and Practice of Constraint Programming","author":"J Guerra","year":"2012","unstructured":"Guerra, J., Lynce, I.: Reasoning over biological networks using maximum satisfiability. In: Milano, M. (ed.) CP 2012. LNCS, pp. 941\u2013956. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-33558-7_67"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Heras, F., Morgado, A., Marques-Silva, J.: Core-guided binary search algorithms for maximum satisfiability. In: AAAI (2011)","DOI":"10.1609\/aaai.v25i1.7822"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Hojjat, H., Rmmer, P., McClurg, J., \u010cern\u00fd, P., Foster, N.: Optimizing horn solvers for network repair. In: FMCAD (2016)","DOI":"10.1109\/FMCAD.2016.7886663"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Ignatiev, A., Morgado, A., Manquinho, V., Lynce, I., Marques-Silva, J.: Progression in maximum satisfiability. In: ECAI (2014)","DOI":"10.3233\/978-1-61499-419-0-453"},{"key":"4_CR29","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68282-2","volume-title":"Bayesian Networks and Decision Graphs","author":"FV Jensen","year":"2007","unstructured":"Jensen, F.V., Nielsen, T.D.: Bayesian Networks and Decision Graphs. Springer, Heidelberg (2007). doi:10.1007\/978-0-387-68282-2"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-49052-6_7","volume-title":"Hardware and Software: Verification and Testing","author":"W Jin","year":"2016","unstructured":"Jin, W., Orso, A.: Improving efficiency and accuracy of formula-based debugging. In: Bloem, R., Arbel, E. (eds.) HVC 2016. LNCS, vol. 10028, pp. 99\u2013116. Springer, Cham (2016). doi:10.1007\/978-3-319-49052-6_7"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: PLDI (2011)","DOI":"10.1145\/1993498.1993550"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Kastrinis, G., Smaragdakis, Y.: Hybrid context sensitivity for points-to analysis. In: PLDI (2013)","DOI":"10.1145\/2491956.2462191"},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"Khoshnood, S., Kusano, M., Wang, C.: ConcBugAssist: constraint solving for diagnosis and repair of concurrency bugs. In: ISSTA (2015)","DOI":"10.1145\/2771783.2771798"},{"key":"4_CR34","unstructured":"Kok, S., Sumner, M., Richardson, M., Singla, P., Poon, H., Lowd, D., Domingos, P.: The Alchemy system for statistical relational AI. Technical report, Department of Computer Science and Engineering, University of Washington, Seattle, WA (2007). http:\/\/alchemy.cs.washington.edu"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: POPL (2014)","DOI":"10.1145\/2535838.2535857"},{"key":"4_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07003-1","volume-title":"Elements of Finite Model Theory","author":"L Libkin","year":"2004","unstructured":"Libkin, L.: Elements of Finite Model Theory. Springer, Heidelberg (2004). doi:10.1007\/978-3-662-07003-1"},{"key":"4_CR37","doi-asserted-by":"crossref","unstructured":"Livshits, B., Sridharan, M., Smaragdakis, Y., Lhot\u00e1k, O., Amaral, J.N., Chang, B.E., Guyer, S.Z., Khedker, U.P., M\u00f8ller, A., Vardoulakis, D.: In defense of soundiness: a manifesto. CACM (2015)","DOI":"10.1145\/2644805"},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"Mangal, R., Zhang, X., Kamath, A., Nori, A.V., Naik, M.: Scaling relational inference using proofs and refutations. In: AAAI (2016)","DOI":"10.1609\/aaai.v30i1.10426"},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"Mangal, R., Zhang, X., Nori, A.V., Naik, M.: A user-guided approach to program analysis. In: FSE (2015)","DOI":"10.1145\/2786805.2786851"},{"key":"4_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-319-24318-4_22","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"R Mangal","year":"2015","unstructured":"Mangal, R., Zhang, X., Nori, A.V., Naik, M.: Volt: a lazy grounding framework for solving very large MaxSAT instances. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 299\u2013306. Springer, Cham (2015). doi:10.1007\/978-3-319-24318-4_22"},{"key":"4_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-642-02777-2_45","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"V Manquinho","year":"2009","unstructured":"Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for weighted boolean optimization. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 495\u2013508. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-02777-2_45"},{"key":"4_CR42","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Planes, J.: Algorithms for maximum satisfiability using unsatisfiable cores. In: DATE (2008)","DOI":"10.1145\/1403375.1403474"},{"key":"4_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/978-3-319-10428-7_39","volume-title":"Principles and Practice of Constraint Programming","author":"R Martins","year":"2014","unstructured":"Martins, R., Joshi, S., Manquinho, V., Lynce, I.: Incremental cardinality constraints for MaxSAT. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 531\u2013548. Springer, Cham (2014). doi:10.1007\/978-3-319-10428-7_39"},{"key":"4_CR44","unstructured":"Milch, B., Zettlemoyer, L.S., Kersting, K., Haimes, M., Kaelbling, L.P.: Lifted probabilistic inference with counting formulas. In: AAAI (2008)"},{"key":"4_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1007\/978-3-319-10428-7_41","volume-title":"Principles and Practice of Constraint Programming","author":"A Morgado","year":"2014","unstructured":"Morgado, A., Dodaro, C., Marques-Silva, J.: Core-guided MaxSAT with soft cardinality constraints. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 564\u2013573. Springer, Cham (2014). doi:10.1007\/978-3-319-10428-7_41"},{"issue":"4","key":"4_CR46","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/s10601-013-9146-2","volume":"18","author":"A Morgado","year":"2013","unstructured":"Morgado, A., Heras, F., Liffiton, M., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints 18(4), 478\u2013534 (2013). http:\/\/dx.doi.org\/10.1007\/s10601-013-9146-2","journal-title":"Constraints"},{"key":"4_CR47","doi-asserted-by":"crossref","unstructured":"Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSAT resolution. In: AAAI (2014)","DOI":"10.1609\/aaai.v28i1.9124"},{"key":"4_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11814948_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A.: On SAT modulo theories and optimization problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 156\u2013169. Springer, Heidelberg (2006). doi:10.1007\/11814948_18"},{"key":"4_CR49","doi-asserted-by":"crossref","unstructured":"Niu, F., R\u00e9, C., Doan, A., Shavlik, J.W.: Tuffy: scaling up statistical inference in Markov logic networks using an RDBMS. In: VLDB (2011)","DOI":"10.14778\/1978665.1978669"},{"key":"4_CR50","doi-asserted-by":"crossref","unstructured":"Noessner, J., Niepert, M., Stuckenschmidt, H.: RockIt: exploiting parallelism and symmetry for MAP inference in statistical relational models. In: AAAI (2013)","DOI":"10.1609\/aaai.v27i1.8579"},{"key":"4_CR51","doi-asserted-by":"crossref","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: PLDI (2016)","DOI":"10.1145\/2908080.2908118"},{"key":"4_CR52","unstructured":"Poole, D.: First-order probabilistic inference. In: IJCAI (2003)"},{"key":"4_CR53","unstructured":"Riedel, S.: Improving the accuracy and efficiency of MAP inference for Markov logic. In: UAI (2008)"},{"key":"4_CR54","doi-asserted-by":"crossref","unstructured":"Ross, K.A.: Modular stratification and magic sets for DATALOG programs with negation. In: PODS (1990)","DOI":"10.1145\/298514.298558"},{"key":"4_CR55","unstructured":"Roussel, O., Manquinho, V.M.: Pseudo-Boolean and Cardinality Constraints. In: Handbook of satisfiability. IOS Press (2009)"},{"key":"4_CR56","doi-asserted-by":"crossref","unstructured":"Safarpour, S., Mangassarian, H., Veneris, A., Liffiton, M.H., Sakallah, K.A.: Improved design debugging using maximum satisfiability. In: FMCAD (2007)","DOI":"10.1109\/FMCAD.2007.4401977"},{"key":"4_CR57","unstructured":"de Salvo Braz, R., Amir, E., Roth, D.: Lifted first-order probabilistic inference. In: IJCAI (2005)"},{"key":"4_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-642-31365-3_38","volume-title":"Automated Reasoning","author":"R Sebastiani","year":"2012","unstructured":"Sebastiani, R., Tomasi, S.: Optimization in SMT with $${\\cal{L}A}$$($$\\mathbb{Q}$$) cost functions. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 484\u2013498. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-31365-3_38"},{"key":"4_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-662-54580-5_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Sebastiani","year":"2017","unstructured":"Sebastiani, R., Trentin, P.: On optimization modulo theories, MaxSMT and sorting networks. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 231\u2013248. Springer, Heidelberg (2017). doi:10.1007\/978-3-662-54580-5_14"},{"key":"4_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-319-44953-1_30","volume-title":"Principles and Practice of Constraint Programming","author":"X Si","year":"2016","unstructured":"Si, X., Zhang, X., Manquinho, V., Janota, M., Ignatiev, A., Naik, M.: On incremental core-guided MaxSAT solving. In: Rueher, M. (ed.) CP 2016. LNCS, vol. 9892, pp. 473\u2013482. Springer, Cham (2016). doi:10.1007\/978-3-319-44953-1_30"},{"key":"4_CR61","unstructured":"Singla, P., Domingos, P.: Discriminative training of Markov logic networks. In: AAAI (2005)"},{"key":"4_CR62","unstructured":"Singla, P., Domingos, P.: Lifted first-order belief propagation. In: AAAI (2008)"},{"key":"4_CR63","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: Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827\u2013831. Springer, Heidelberg (2005). doi:10.1007\/11564751_73"},{"key":"4_CR64","doi-asserted-by":"crossref","unstructured":"Smaragdakis, Y., Bravenboer, M.: Using datalog for fast and easy program analysis. In: Datalog 2.0 Workshop (2010)","DOI":"10.1007\/978-3-642-24206-9_14"},{"key":"4_CR65","unstructured":"Smaragdakis, Y., Bravenboer, M., Lhot\u00e1k, O.: Pick your contexts well: understanding object-sensitivity. In: POPL (2013)"},{"key":"4_CR66","doi-asserted-by":"crossref","unstructured":"Smaragdakis, Y., Kastrinis, G., Balatsouras, G.: Introspective analysis: context-sensitivity, across the board. In: PLDI (2014)","DOI":"10.1145\/2594291.2594320"},{"key":"4_CR67","doi-asserted-by":"crossref","unstructured":"Tucker, C., Shuffelton, D., Jhala, R., Lerner, S.: OPIUM: optimal package install\/uninstall manager. In: ICSE (2007)","DOI":"10.1109\/ICSE.2007.59"},{"key":"4_CR68","unstructured":"Walter, R., Zengler, C., Kuchlin, W.: Applications of MaxSAT in automotive configuration. In: Proceedings of the 15th International Configuration Workshop (2013)"},{"key":"4_CR69","doi-asserted-by":"crossref","unstructured":"Zhang, X., Grigore, R., Si, X., Naik, M.: Effective interactive resolution of static analysis alarms (2016)","DOI":"10.1145\/3133881"},{"key":"4_CR70","doi-asserted-by":"crossref","unstructured":"Zhang, X., Mangal, R., Grigore, R., Naik, M., Yang, H.: On abstraction refinement for program analyses in datalog. In: PLDI (2014)","DOI":"10.1145\/2594291.2594327"},{"key":"4_CR71","doi-asserted-by":"crossref","unstructured":"Zhang, X., Mangal, R., Nori, A.V., Naik, M.: Query-guided maximum satisfiability. In: POPL (2016)","DOI":"10.1145\/2837614.2837658"},{"key":"4_CR72","unstructured":"Zhu, C.S., Weissenbacher, G., Malik, S.: Post-silicon fault localisation using maximum satisfiability and backbones. In: FMCAD (2011)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63387-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T00:56:27Z","timestamp":1750553787000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63387-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633862","9783319633879"],"references-count":72,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63387-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}