Iterative and core-guided MaxSAT solving: A survey and assessment
MetadataShow full item record
Maximum Satisfiability (MaxSAT) is an optimization version of SAT, and many real world applications can be naturally encoded as such. Solving MaxSAT is an important problem from both a theoretical and a practical point of view. In recent years, there has been considerable interest in developing efficient algorithms and several families of algorithms have been proposed. This paper overviews recent approaches to handle MaxSAT and presents a survey of MaxSAT algorithms based on iteratively calling a SAT solver which are particularly effective to solve problems arising in industrial settings. First, classic algorithms based on iteratively calling a SAT solver and updating a bound are overviewed. Such algorithms are referred to as iterative MaxSAT algorithms. Then, more sophisticated algorithms that additionally take advantage of unsatisfiable cores are described, which are referred to as core-guided MaxSAT algorithms. Core-guided MaxSAT algorithms use the information provided by unsatisfiable cores to relax clauses on demand and to create simpler constraints. Finally, a comprehensive empirical study on non-random benchmarks is conducted, including not only the surveyed algorithms, but also other state-of-the-art MaxSAT solvers. The results indicate that (i) core-guided MaxSAT algorithms in general abort in less instances than classic solvers based on iteratively calling a SAT solver and that (ii) core-guided MaxSAT algorithms are fairly competitive compared to other approaches.
Is part ofConstraints, 2013, vol. 18, núm. 4, p. 478-534
European research projects
Showing items related by title, author, creator and subject.
Marques-Silva, Joao; Argelich Romà, Josep; Graça, Ana; Lynce, Inês (Springer Verlag, 2011)Multi-Objective Combinatorial Optimization (MOCO) problems find a wide range of practical application problems, some of which involving Boolean variables and constraints. This paper develops and evaluates algorithms for ...
Gibert Llauradó, Daniel; Mateu Piñol, Carles; Planes Cid, Jordi; Marques-Silva, Joao (Elsevier, 2021)Malicious software is one of the most serious cyber threats on the Internet today. Traditional malware detection has proven unable to keep pace with the sheer number of malware because of their growing complexity, new ...
de Hollanda, Ana; Lecube Torelló, Albert; Rubio, Miguel Ángel; Sánchez Peña, Enric; Vilarrasa, Núria; Gregorio Oliva, José; Fernández-Soto, María Luisa; Salas-Salvadó, Jordi; Ballesteros-Pomar, María D.; Ciudin, Andreea; Torres, Ferran; Vidal, Concepción; Morales, María José; Valdés, Sergio; Pellitero, Silvia; Miñambres, Inka; Masmiquel, Lluís; Goday, Albert; Suarez, Lorena; Flores, Liliam; Bueno Díez, Marta; Caixàs, Assumpta; Bretón, Irene; Cámara, Rosa; Olbeyra, Romina; Penso, Rona; de la Cruz, María José; Simó-Servat, Andreu; Pereyra-García, Francisca María; López-Mezquita, Elena Teresa; Gils, Anna; Fidilio, Enzamaria; Bandrés, Orosia; Martínez, Ángel; Abuín, Jose; Marques-Pamies, Montserrat; Tuneu, Laura; Arteaga, Magdalena; Castañer, Olga; Goñi, Fernando; Arrizabalaga, Cristina; Botana, Manuel Antonio; Calañas, Alfonso (MDPI, 2020)Almost one third of patients do not achieve type 2 diabetes remission after bariatric surgery or are unable to sustain this effect long term. Our objective was to delve further into the dynamic responses of diabetes after ...