Journal
JOURNAL OF EXPERIMENTAL & THEORETICAL ARTIFICIAL INTELLIGENCE
Volume 27, Issue 5, Pages 673-701Publisher
TAYLOR & FRANCIS LTD
DOI: 10.1080/0952813X.2014.993508
Keywords
maximum satisfiability; linear search algorithms; model-based approaches; incrementality in MaxSAT
Categories
Ask authors/readers for more resources
Linear search algorithms have been shown to be particularly effective for solving partial Maximum Satisfiability (MaxSAT) problem instances. These algorithms start by adding a new relaxation variable to each soft clause and solving the resulting formula with a SAT solver. Whenever a Model is found, a new constraint on the relaxation variables is added such that Models with a greater or equal value are excluded. However, if the problem instance has a large number of relaxation variables, then adding a new constraint over these variables can lead to the exploration of a much larger search space. This article proposes new algorithms to improve the performance of linear search algorithms for MaxSAT by using Models found by the SAT solver to partition the relaxation variables. These algorithms add a new constraint on a subset of relaxation variables, thus intensifying the search on that subspace. In addition, the proposed algorithms are further enhanced by using incremental approaches where learned clauses are kept between calls to the SAT solver. Experimental results show that Model-based algorithms can outperform a classic linear search algorithm in several problem instances. Moreover, incremental approaches further improve the performance of linear search and Model-based algorithms for MaxSAT. Overall, Model-based algorithms are competitive with state-of-the-art MaxSAT solvers, and can improve their performance when solving problem instances with a large number of soft clauses.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available