Abstract
We describe a preprocessor that incorporates a variable saturation procedure for Max-SAT, and provide empirical evidence that it improves the performance of some of the most successful state-of-the-art solvers on several partial (weighted) Max-SAT instances of the 2007 Max-SAT Evaluation.
This research was funded by the MEC research projects TIN2006-15662-C02-02 and TIN2007-68005-C04-04, and Acción Integrada HP2005-0147.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Alsinet, T., Manyà, F., Planes, J.: Improved exact solver for weighted Max-SAT. In: SAT-2005, pp. 371–377 (2005)
Argelich, J., Manyà, F.: Exact Max-SAT solvers for over-constrained problems. Journal of Heuristics 12(4–5), 375–392 (2006)
Argelich, J., Manyà, F.: Partial Max-SAT solvers with clause learning. In: SAT-2007, pp. 28–40 (2007)
Bonet, M.L., Levy, J., Manyà, F.: A complete calculus for Max-SAT. In: SAT-2006, pp. 240–251 (2006)
Bonet, M.L., Levy, J., Manyà, F.: Resolution for Max-SAT. Artificial Intelligence 171(8–9), 240–251 (2007)
Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: SAT-2006, pp. 252–265 (2006)
Heras, F., Larrosa, J.: New inference rules for efficient Max-SAT solving. In: AAAI-2006, pp. 68–73 (2006)
Heras, F., Larrosa, J., Oliveras, A.: MiniMaxSat: A new weighted Max-SAT solver. In: SAT-2007 (2007)
Larrosa, J., Heras, F.: Resolution in Max-SAT and its relation to local consistency in weighted CSPs. In: IJCAI-2005, pp. 193–198 (2005)
Li, C.M., Manyà, F., Planes, J.: Exploiting unit propagation to compute lower bounds in branch and bound Max-SAT solvers. In: CP-2005, pp. 403–414 (2005)
Li, C.M., Manyà, F., Planes, J.: Detecting disjoint inconsistent subformulas for computing lower bounds for Max-SAT. In: AAAI-2006, pp. 86–91 (2006)
Li, C.M., Manyà, F., Planes, J.: New inference rules for Max-SAT. Journal of Artificial Intelligence Research 30, 321–359 (2007)
Marques-Silva, J., Planes, J.: Algorithms for Maximum Satisfiability using Unsatisfiable Cores. In: DATE-2008 (2008)
Pipatsrisawat, K., Darwiche, A.: Clone: Solving weighted max-sat in a reduced search space. In: 20th Australian Joint Conf. on AI, AI-2007, pp. 223–233 (2007)
Ramírez, M., Geffner, H.: Structural relaxations by variable renaming and their compilation for solving MinCostSAT. In: CP-2007, pp. 605–619 (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Argelich, J., Li, C.M., Manyà, F. (2008). A Preprocessor for Max-SAT Solvers. In: Kleine Büning, H., Zhao, X. (eds) Theory and Applications of Satisfiability Testing – SAT 2008. SAT 2008. Lecture Notes in Computer Science, vol 4996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79719-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-79719-7_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79718-0
Online ISBN: 978-3-540-79719-7
eBook Packages: Computer ScienceComputer Science (R0)