Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms
The MaxSAT problem and some of its well-known variants find an increasing number of practical applications in a wide range of areas. Examples include different optimization problems in system design and verification. However, most MaxSAT problem instances
- PDF / 256,172 Bytes
- 6 Pages / 430 x 660 pts Page_size
- 40 Downloads / 177 Views
Abstract. The MaxSAT problem and some of its well-known variants find an increasing number of practical applications in a wide range of areas. Examples include different optimization problems in system design and verification. However, most MaxSAT problem instances from these practical applications are too hard for existing branch and bound algorithms. One recent alternative to branch and bound MaxSAT algorithms is based on unsatisfiable subformula identification. A number of different unsatisfiability-based MaxSAT algorithms have been developed, which are effective at solving different classes of problem instances. All MaxSAT algorithms based on unsatisfiable subformula identification require using additional Boolean variables, either to allow relaxing some of the clauses or to encode cardinality constraints used by these algorithms. As a result, these algorithms may require using a significant number of additional Boolean variables, that can exceed the original number of variables for some problem instances. This paper proposes techniques for effectively reducing the number of auxiliary variables that must be used in unsatisfiability-based MaxSAT algorithms. Experimental results indicate that the techniques for reducing the number of auxiliary variables are effective, and contribute to more efficient MaxSAT algorithms.
1 Introduction Maximum Satisfiability (MaxSAT) and variants allow modeling an increasingly large number of optimization problems in an also growing number of practical settings. The recent application of MaxSAT and variants in design debugging and verification of complex designs [11, 4, 5] motivated the development of new MaxSAT algorithms, capable of solving large structured problem instances common to these application domains. Despite the significant improvements made in recent years to standard branch and bound MaxSAT algorithms, in practice existing branch and bound algorithms are unable to solve the vast majority of problem instances from practical applications. One recent promising line of research is the development of MaxSAT solvers based on the identification of unsatisfiable subformulas (or cores) [4, 8, 9]. These MaxSAT algorithms are built on top of SAT solvers, and so can exploit the most effective SAT techniques [2]. Moreover, these algorithms rely extensively on the ability of modern SAT solvers for producing certificates of unsatisfiability [12]. Even though the organization of existing unsatisfiability-based MaxSAT algorithms is fairly different, these algorithms also share a number of key common characteristics. For example, all unsatisfiability-based MaxSAT algorithms iteratively identify and relax unsatisfiable subformulas. The approach for relaxing unsatisfiable subformulas is well-known H. Kleine B¨uning and X. Zhao (Eds.): SAT 2008, LNCS 4996, pp. 225–230, 2008. c Springer-Verlag Berlin Heidelberg 2008
226
J. Marques-Silva and V. Manquinho
(e.g. see [8] for an overview), and consists of adding relaxing (or blocking) variables to each clause in each identified unsatisf
Data Loading...
