×

zbMATH — the first resource for mathematics

Iterative and core-guided maxsat solving: a survey and assessment. (English) Zbl 1317.90199
Summary: Maximum Satisfiability (MaxSAT) is an optimization version of SAT, and many real world applications can be naturally encoded as such. Solving MaxSAT is an important problem from both a theoretical and a practical point of view. In recent years, there has been considerable interest in developing efficient algorithms and several families of algorithms have been proposed. This paper overviews recent approaches to handle MaxSAT and presents a survey of MaxSAT algorithms based on iteratively calling a SAT solver which are particularly effective to solve problems arising in industrial settings. First, classic algorithms based on iteratively calling a SAT solver and updating a bound are overviewed. Such algorithms are referred to as iterative MaxSAT algorithms. Then, more sophisticated algorithms that additionally take advantage of unsatisfiable cores are described, which are referred to as core-guided MaxSAT algorithms. Core-guided MaxSAT algorithms use the information provided by unsatisfiable cores to relax clauses on demand and to create simpler constraints. Finally, a comprehensive empirical study on non-random benchmarks is conducted, including not only the surveyed algorithms, but also other state-of-the-art MaxSAT solvers. The results indicate that (i) core-guided MaxSAT algorithms in general abort in less instances than classic solvers based on iteratively calling a SAT solver and that (ii) core-guided MaxSAT algorithms are fairly competitive compared to other approaches.

MSC:
90C09 Boolean programming
90C59 Approximation methods and heuristics in mathematical programming
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aksoy, L; daCosta, EAC; Flores, PF; Monteiro, J, Exact and approximate algorithms for the optimization of area and delay in multiple constant multiplications, IEEE Transactions on CAD of Integrated Circuits and Systems on CAD, 27, 1013-1026, (2008)
[2] Aloul, F., Ramani, A., Markov, I., Sakallah, K. (2002). PBS: A backtrack search pseudo-Boolean solver. In Symposium on theory and applications of satisfiability testing (pp. 346-353). · Zbl 1339.68244
[3] Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A. (2002). Generic ILP versus specialized 0-1 ILP: An update. In International conference on computer-aided design (pp. 450-457). · Zbl 1208.68199
[4] Andres, B., Kaufmann, B., Matheis, O., Schaub, T. (2012). Unsatisfiability-based optimization in clasp. In International conference on logic programming (Technical communications) (pp. 211-221). · Zbl 1281.68204
[5] Anjos, MF, Semidefinite optimization approaches for satisfiability and maximum-satisfiability problems, Journal on Satisfiability, Boolean Modeling and Computation, 1, 1-47, (2006) · Zbl 1194.90064
[6] Ansótegui, C., Bonet, M.L., Gabàs, J., Levy, J. (2012). Improving SAT-based weighted MaxSAT solvers. In International conference on principles and practice of constraint programming (pp. 86-101).
[7] Ansótegui, C., Bonet, M.L., Levy, J. (2009). On solving MaxSAT through SAT. In International conference of the Catalan Association for artificial intelligence (pp. 284-292). · Zbl 1247.68242
[8] Ansótegui, C., Bonet, M.L., Levy, J. (2009). Solving (weighted) partial MaxSAT through satisfiability testing. In International conference on theory and applications of satisfiability testing (pp. 427-440). · Zbl 1247.68242
[9] Ansótegui, C., Bonet, M.L., Levy, J. (2010). A new algorithm for weighted partial MaxSAT. In AAAI conference on artificial intelligence (pp. 3-8).
[10] Ansótegui, C., Bonet, M.L., Levy, J. (2013). SAT-based MaxSAT algorithms. In Artificial inteligence journal (Vol. 196, pp. 77-105). · Zbl 1270.68265
[11] Ansótegui, C., & Manyà, F. (2004). Mapping problems with finite-domain variables into problems with Boolean variables. In International conference on theory and applications of satisfiability testing (pp. 111-119).
[12] Ardagna, C.A., diVimercati, S.D.C., Foresti, S., Paraboschi, S., Samarati, P. (2010). Minimizing disclosure of private information in credential-based interactions: A graph-based approach. In International conference on social computing/international conference on privacy, security, risk and trust (pp. 743-750).
[13] Argelich, J., Berre, D.L., Lynce, I., Marques-Silva, J., Rapicault, P. (2010). Solving linux upgradeability problems using Boolean optimization. In International workshop on logics for component configuration (pp. 11-22).
[14] Argelich, J., Li, C.M., Manya, F., Planes, J. (2011). Experimenting with the instances of the MaxSAT Evaluation. In International conference of the catalan association for artificial intelligence (pp. 360-361). · Zbl 1326.68164
[15] Argelich, J., & Lynce, I. (2008). CNF instances from the software package installation problem. In RCRA international workshop on “Experimental Evaluation of Algorithms for solving problems with combinatorial explosion”.
[16] Argelich, J., Lynce, I., Marques-Silva, J. (2009). On solving Boolean multilevel optimization problems. In International joint conference on artificial intelligence (pp. 393-398). · Zbl 0959.68049
[17] Asín, R., & Nieuwenhuis, R. (2010). Curriculum-based course timetabling with SAT and MaxSAT. In International conference on the practice and theory of automated timetabling (pp. 42-56). · Zbl 1215.92043
[18] Asín, R., & Nieuwenhuis, R. (2012). Curriculum-based course timetabling with SAT and MaxSAT. Annals of Operations Research, 1-21. · Zbl 1301.90023
[19] Asín, R; Nieuwenhuis, R; Oliveras, A; Rodríguez-Carbonell, E, Cardinality networks: a theoretical and empirical study, Constraints, 16, 195-221, (2011) · Zbl 1217.68200
[20] Bailleux, O., & Boufkhad, Y. (2003). Efficient CNF encoding of Boolean cardinality constraints. In International conference on principles and practice of constraint programming (pp. 108-122). · Zbl 1273.68332
[21] Bansal, N., & Raman, V. (1999). Upper bounds for MaxSat: Further improved. In International symposium on algorithms and computation (pp. 247-258). · Zbl 0971.68069
[22] Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C. (2009). Satisfiability modulo theories. In Handbook of satisfiability (pp. 825-884). IOS Press. · Zbl 1159.68567
[23] Barth, P. (1995). A Davis-Putnam enumeration algorithm for linear pseudo-Boolean optimization. Technical Report MPI-I-95-2-003, Max Plank Institute for Computer Science. · Zbl 1242.90199
[24] Batcher, K.E. (1968). Sorting networks and their applications. In AFIPS spring joint computing conference (pp. 307-314). · Zbl 1145.68501
[25] Berre, DL; Parrain, A, The sat4j library, release 2.2, Journal on Satisfiability, Boolean Modeling and Computation, 7, 59-64, (2010)
[26] Biere, A, Picosat essentials, Journal on Satisfiability, Boolean Modeling and Computation, 2, 75-97, (2008) · Zbl 1159.68403
[27] Birnbaum, E; Lozinskii, EL, Consistent subsets of inconsistent systems: structure and behaviour, Journal of Experimental and Theoretical Artificial Intelligence, 15, 25-46, (2003) · Zbl 1025.68090
[28] Bonet, ML; Levy, J; Manyà, F, Resolution for MAX-SAT, Artificial Intelligence Journal, 171, 606-618, (2007) · Zbl 1168.68541
[29] Borchers, B; Furman, J, A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems, Journal of Combinatorial Optimization, 2, 299-306, (1999) · Zbl 0954.90026
[30] Brihaye, T., Bruyère, V., Doyen, L., Ducobu, M., Raskin, J.-F. (2011). Antichain-based QBF solving. In International symposium on automated technology for verification and analysis (pp. 183-197). · Zbl 1348.68224
[31] Cha, B., Iwama, K., Kambayashi, Y., Miyazaki, S. (1997). Local search algorithms for partial MaxSAT. In AAAI conference on artificial intelligence/IAAI innovative applications of artificial intelligence conference (pp. 263-268). · Zbl 1182.68253
[32] Chai, D., & Kuehlmann, A. (2003). A fast pseudo-Boolean constraint solver. In Design automation conference (pp. 830-835). · Zbl 1154.68510
[33] Chen, Y; Safarpour, S; Marques-Silva, J; Veneris, AG, Automated design debugging with maximum satisfiability, IEEE Transactions on CAD of Integrated Circuits and Systems, 29, 1804-1817, (2010)
[34] Chen, Y., Safarpour, S., Veneris, A., Marques-Silva, J. (2009). Spatial and temporal design debug using partial MaxSAT. In IEEE great lakes symposium on VLSI. · Zbl 1331.68209
[35] Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R., Stenico, C. (2010). Satisfiability modulo the theory of costs: Foundations and applications. In International conference tools and algorithms for the construction and analysis of systems (pp. 99-113). · Zbl 1284.68388
[36] Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R. (2013). A modular approach to MaxSAT modulo theories. In International conference on theory and applications of satisfiability testing (pp. 150-165). · Zbl 1390.68572
[37] Codish, M; Lagoon, V; Stuckey, PJ, Logic programming with satisfiability, Journal of Theory and Practice of Logic Programming, 8, 121-128, (2008) · Zbl 1128.68014
[38] Cooper, M.C., Cussat-Blanc, S., deRoquemaurel, M., Régnier, P. (2006). Soft arc consistency applied to optimal planning. In International conference on principles and practice of constraint programming (pp. 680-684). · Zbl 0643.68122
[39] Cooper, MC; deGivry, S; Sanchez, M; Schiex, T; Zytnicki, M; Werner, T, Soft arc consistency revisited, Artificial Intelligence Journal, 174, 449-478, (2010) · Zbl 1213.68580
[40] Davies, J., & Bacchus, F. (2011). Solving MaxSAT by solving a sequence of simpler SAT instances. In International conference on principles and practice of constraint programming (pp. 225-239). · Zbl 1183.68578
[41] Davies, J., Cho, J., Bacchus, F. (2010). Using learnt clauses in MaxSAT. In International conference on principles and practice of constraint programming (pp. 176-190). · Zbl 1159.68565
[42] deGivry, S., Larrosa, J., Meseguer, P., Schiex, T. (2003). Solving Max-SAT as weighted CSP. In International conference on principles and practice of constraint programming (pp. 363-376). · Zbl 1273.68368
[43] deMoura, L.M., & Bjørner, N. (2008). Z3: An efficient SMT solver. In International conference tools and algorithms for the construction and analysis of systems (pp. 337-340).
[44] Eén, N., & Sörensson, N. (2003). An extensible SAT-solver. In International conference on theory and applications of satisfiability testing (pp. 502-518). · Zbl 1215.92043
[45] Een, N; Sörensson, N, Translating pseudo-Boolean constraints into SAT, Journal on Satisfiability, Boolean Modeling and Computation, 2, 1-26, (2006) · Zbl 1116.68083
[46] Feldman, A., Provan, G., deKleer, J., Robert, S., van Gemund, A. (2010). Solving model-based diagnosis problems with MaxSAT solvers and vice versa. In International workshop on the principles of diagnosis. · Zbl 0886.68069
[47] Fu, Z., & Malik, S. (2006). On solving the partial MAX-SAT problem. In International conference on theory and applications of satisfiability testing (pp. 252-265). · Zbl 1187.68540
[48] Gebser, M., Kaufmann, B., Schaub, T. (2009). The conflict-driven answer set solver clasp: Progress report. In International conference on logic programming and nonmonotonic reasoning (pp. 509-514). · Zbl 1107.68029
[49] Gent, I.P., & Nightingale, P. (2004). A new encoding of alldifferent into SAT. In International workshop on modelling and reformulating constraint satisfaction problems (pp. 95-110).
[50] Giunchiglia, E; Lierler, Y; Maratea, M, Answer set programming based on propositional satisfiability, Journal of Automated Reasoning, 36, 345-377, (2006) · Zbl 1107.68029
[51] Giunchiglia, E., & Maratea, M. (2006). Optsat: A tool for solving SAT related optimization problems. In European conference on logics in artificial intelligence (JELIA) (pp. 485-489). · Zbl 1152.68553
[52] Giunchiglia, E., & Maratea, M. (2006). Solving optimization problems with DLL. In European conference on artificial intelligence (pp. 377-381). · Zbl 1217.68200
[53] Giunchiglia, E., & Maratea, M. (2007). Planning as satisfiability with preferences. In AAAI conference on artificial intelligence (pp. 987-992).
[54] Gomes, C.P., van Hoeve, W.J., Leahu, L. (2006). The power of semidefinite programming relaxations for Max-SAT. In International conference integration of AI and OR techniques in constraint programming for combinatorial optimization problems (pp. 104-118). · Zbl 1177.68186
[55] Gottlob, G, NP trees and carnap’s modal logic, Journal of ACM, 42, 421-457, (1995) · Zbl 0886.68069
[56] Graca, A., Lynce, I., Marques-Silva, J., Oliveira, A. (2010). Efficient and accurate haplotype inference by combining parsimony and pedigree information. In International conference algebraic and numeric biology (pp. 38-56). · Zbl 1256.92037
[57] Graca, A; Marques-Silva, J; Lynce, I; Oliveira, A, Haplotype inference with pseudo-Boolean optimization, Annals of Operations Research, 184, 137-162, (2011) · Zbl 1215.92043
[58] Guerra, J., & Lynce, I. (2012). Reasoning over biological networks using maximum satisfiability. In International conference on principles and practice of constraint programming (pp. 941-956).
[59] Hachtel, G.D., & Somenzi, F. (1996). Logic synthesis and verification algorithms. Kluwer. · Zbl 0861.94035
[60] Heras, F; Larrosa, J; deGivry, S; Schiex, T, 2006 and 2007 MAX-SAT evaluations: contributed instances, Journal on Satisfiability, Boolean Modeling and Computation, 4, 239-250, (2008) · Zbl 1159.68565
[61] Heras, F; Larrosa, J; Oliveras, A, Minimaxsat: an efficient weighted MAX-SAT solver, Journal of Artificial Intelligence Research, 31, 1-32, (2008) · Zbl 1183.68578
[62] Heras, F., & Marques-Silva, J. (2011). Read-once resolution for unsatisfiability-based Max-SAT algorithms. In International joint conference on artificial intelligence (pp. 572-577).
[63] Heras, F., Morgado, A., Marques-Silva, J. (2011). Core-guided binary search for maximum satisfiability. In AAAI conference on artificial intelligence. · Zbl 1273.68357
[64] Hoos, H., & Stützle, T. (2005). Stochastic local search: Foundations and applications. Morgan Kaufmann. · Zbl 1126.68032
[65] Hoos, H.H. (2002). An adaptive noise mechanism for WalkSAT. In AAAI conference on artificial intelligence/IAAI innovative applications of artificial intelligence conference (pp. 655-660).
[66] Jose, M., & Majumdar, R. (2011). Bug-assist: Assisting fault localization in ANSI-C programs. In International conference on computer aided verification (pp. 504-509).
[67] Jose, M., & Majumdar, R. (2011). Cause clue clauses: Error localization using maximum satisfiability. In ACM SIGPLAN conference on programming language design and implementation (pp. 437-446).
[68] Juma, F., Hsu, E.I., McIlraith, S.A. (2012). Preference-based planning via MaxSAT. In Canadian conference on AI (pp. 109-120).
[69] Koshimura, M; Zhang, T; Fujita, H; Hasegawa, R, Qmaxsat: a partial MAX-SAT solver, Journal on Satisfiability, Boolean Modeling and Computation, 8, 95-100, (2012) · Zbl 1331.68209
[70] Kuegel, A. (2010). Improved exact solver for the weighted MAX-SAT problem. In Pragmatics of SAT. · Zbl 1168.68541
[71] Larrosa, J., & Heras, F. (2005). Resolution in Max-SAT and its relation to local consistency in weighted CSPs. In International joint conference on artificial intelligence (pp. 193-198). · Zbl 1153.68463
[72] Larrosa, J; Heras, F; deGivry, S, A logical approach to efficient MAX-SAT solving, Artificial Inteligence Journal, 172, 204-233, (2008) · Zbl 1182.68253
[73] Larrosa, J; Schiex, T, Solving weighted CSP by maintaining arc consistency, Artificial Inteligence Journal, 159, 1-26, (2004) · Zbl 1086.68592
[74] Li, C.M., & Manyà, F. (2009). MaxSAT, hard and soft constraints. In Handbook of satisfiability (pp. 613-632). IOS Press.
[75] Li, C.M., Manyà, F., Planes, J. (2005). Exploiting unit propagation to compute lower bounds in branch and bound Max-SAT solvers. In International conference on principles and practice of constraint programming (pp. 403-414). · Zbl 1153.68470
[76] Li, CM; Manyà, F; Planes, J, New inference rules for MAX-SAT, Journal of Artificial Intelligence Research, 30, 321-359, (2007) · Zbl 1182.68254
[77] Liffiton, M.H., Sakallah, K.A. (2005). On finding all minimally unsatisfiable subformulas. In International conference on theory and applications of satisfiability testing (pp. 173-186). · Zbl 1128.68473
[78] Liffiton, MH; Sakallah, KA, Algorithms for computing minimal unsatisfiable subsets of constraints, Journal Automated Reasoning, 40, 1-33, (2008) · Zbl 1154.68510
[79] Lin, H., Su, K., Li, C.M. (2008). Within-problem learning for efficient lower bound computation in Max-SAT solving. In AAAI conference on artificial intelligence (pp. 351-356).
[80] Mancinelli, F., Boender, J., diCosmo, R., Vouillon, J., Durak, B., Leroy, X., Treinen, R. (2006). Managing the complexity of large free and open source package-based software distributions. In International conference on automated software engineering (pp. 199-208). · Zbl 1217.68200
[81] Mangassarian, H., Veneris, A.G., Safarpour, S., Najm, F.N., Abadir, M.S. (2007). Maximum circuit activity estimation using pseudo-Boolean satisfiability. In Conference on design, automation and test in Europe (pp. 1538-1543).
[82] Manquinho, V., Marques-Silva, J., Planes, J. (2009). Algorithms for weighted Boolean optimization. In International conference on theory and applications of satisfiability testing (pp. 495-508). · Zbl 1247.68258
[83] Manquinho, V., Martins, R., Lynce, I. (2010). Improving unsatisfiability-based algorithms for Boolean optimization. In International conference on theory and applications of satisfiability testing (pp. 181-193). · Zbl 1306.68166
[84] Marques-Silva, J; Argelich, J; Graça, A; Lynce, I, Boolean lexicographic optimization: algorithms & applications, Annals of Mathematics and Artificial Intelligence, 62, 317-343, (2011) · Zbl 1242.90199
[85] Marques-Silva, J., & Manquinho, V. (2008). Towards more effective unsatisfiability-based maximum satisfiability algorithms. In International conference on theory and applications of satisfiability testing (pp. 225-230). · Zbl 1138.68548
[86] Marques-Silva, J., & Planes, J. (2007). On using unsatisfiability for solving maximum satisfiability. Computing Research Repository. arXiv: abs/0712.0097.
[87] Marques-Silva, J., Planes, J. (2008). Algorithms for maximum satisfiability using unsatisfiable cores. In Conference on design, automation and testing in Europe (pp. 408-413).
[88] Marques-Silva, J., & Sakallah, K.A. (1996). GRASP—a new search algorithm for satisfiability. In International conference on computer-aided design (pp. 220-227).
[89] Martins, R., Manquinho, V., Lynce, I. (2012). On partitioning for maximum satisfiability. In European conference on artificial intelligence (pp. 913-914). · Zbl 1165.90664
[90] Martins, R., Manquinho, V.M., Lynce, I. (2013). Community-based partitioning for MaxSAT solving. In International conference on theory and applications of satisfiability testing (pp. 182-191). · Zbl 1390.68603
[91] Morgado, A., Heras, F., Marques-Silva, J. (2011). The MSUnCore MaxSAT solver. In Pragmatics of SAT.
[92] Morgado, A., Heras, F., Marques-Silva, J. (2012). Improvements to core-guided binary search for MaxSAT. In Theory and applications of satisfiability testing (pp. 284-297). · Zbl 1273.68357
[93] Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S. (2001). Chaff: Engineering an efficient SAT solver. In Design automation conference (pp. 530-535). · Zbl 1132.68716
[94] Neveu, B., Trombettoni, G., Glover, F. (2004). ID Walk: A candidate list strategy with a simple diversification device. In International conference on principles and practice of constraint programming (pp. 423-437). · Zbl 1152.68568
[95] Niedermeier, R; Rossmanith, P, New upper bounds for maximum satisfiability, Journal of Algorithms, 36, 63-88, (2000) · Zbl 0959.68049
[96] Nieuwenhuis, R., & Oliveras, A. (2006). On SAT modulo theories and optimization problems. In International conference on theory and applications of satisfiability testing (pp. 156-169). · Zbl 1187.68558
[97] Nieuwenhuis, R; Oliveras, A; Tinelli, C, Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-logemann-loveland procedure to DPLL(\(T\)), Journal of ACM, 53, 937-977, (2006) · Zbl 1326.68164
[98] Oikarinen, E., Järvisalo, M. (2009). Max-ASP: Maximum satisfiability of answer set programs. In International conference on logic programming and nonmonotonic reasoning (pp. 236-249). · Zbl 1258.68037
[99] Palubeckis, G, A new bounding procedure and an improved exact algorithm for the MAX-2-SAT problem, Applied Mathematics and Computation, 215, 1106-1117, (2009) · Zbl 1179.90234
[100] Papadimitriou, C. (1994). Computational complexity. USA: Addison-Wesley. · Zbl 0833.68049
[101] Papadimitriou, C., & Zachos, S. (1983). Two remarks on the power of counting. Theoretical Computer Science, 269-276. · Zbl 1116.68090
[102] Park, J.D. (2002). Using weighted MAX-SAT engines to solve MPE. In AAAI conference on artificial intelligence (pp. 682-687).
[103] Pipatsrisawat, K; Palyan, A; Chavira, M; Choi, A; Darwiche, A, Solving weighted MAX-SAT problems in a reduced search space: a performance analysis, Journal on Satisfiability Boolean Modeling and Computation, 4, 191-217, (2008) · Zbl 1159.68567
[104] Prestwich, S. (2009). CNF encodings. In Handbook of satisfiability (pp. 75-98). IOS Press. · Zbl 1107.68029
[105] Prestwich, S.D. (2007). Variable dependency in local search: Prevention is better than cure. In International conference on theory and applications of satisfiability testing (pp. 107-120). · Zbl 1214.68369
[106] Ramírez, M., & Geffner, H. (2007). Structural relaxations by variable renaming and their compilation for solving MinCostSAT. In International conference on principles and practice of constraint programming (pp. 605-619).
[107] Reiter, R, A theory of diagnosis from first principles, Artificial Inteligence Journal, 32, 57-95, (1987) · Zbl 0643.68122
[108] Robinson, N., Gretton, C., Pham, D.N., Sattar, A. (2010). Partial weighted MaxSAT for optimal planning. In Pacific rim international conference on artificial intelligence (pp. 231-243).
[109] Rosa, ED; Giunchiglia, E; Maratea, M, Solving satisfiability problems with preferences, Constraints, 15, 485-515, (2010) · Zbl 1208.68199
[110] Roussel, O., & Manquinho, V. (2009). Pseudo-Boolean and cardinality constraints. In Handbook of satisfiability (pp. 695-734). IOS Press. · Zbl 1086.68058
[111] Safarpour, S., Mangassarian, H., Veneris, A., Liffiton, M.H., Sakallah, K.A. (2007). Improved design debugging using maximum satisfiability. In Formal methods in computer-aided design.
[112] Sandholm, T. (1999). An algorithm for optimal winner determination in combinatorial auctions. In International joint conference on artificial intelligence (pp. 542-547).
[113] Sebastiani, R, Lazy satisfiability modulo theories, Journal on Satisfiability, Boolean Modeling and Computation, 3, 141-224, (2007) · Zbl 1145.68501
[114] Sebastiani, R., & Tomasi, S. (2012). Optimization in SMT with LA(Q) cost functions. In International joint conference in automated reasoning (pp. 484-498). · Zbl 1358.68264
[115] Selman, B., Kautz, H.A., Cohen, B. (1994). Noise strategies for improving local search. In AAAI conference on artificial intelligence (pp. 337-343).
[116] Selman, B., Levesque, H.J., Mitchell, D.G. (1992). A new method for solving hard satisfiability problems. In AAAI conference on artificial intelligence (pp. 440-446).
[117] Sheini, H; Sakallah, K, Pueblo: a hybrid pseudo-Boolean SAT solver, Journal on Satisfiability, Boolean Modeling and Computation, 3, 165-189, (2006) · Zbl 1116.68090
[118] Shen, H; Zhang, H, Improving exact algorithms for MAX-2-SAT, Annals of Mathematics and Artificial Intelligence, 44, 419-436, (2005) · Zbl 1086.68058
[119] Sinz, C. (2005). Towards an optimal CNF encoding of Boolean cardinality constraints. In International conference on principles and practice of constraint programming (pp. 827-831). · Zbl 1153.68488
[120] Strickland, D; Barnes, E; Sokol, J, Optimal protein structure alignment using maximum cliques, Operations Research, 53, 389-402, (2005) · Zbl 1165.90664
[121] Teresa Alsinet, J.P., Manyà, F. (2004). A Max-SAT solver with lazy data structures. In Ibero-American conference on AI (IBERAMIA) (pp. 334-342).
[122] Tompkins, D.A.D., & Hoos, H.H. (2004). UBCSAT: An implementation and experimentation environment for SLS algorithms for SAT & Max-SAT. In International conference on theory and applications of satisfiability testing (pp. 37-46). · Zbl 1122.68620
[123] Tucker, C., Shuffelton, D., Jhala, R., Lerner, S. (2007). OPIUM: Optimal package install/uninstall manager. In International conference on software engineering (pp. 178-188).
[124] Vasquez, M; Hao, J, A logic-constrained knapsack formulation and a tabu algorithm for the daily photograph scheduling of an Earth observation satellite, Journal of Computational Optimization and Applications, 20, 137-157, (2001) · Zbl 0983.90082
[125] Warners, JP, A linear-time transformation of linear inequalities into conjunctive normal form, Information Processing Letters, 68, 63-69, (1998) · Zbl 1339.68244
[126] Xing, Z; Zhang, W, Maxsolver: an efficient exact algorithm for (weighted) maximum satisfiability, Artificial Inteligence Journal, 164, 47-80, (2005) · Zbl 1132.68716
[127] Xu, H., Rutenbar, R., Sakallah, K. (2002). sub-SAT: A formulation for relaxed boolean satisfiability with applications in routing. In International symposium on physical design (pp. 182-187). · Zbl 0983.90082
[128] Zhang, L., & Malik, S. (2003). Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In Conference on design, automation and testing in Europe (pp. 10880-10885).
[129] Zhang, L., & Bacchus, F. (2012). MaxSAT heuristics for cost optimal planning. In AAAI conference on artificial intelligence (pp. 1846-1852). · Zbl 1165.90664
[130] Zhu, C.S., Weissenbacher, G., Malik, S. (2011). Post-silicon fault localisation using maximum satisfiability and backbones. In Formal methods in computer-aided design (pp. 63-66).
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.