Abstract
Many decision and optimization problems in electronic design automation (EDA) can be solved with Boolean satisfiability (SAT). These include binate covering problem (BCP), pseudo-Boolean optimization (PBO), quantified Boolean formulas (QBF), multi-valued SAT, and, more recently, maximum satisfiability (MaxSAT). The first generation of MaxSAT algorithms are known to be fairly inefficient in industrial settings, in part because the most effective SAT techniques cannot be easily extended to MaxSAT. This chapter proposes a novel algorithm for MaxSAT that improves existing state-of-the-art solvers by orders of magnitude on industrial benchmarks. The new algorithm exploits modern SAT solvers, being based on the identification of unsatisfiable subformulas. Moreover, the new algorithm provides additional insights between unsatisfiable subformulas and the maximum satisfiability problem.
Based on Marques-Silva, J.; Planes, J.: “Algorithms for maximum satisfiability using unsatisfiable cores,” Design, Automation and Test in Europe, 2008. DATE ’08, pp. 408–413, 10–14 March 2008 Doi: 10.1109/DATE.2008.4484715 © [2008] IEEE.
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
Ansótegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial MaxSAT through satisfiability testing. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 427–440. Swansea, UK (2009)
Ansótegui, C., Bonet, M.L., Levy, J.: A new algorithm for weighted partial MaxSAT. In: National Conference on Artificial Intelligence. Atlanta, USA (2010)
Argelich, J., Li, C.M., Manyá, F., Planes, J.: MaxSAT evaluation. http://www.maxsat07.udl.es/ (2008)
Argelich, J., Li, C.M., Manyá, F., Planes, J.: The first and second Max-SAT evaluations. Journal on Satisfiability, Boolean Modeling and Computation 4, 251–278 (2008)
Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality networks and their applications. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 167–180. Swansea, UK (2009)
de la Banda, M.G., Stuckey, P.J., Wazny, J.: Finding all minimal unsatisfiable sub-sets. In: International Conference on Principles and Practice of Declarative Programming, pp. 32–43. Uppsala, Sweden (2003)
Berre, D.L., Simon, L., Roussel, O.: SAT competition. http://www.satcompetition.org/ (2008)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 193–207. (1999)
Bonet, M.L., Levy, J., Manyá, F.: Resolution for Max-SAT. Artificial Intelligence 171(8–9), 606–618 (2007)
Bordeaux, L., Hamadi, Y., Zhang, L.: Propositional satisfiability and constraint programming: A comparative survey. ACM Computing Surveys 38(4) (2006)
Chen, Y., Safarpour, S., Veneris, A.G., Marques-Silva, J.: Spatial and temporal design debug using partial MaxSAT. In: ACM Great Lakes Symposium on VLSI, pp. 345–350. Boston, USA (2009)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM 5, 394–397 (1962)
Dershowitz, N., Hanna, Z., Katz, J.: Bounded model checking with QBF. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 408–414. St. Andrews, UK (2005)
Een, N., Sörensson, N.: An extensible SAT solver. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 502–518. Santa Margherita Ligure, Italy (2003)
Een, N., Sörensson, N.: Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation 2, 1–26 (2006)
Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 252–265. Seattle, USA (2006)
Heras, F., Larrosa, J., Oliveras, A.: MiniMaxSat: a new weighted Max-SAT solver. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 41–55. Lisbon, Portugal (2007)
Hoos, H., Stützle, T.: SAT lib. http://www.satlib.org/ (2008)
Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Transactions on CAD of Integrated Circuits and Systems 21(12), 1377–1394 (2002)
Kullmann, O.: Investigations on autark assignments. Discrete Applied Mathematics 107(1–3), 99–137 (2000)
Kullmann, O.: Lean clause-sets: generalizations of minimally unsatisfiable clause-sets. Discrete Applied Mathematics 130(2), 209–249 (2003)
Li, C.M., Manyá, F., Planes, J.: Detecting disjoint inconsistent subformulas for computing lower bounds for Max-SAT. In: National Conference on Artificial Intelligence, pp. 86–91. Boston, USA (2006)
Li, C.M., Manyá, F., Planes, J.: New inference rules for Max-SAT. Journal of Artificial Intelligence Research 30, 321–359 (2007)
Liffiton, M.H., Sakallah, K.A.: On finding all minimally unsatisfiable subformulas. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 173–186. (2005)
Liffiton, M.H., Sakallah, K.A.: Generalizing core-guided max-sat. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 481–494. Swansea, UK (2009)
Liu, C., Kuehlmann, A., Moskewicz, M.W.: CAMA: A multi-valued satisfiability solver. In: International Conference on Computer-Aided Design, pp. 326–333. San Jose, USA (2003)
Mangassarian, H., Veneris, A.G., Safarpour, S., Najm, F.N., Abadir, M.S.: Maximum circuit activity estimation using pseudo-Boolean satisfiability. In: Design, Automation and Testing in Europe Conference, pp. 1538–1543. Nice, France (2007)
Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for weighted Boolean optimization. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 495–508. Swansea, UK (2009)
Marques-Silva, J., Manquinho, V.: Towards more effective unsatisfiability-based maximum satisfiability algorithms. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 225–230. Guangzhou, China (2008)
Marques-Silva, J., Planes, J.: On using unsatisfiability for solving maximum satisfiability. http://arxiv.org/corr/ (2007)
Marques-Silva, J., Planes, J.: Algorithms for maximum satisfiability using unsatisfiable cores. In: Design, Automation and Testing in Europe Conference, pp. 408–413. Munich, Germany (2008)
McMillan, K.L.: Interpolation and SAT-based model checking. In: Computer-Aided Verification, pp. 1–13. Boulders, USA (2003)
Safarpour, S., Mangassarian, H., Veneris, A.G., Liffiton, M.H., Sakallah, K.A.: Improved design debugging using maximum satisfiability. In: Formal Methods in Computer-Aided Design, pp. 13–19. Austin, USA (2007)
Smith, A., Veneris, A.G., Ali, M.F., Viglas, A.: Fault diagnosis and logic debugging using Boolean satisfiability. IEEE Transactions on CAD of Integrated Circuits and Systems 24(10), 1606–1621 (2005)
Sülflow, A., Fey, G., Bloem, R., Drechsler, R.: Using unsatisfiable cores to debug multiple design errors. In: ACM Great Lakes Symposium on VLSI, pp. 77–82. Orlando, USA (2008)
Wang, K.H., Chan, C.M.: Incremental learning approach and SAT model for Boolean matching with don’t cares. In: International Conference on Computer-Aided Design, pp. 234–239. San Jose, USA (2007)
Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: Design, Automation and Testing in Europe Conference. Munich, Germany (2003)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer Science+Business Media, LLC
About this chapter
Cite this chapter
Marques-Sila, J., Planes, J. (2011). Algorithms for Maximum Satisfiability Using Unsatisfiable Cores. In: Gulati, K. (eds) Advanced Techniques in Logic Synthesis, Optimizations and Applications. Springer, New York, NY. https://doi.org/10.1007/978-1-4419-7518-8_10
Download citation
DOI: https://doi.org/10.1007/978-1-4419-7518-8_10
Published:
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4419-7517-1
Online ISBN: 978-1-4419-7518-8
eBook Packages: EngineeringEngineering (R0)