Abstract
Boolean Satisfiability (SAT) has seen many successful applications in various fields such as Electronic Design Automation and Artificial Intelligence. However, in some cases, it may be required/preferable to use variations of the general SAT problem. In this paper, we consider one important variation, the Partial MAX-SAT problem. Unlike SAT, Partial MAX-SAT has certain constraints (clauses) that are marked as relaxable and the rest are hard, i.e. non-relaxable. The objective is to find a variable assignment that satisfies all non-relaxable clauses together with the maximum number of relaxable ones. We have implemented two solvers for the Partial MAX-SAT problem using a contemporary SAT solver, zChaff. The first approach is a novel diagnosis based algorithm; it iteratively analyzes the UNSAT core of the current SAT instance and eliminates the core through a modification of the problem instance by adding relaxation variables. The second approach is encoding based; it constructs an efficient auxiliary counter that constrains the number of relaxed clauses and supports binary search or linear scan for the optimal solution. Both solvers are complete as they guarantee the optimality of the solution. We discuss the relative strengths and thus applicability of the two solvers for different solution scenarios. Further, we show how both techniques benefit from the persistent learning techniques of incremental SAT. Experiments using practical instances of this problem show significant improvements over the best known solvers.
This research is supported by a grant from the Air Force Research Laboratory.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Argelich, J., Manyà, F.: Solving Over-Constrained Problems with SAT Technology. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 1–15. Springer, Heidelberg (2005)
Cha, B., Iwama, K., Kambayashi, Y., Miyazaki, S.: Local search algorithms for partial MAXSAT. In: Proceedings of the Fourteenth National Conference on Artificial Intelligence, pp. 263–268 (1997)
Coudert, O.: On solving covering problems. In: Proceedings of the 33rd Design Automation Conference, pp. 197–202 (1996)
Eén, N., Sörensson, N.: MiniSat – A SAT solver with conflict-clause minimization. In: Proceedings of the International Symposium on the Theory and Applications of Satisfiability Testing (2005)
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-completeness. Freemand & Co., New York (1979)
Goldberg, E., Novikov, Y.: Berkmin: A fast and robust SAT solver. In: Proceedings of the Design Automation and Test in Europe, pp. 142–149 (2002)
ILOG. Cplex (2006), http://www.ilog.com/products/cplex/
Johnson, D.S.: Approximation algorithms for combinatorial problems. Journal of Computer and System Sciences 9, 256–278 (1974)
Katz, R.H.: Contemporary Logic Design. Benjamin Cummings/Addison Wesley Publishing Company (1993)
Kautz, H., Selman, B., Jiang, Y.: A general stochastic approach to solving problems with hard and soft constraints. In: Du, D., Gu, J., Pardalos, P.M. (eds.) The Satisfiability Problem: Theory and Applications (1996)
Koren, I.: Computer Arithmetic Algorithms. Prentice-Hall, Englewood Cliffs (1993)
Li, X.Y.: Optimization Algorithms for the Minimum-Cost Satisfiability Problem. PhD thesis, Department of Computer Science, North Carolina State University, Raleigh, North Carolina, 162 pages (2004)
Manquinho, V., Marques-Silva, J.: Search pruning techniques in SAT-based branch-and-bound algorithms for the binate covering problem. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 21, 505–516 (2002)
Marques-Silva, J., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers 48, 506–521 (1999)
Miyazaki, S., Iwama, K., Kambayashi, Y.: Database queries as combinatorial optimization problems. In: Proceedings of the International Symposium on Cooperative Database Systems for Advanced Applications, pp. 448–454 (1996)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (2001)
Ryan, L.: Efficient algorithms for clause-learning SAT solvers. Master’s thesis, Simon Fraser University (2004)
Strichman, O.: Prunning techniques for the SAT-based bounded model checking problem. In: Proceedings of the 11th Conference on Correct Hardware Design and Verification Methods (2001)
Velev, M.: Sat benchmarks (2006), http://www.ece.cmu.edu/~mvelev/
Xu, H.: subSAT: A Formulation for Relaxed Satisfiability and its Applications. PhD thesis, Department of Electrical and Computer Engineering, Carnegie Mellon University, Pittsburgh, Pennsylvania, 160 pages (2004)
Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: Proceedings of the Design Automation and Test in Europe (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fu, Z., Malik, S. (2006). On Solving the Partial MAX-SAT Problem. In: Biere, A., Gomes, C.P. (eds) Theory and Applications of Satisfiability Testing - SAT 2006. SAT 2006. Lecture Notes in Computer Science, vol 4121. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11814948_25
Download citation
DOI: https://doi.org/10.1007/11814948_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37206-6
Online ISBN: 978-3-540-37207-3
eBook Packages: Computer ScienceComputer Science (R0)