Core-Boosted Linear Search for Incomplete MaxSAT
| Autor: | Jeremias Berg, Peter J. Stuckey, Emir Demirović |
|---|---|
| Přispěvatelé: | Rousseau, Louis-Martin, Stergiou, Kostas, Department of Computer Science |
| Rok vydání: | 2019 |
| Předmět: |
021103 operations research
Theoretical computer science Computational complexity theory Computer science 0211 other engineering and technologies 02 engineering and technology Extension (predicate logic) 113 Computer and information sciences Satisfiability Scalability Maximum satisfiability problem Core (graph theory) 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Boolean satisfiability problem Linear search |
| Zdroj: | Integration of Constraint Programming, Artificial Intelligence, and Operations Research ISBN: 9783030192112 CPAIOR |
| DOI: | 10.1007/978-3-030-19212-9_3 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|