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 ...
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 ...
Survey of mycotoxins in beer and exposure assessment through the consumption of commercially available beer in Lleida, Spain Pascari, Xenia; Ortiz-Solá, Jordi; Marín Sillué, Sònia; Ramos Girona, Antonio J.; Sanchís Almenar, Vicente (Elsevier, 2018)A multianalyte method, using a MS/MS detector, was applied for a simultaneous determination of 23 mycotoxins in 64 beer products purchased from the supermarket in Lleida, Spain. The samples varied by their origin, brewing ...