Core-Boosted Linear Search for Incomplete MaxSAT

Show simple item record

dc.contributor.author Berg, Otto Jeremias
dc.contributor.author Demirović, Emir
dc.contributor.author Stuckey, Peter J.
dc.contributor.editor Rousseau, Louis-Martin
dc.contributor.editor Stergiou, Kostas
dc.date.accessioned 2020-01-30T09:34:01Z
dc.date.available 2020-01-30T09:34:01Z
dc.date.issued 2019-06
dc.identifier.citation 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
dc.identifier.citation conference
dc.identifier.other PURE: 122031948
dc.identifier.other PURE UUID: 4a39754d-a8fa-4aa5-b37f-59944af6923e
dc.identifier.uri http://hdl.handle.net/10138/310651
dc.description.abstract 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. en
dc.format.extent 18
dc.language.iso eng
dc.publisher Springer International Publishing AG
dc.relation.ispartof Integration of Constraint Programming, Artificial Intelligence, and Operations Research
dc.relation.ispartofseries Lecture Notes in Computer Science. Theoretical Computer Science and General Issues
dc.relation.isversionof 978-3-030-19211-2
dc.relation.isversionof 978-3-030-19212-9
dc.rights.uri info:eu-repo/semantics/openAccess
dc.subject 113 Computer and information sciences
dc.title Core-Boosted Linear Search for Incomplete MaxSAT en
dc.type Conference contribution
dc.contributor.organization Department of Computer Science
dc.description.reviewstatus Peer reviewed
dc.relation.doi https://doi.org/10.1007/978-3-030-19212-9_3
dc.relation.issn 0302-9743
dc.rights.accesslevel openAccess
dc.type.version acceptedVersion
dc.identifier.url https://www.springer.com/gp/book/9783030192112

Files in this item

Total number of downloads: Loading...

Files Size Format View
CPAIOR_coreBoostedLinearAlgorithm.tex 60.23Kb TeX View/Open

This item appears in the following Collection(s)

Show simple item record