Stochastic local search for Partial Max-SAT: an experimental evaluation
- PDF / 2,138,747 Bytes
- 42 Pages / 439.37 x 666.142 pts Page_size
- 105 Downloads / 192 Views
Stochastic local search for Partial Max‑SAT: an experimental evaluation Haifa Hamad AlKasem1 · Mohamed El Bachir Menai1 Accepted: 6 September 2020 © Springer Nature B.V. 2020
Abstract Stochastic local search (SLS) methods are heuristic-based algorithms that have gained in popularity for their efficiency and robustness when solving very large and complex problems from various areas of artificial intelligence. This study aims to gain insights into SLS methods for solving the Partial Max-SAT (PMSAT) problem. The PMSAT is an NPHard problem, an optimization variant of the Propositional Boolean Satisfiability (SAT) problem, that has importance in theory and practice. Many real-world problems including timetabling, scheduling, planning, routing, and software debugging can be reduced to the PMSAT problem. Modern PMSAT solvers are able to solve practical instances with hundreds of thousands to millions of variables and clauses. However, performance of PMSAT solvers are still limited for solving some benchmark instances. In this paper, we present, investigate, and analyze state-of-the-art SLS methods for solving the PMSAT problem. An experimental evaluation is presented based on the MAX-SAT evaluations from 2014 to 2019. The results of this evaluation study show that the currently best performing SLS methods for the PMSAT problem fall into three categories: distinction-based, configuration checking-based, and dynamic local search methods. Very good performance was reported for the dynamic local search based method. The paper gives a detailed picture of the performance of SLS solvers for the PMSAT problem, aims to improve our understanding of their capabilities and limitations, and identifies future research directions. Keywords Boolean satisfiability · Partial Max-SAT · Max-SAT · Stochastic local search · Incomplete solver · Max-SAT evaluation
* Haifa Hamad AlKasem [email protected] * Mohamed El Bachir Menai [email protected] 1
Department of Computer Science, College of Computer and Information Sciences, King Saud University, Riyadh, Saudi Arabia
13
Vol.:(0123456789)
H. H. AlKasem, M. E. B. Menai
1 Introduction The Propositional Boolean Satisfiability (SAT) problem is a fundamental problem in computer science and artificial intelligence (Cook 1971; Garey and Johnson 1979). It has been widely studied due to its importance in theory and practice (Kautz et al. 2009; Alouneh et al. 2018). The SAT problem is the first decision problem proven to be an NP-complete by Cook in 1971 (Cook 1971). The SAT asks whether the variables of a given Boolean formula can be assigned Boolean values such that the formula evaluates to true. The few past years have seen enormous progress in the performance of SAT solvers in various practical applications such as verification and model checking (Alouneh et al. 2018), planning (Vallati et al. 2013), and scheduling (Horbach et al. 2012). The Partial Max-SAT (PMSAT) problem is an optimization variant of the SAT problem; it is classified as an NP-hard problem. The PMSAT problem is impo
Data Loading...
