As a guest user you are not logged in or recognized by your IP address. You have
access to the Front Matter, Abstracts, Author Index, Subject Index and the full
text of Open Access publications.
Motivated by the success of preprocessing in Boolean satisfiability (SAT) solving, development and analysis of preprocessing in maximum satisfiability (MaxSAT)—the optimization extension of SAT—has received noticeable attention recently. The correctness of preprocessing techniques for MaxSAT is standardly established by arguing that optimal solutions are maintained. However, the effects of preprocessing on the relative perceived costs of non-optimal solutions has not been considered, despite the fact that one of the most recent directions in MaxSAT research is developing incomplete solvers, i.e., solvers that are designed to provide good (but not necessarily optimal) solutions fast. In this paper, we bridge this gap by showing that employing central preprocessing techniques misleads MaxSAT solvers in terms of their interpretation of the costs of non-optimal solutions seen during search. This issue impacts both complete and incomplete solvers and the effects can be shown to be present also in practice with different types of MaxSAT solvers. Furthermore, we propose ideas for circumventing these negative effects in the context of stochastic local search algorithms for MaxSAT.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.