MaxSolver swMATH ID: 1990 Software Authors: Zhao Xing , Weixiong Zhang Description: Maximum Boolean satisfiability (max-SAT) is the optimization counterpart of Boolean satisfiability (SAT), in which a variable assignment is sought to satisfy the maximum number of clauses in a Boolean formula. A branch and bound algorithm based on the Davis–Putnam–Logemann–Loveland procedure (DPLL) is one of the most competitive exact algorithms for solving max-SAT. In this paper, we propose and investigate a number of strategies for max-SAT. The first strategy is a set of unit propagation or unit resolution rules for max-SAT. We summarize three existing unit propagation rules and propose a new one based on a nonlinear programming formulation of max-SAT. The second strategy is an effective lower bound based on linear programming (LP). We show that the LP lower bound can be made effective as the number of clauses increases. The third strategy consists of a binary-claus! e first rule and a dynamic-weighting variable ordering rule, which are motivated by a thorough analysis of two existing well-known variable orderings. Based on the analysis of these strategies, we develop an exact solver for both max-SAT and weighted max-SAT. Our experimental results on random problem instances and many instances from the max-SAT libraries show that our new solver outperforms most of the existing exact max-SAT solvers, with orders of magnitude of improvement in many cases. Homepage: http://www.sciencedirect.com/science/article/pii/S0004370205000160 Keywords: Weighted maximum satisfiability; DPLL; Unit propagation; Linear programming; Nonlinear programming; Variable ordering Related Software: Chaff; MiniMaxSat; MiniSat; Pueblo; PBS; UBCSAT; MAX-2-SAT; GLPK; SATLIB; OPL; XPRESS; TSPTW; MaxHS; MSUnCore; QMaxSAT; OPIUM; ToulBar2; Sat4j; clasp; PicoSAT Cited in: 19 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability. Zbl 1132.68716Xing, Zhao; Zhang, Weixiong 2005 all top 5 Cited by 41 Authors 4 Larrosa, Javier 4 Oliveras, Albert 3 Heras, Federico 3 Nieuwenhuis, Robert 2 Arieli, Ofer 2 Rodríguez-Carbonell, Enric 2 van Hoeve, Willem-Jan 2 Zamansky, Anna 1 Argelich, Josep 1 Benhamou, Belaid 1 Boughaci, Dalila 1 Crama, Yves 1 de Givry, Simon 1 Di Rosa, Emanuele 1 Drias, Habiba 1 Eiter, Thomas 1 Erdem, Esra 1 Fink, Michael 1 Giunchiglia, Enrico 1 Gomes, Carla P. 1 Hammer, Peter Ladislaw 1 Ibaraki, Toshihide 1 Imamichi, Takashi 1 Koga, Yuichi 1 Leahu, Lucian 1 Liffiton, Mark H. 1 Manyà, Felip 1 Maratea, Marco 1 Marques-Silva, João P. 1 Mengshoel, Ole J. 1 Morgado, António 1 Nagamochi, Hiroshi 1 Nonobe, Koji 1 Palubeckis, Gintaras 1 Planes, Jordi 1 Roth, Dan 1 Senko, Ján 1 Wilkins, David C. 1 Xing, Zhao 1 Yagiura, Mutsunori 1 Zhang, Weixiong all top 5 Cited in 12 Serials 2 Artificial Intelligence 2 Journal of Automated Reasoning 2 Constraints 1 Applied Mathematics and Computation 1 International Journal of Approximate Reasoning 1 Mathematical Programming. Series A. Series B 1 The Journal of Artificial Intelligence Research (JAIR) 1 Annals of Mathematics and Artificial Intelligence 1 Journal of Heuristics 1 JMMA. Journal of Mathematical Modelling and Algorithms 1 Journal of Applied Logic 1 Encyclopedia of Mathematics and Its Applications all top 5 Cited in 6 Fields 15 Computer science (68-XX) 8 Operations research, mathematical programming (90-XX) 2 Mathematical logic and foundations (03-XX) 1 General and overarching topics; collections (00-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year