Analysis and Solving SAT and MAX‐SAT Problems Using an L‐partition Approach

Analysis and Solving SAT and MAX‐SAT Problems Using an L‐partition Approach

0.00 Avg rating0 Votes
Article ID: iaor20134017
Volume: 12
Issue: 2
Start Page Number: 201
End Page Number: 212
Publication Date: Jun 2013
Journal: Journal of Mathematical Modelling and Algorithms in Operations Research
Authors: , ,
Keywords: programming: integer
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.

Reviews

Required fields are marked *. Your email address will not be published.