Analysis and Solving SAT and MAX-SAT Problems Using an L-partition Approach |
| |
Authors: | Alexander Kolokolov Alexander Adelshin Darya Yagofarova |
| |
Institution: | 1. Omsk Branch of Sobolev Institute of Mathematics, Siberian Branch of Russian Academy of Sciences, 13, Pevtsov St., 644099, Omsk, Russia 2. Omsk F.M. Dostoevsky State University, 55a, Mira pr., 644077, Omsk, Russia
|
| |
Abstract: | In this paper, we study SAT and MAX-SAT using the integer linear programming models and L-partition approach. This approach can be applied to analyze and solve many discrete optimization problems including location, covering, scheduling problems. We describe examples of SAT and MAX-SAT families for which the cardinality of L-covering of the relaxation polytope grows exponentially with the number of variables. These properties are useful in analysis and development of algorithms based on the linear relaxation of the problems. Besides we present the L-class enumeration algorithm for SAT using the L-partition approach. In addition we consider an application of this algorithm to construct exact algorithm and local search algorithms for the MAX-SAT problem. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|