Two paradigms for combining optimization and satisfiability : Maximum satisfiability and optimum satisfiability problems
Anna Konovalenkoanna.konovalenko@himolde.noFaculty of LogisticsMolde University CollegeMolde, P. O. Box 2110, N-6402, NorwayView full profile → , *Lars Magnus HvattumCorresponding authorhvattum@himolde.noFaculty of LogisticsMolde University CollegeMolde, P. O. Box 2110, N-6402, NorwayView full profile → , Sebastián Urrutiasebastian.urrutia@himolde.noFaculty of LogisticsMolde University CollegeMolde, P. O. Box 2110, N-6402, NorwayView full profile →
* Corresponding author · click or hover a name for details
- Received:
- 08 Nov 2022
- Published Online:
- 03 Feb 2025
- Article type:
- Research Article
- Language:
- EN
- Article no.:
- JIOS-1392
- Pages:
- 399–427
Abstract
Keywords
Subject Classifications
References
[1] J. Argelich, C. M. Li, F. Manyà, and J. Planes, “The first and second Max-SAT evaluations,” Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, pp. 251–278 (2008).
[2] D. L. Berre and A. Parrain, “The SAT4J library, release 2.2,” Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, pp. 59–64 (2010).
[3] J. Coelho and M. Vanhoucke, “Multi-mode resource-constrained project scheduling using RCPSP and SAT solvers,” European Journal of Operational Research, vol. 213, pp. 73–82, Aug. (2011), doi: 10.1016/j.ejor.2011.03.019.
[4] S. A. Cook, “The complexity of theorem-proving procedures,” in Proc. Third ACM Symp. Theory Comput., pp. 151–158 (1971).
[5] R. da Silva, L. M. Hvattum, and F. Glover, “Combining solutions of the optimum satisfiability problem using evolutionary tunneling,” MENDEL, vol. 26, pp. 23–29, May (2020), doi: 10.13164/mendel.2020.1.023.
[6] T. Davoine, P. L. Hammer, and B. Vizvári, “A heuristic for Boolean optimization problems,” Journal of Heuristics, vol. 9, pp. 229–247 (2003).
[7] L. Fang and M. S. Hsiao, “A fast approximation algorithm for MINONE SAT and its application on MAX-SAT solving,” in Adv. Techniques Logic Synthesis, Optimizations and Applications, pp. 149–170, Springer (2011.
[8] Z. Fu and S. Malik, “Solving the minimum-cost satisfiability problem using SAT-based branch-and-bound search,” in Proc. 2006 IEEE/ACM Int. Conf. Comput. Aided Design, pp. 852–859 (2006).
[9] Z. Fu and S. Malik, “On solving the partial MAX-SAT problem,” in Theory and Applications of Satisfiability Testing - SAT 2006, A. Biere and C. P. Gomes, Eds., Berlin, Heidelberg: Springer, pp. 252–265 (2006).
[10] F. Glover and M. Laguna, Tabu Search, Kluwer Academic Publisher, Boston, Dordrecht, London (1997).
[11] P. Großmann, S. Hölldobler, M. Norbert, K. Nachtigall, J. Opitz, and P. Steinke, “Solving periodic event scheduling problems with SAT,” in Adv. Research Appl. Artif. Intell., J. He, D. Wei, A. Moonis, and W. Xindong, Eds., Berlin, Heidelberg: Springer, pp. 166–175 (2012).
[12] S. Guo, W. Sun, and M. A. Weiss, “Solving satisfiability and implication problems in database systems,” ACM Trans. Database Systems, vol. 21, no. 2, pp. 270–293 (1996), doi: 10.1145/232616.232692.
[13] G. D. Hachtel and F. Somenzi, Logic Synthesis and Verification Algorithms, 1st ed. Kluwer Academic Publishers, USA (2000), ISBN 0792397460.
[14] J. Homer and X. Ou, “SAT-solving approaches to context-aware enterprise network security management,” IEEE Journal on Selected Areas in Communications, vol. 27, pp. 315–322, May (2009), doi: 10.1109/JSAC.2009.090407.
[15] H. H. Hoos and T. Stützle, “SATLIB: An online resource for research on SAT,” in SAT2000, I. P. Gent, H. van Maaren, and T. Walsh, Eds., IOS Press, pp. 283–292 (2000).
[16] L. M. Hvattum, A. Løkketangen, and F. Glover, “Adaptive memory search for Boolean optimization problems,” Discrete Applied Mathematics, vol. 142, pp. 99–109 (2004).
[17] L. M. Hvattum, A. Løkketangen, and F. Glover, “New heuristics and adaptive memory procedures for Boolean optimization problems,” in Integer Programming: Theory and Practice, J. Karlof, Ed., CRC Press, Boca Raton, FL, pp. 1–18 (2006).
[18] F. Imeson and S. L. Smith, “A language for robot path planning in discrete environments: the TSP with Boolean satisfiability constraints,” in Proc. IEEE Int. Conf. Robotics Automation (ICRA), pp. 5772–5777 (2014), doi: 10.1109/ICRA.2014.6907707.
[19] S. Joshi, P. Kumar, V. Manquinho, R. Martins, A. Nadel, and S. Rao, “Open-WBO-Inc in MaxSAT evaluation 2018,” in MaxSAT Evaluation 2018: Solver and Benchmark Descriptions, F. Bacchus, J. Berg, M. Järvisalo, and R. Martins, Eds., vol. B-2018-2, Department of Computer Science, University of Helsinki, Finland, pp. 16–17 (2018).
[20] S. Joshi, P. Kumar, S. Rao, and R. Martins, “Open-WBO-Inc: Approximation strategies for incomplete weighted MaxSAT,” Journal on Satisfiability, Boolean Modeling and Computation, vol. 11, pp. 73–97, Sept. (2019), doi: 10.3233/SAT190118.
[21] S. Joshi, P. Kumar, S. Rao, and R. Martins, “Open-WBO-Inc in MaxSAT evaluation 2020,” in MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, F. Bacchus, J. Berg, M. Järvisalo, and R. Martins, Eds., vol. B-2020-2, Department of Computer Science, University of Helsinki, Finland, pp. 24–25 (2020).
[22] Z. Lei and S. Cai, “Solving (weighted) partial MaxSAT by dynamic local search for SAT,” in Proc. Twenty-Seventh Int. Joint Conf. Artificial Intelligence (IJCAI-18), pp. 1346–1352 (2018), doi: 10.24963/ijcai.2018/187.
[23] Z. Lei and S. Cai, “SATLike-c(w): solver description,” in MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, F. Bacchus, J. Berg, M. Järvisalo, and R. Martins, Eds., vol. B-2020-2, Department of Computer Science, University of Helsinki, Finland, p. 15 (2020).
[24] C. M. Li, Z. Zhu, F. Manyà, and L. Simon, “Minimum satisfiability and its applications,” in Proc. IJCAI’11, Barcelona, Catalonia, Spain, pp. 605–610 (2011), AAAI Press, ISBN 9781577355137.
[25] X. Y. Li, Optimization Algorithms for the Minimum-Cost Satisfiability Problem, Ph.D. dissertation, North Carolina State University, 2004, AAI3154233.
[26] V. Manquinho, J. Marques-Silva, and J. Planes, “Algorithms for weighted Boolean optimization,” (2009), ISBN 978-3-642-02776-5, doi: 10.1007/978-3-642-02777-2_45.
[27] J. Marques-Silva, J. Argelich, A. Graça, and I. Lynce, “Boolean lexicographic optimization: algorithms & applications,” Annals of Mathematics and Artificial Intelligence, vol. 62, pp. 317–343 (2011).
[28] J. P. Marques-Silva and K. A. Sakallah, “Boolean satisfiability in electronic design automation,” in Proc. 37th Annual Design Automation Conf. (DAC ’00), New York, NY, USA, pp. 675–680 (2000), Association for Computing Machinery, ISBN 1581131879, doi: 10.1145/337292.337611.
[29] A. Nadel, “TT-Open-WBO-Inc-20: an anytime MaxSAT solver entering MSE’20,” in MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, F. Bacchus, J. Berg, M. Järvisalo, and R. Martins, Eds., vol. B-2020-2, Department of Computer Science, University of Helsinki, Finland, pp. 32–33 (2020).
[30] A. Nadel, “Polarity and variable selection heuristics for SAT-based anytime MaxSAT,” Journal on Satisfiability, Boolean Modeling and Computation, vol. 12, pp. 17–22 (2020).
[31] A. Nadel, “On optimizing a generic function in SAT,” in Proc. 2020 Formal Methods in Computer Aided Design (FMCAD), pp. 205–213 (2020), doi: 10.34727/2020/isbn.978-3-85448-042-6_28.
[32] E. Niklas and S. Niklas, “An extensible SAT-solver,” in Theory and Applications of Satisfiability Testing, E. Giunchiglia and A. Tacchella, Eds., Springer Berlin Heidelberg, pp. 502–518 (2004), ISBN 978-3-540-24605-3.
[33] H. Pierre and J. Brigitte, “Algorithms for the maximum satisfiability problem,” Computing, vol. 44, no. 4, pp. 279–303, Apr. (1990), ISSN 0010-485X, doi: 10.1007/BF02241270.
[34] O. Roussel and V. Manquinho, Pseudo-Boolean and Cardinality Constraints, IOS Press, Netherlands (2020), ISBN 1586039296.
[35] M. Ruben, M. Vasco, and L. Inês, “Open-WBO: a modular MaxSAT solver,” in Theory and Applications of Satisfiability Testing - SAT 2014, S. Carsten and E. Uwe, Eds., Springer International Publishing, pp. 438–445 (2014), ISBN 978-3-319-09284-3.
[36] H. Xu, R. A. Rutenbar, and K. Sakallah, “Sub-SAT: A formulation for relaxed Boolean satisfiability with applications in routing,” in Proc. 2002 Int. Symposium on Physical Design (ISPD ’02), New York, NY, USA, pp. 182–187 (2002), Association for Computing Machinery, ISBN 1581134606.
[37] M. Zapletina, D. Zhukov, and S. V. Gavrilov, “Boolean satisfiability methods for modern computer-aided design problems in microelectronics,” Proceedings of Universities. ELECTRONICS, vol. 25, pp. 525–538, Dec. (2020), doi: 10.24151/1561-5405-2020-25-6-525-538.
