Core-Boosted Linear Search for Incomplete MaxSAT

Näytä kaikki kuvailutiedot



Pysyväisosoite

http://hdl.handle.net/10138/310651

Lähdeviite

Berg , O J , Demirović , E & Stuckey , P J 2019 , Core-Boosted Linear Search for Incomplete MaxSAT . in L-M Rousseau & K Stergiou (eds) , Integration of Constraint Programming, Artificial Intelligence, and Operations Research : 16th International Conference, CPAIOR 2019, Thessaloniki, Greece, June 4–7, 2019, Proceedings . Lecture Notes in Computer Science. Theoretical Computer Science and General Issues , vol. 11494 , Springer International Publishing AG , Cham , pp. 39-56 , 16th International Conference on Integration of AI and OR Techniques in Constraint Programming (CPAIOR 2019) , Thessaloniki , Greece , 04/06/2019 . https://doi.org/10.1007/978-3-030-19212-9_3

Julkaisun nimi: Core-Boosted Linear Search for Incomplete MaxSAT
Tekijä: Berg, Otto Jeremias; Demirović, Emir; Stuckey, Peter J.
Muu tekijä: Rousseau, Louis-Martin
Stergiou, Kostas
Tekijän organisaatio: Department of Computer Science
Julkaisija: Springer International Publishing AG
Päiväys: 2019-06
Kieli: eng
Sivumäärä: 18
Kuuluu julkaisusarjaan: Integration of Constraint Programming, Artificial Intelligence, and Operations Research
Kuuluu julkaisusarjaan: Lecture Notes in Computer Science. Theoretical Computer Science and General Issues
ISBN: 978-3-030-19211-2
978-3-030-19212-9
ISSN: 0302-9743
DOI-tunniste: https://doi.org/10.1007/978-3-030-19212-9_3
URI: http://hdl.handle.net/10138/310651
Tiivistelmä: Maximum Satisfiability (MaxSAT), the optimisation extension of the well-known Boolean Satisfiability (SAT) problem, is a competitive approach for solving NP-hard problems encountered in various artificial intelligence and industrial domains. Due to its computational complexity, there is an inherent tradeoff between scalability and guarantee on solution quality in MaxSAT solving. Limitations on available computational resources in many practical applications motivate the development of complete any-time MaxSAT solvers, i.e. algorithms that compute optimal solutions while providing intermediate results. In this work, we propose core-boosted linear search, a generic search-strategy that combines two central approaches in modern MaxSAT solving, namely linear and core-guided algorithms. Our experimental evaluation on a prototype combining reimplementations of two state-of-the-art MaxSAT solvers, PMRES as the core-guided approach and LinSBPS as the linear algorithm, demonstrates that our core-boosted linear algorithm often outperforms its individual components and shows competitive and, on many domains, superior results when compared to other state-of-the-art solvers for incomplete MaxSAT solving.
Avainsanat: 113 Computer and information sciences
Vertaisarvioitu: Kyllä
Pääsyrajoitteet: openAccess
Rinnakkaistallennettu versio: acceptedVersion


Tiedostot

Latausmäärä yhteensä: Ladataan...

Tiedosto(t) Koko Formaatti Näytä
CPAIOR_coreBoostedLinearAlgorithm.tex 60.23KB TeX Avaa tiedosto

Viite kuuluu kokoelmiin:

Näytä kaikki kuvailutiedot