An Efficient Method to Transform SAT problems to Binary Integer Linear Programming Problem

TL;DR

This paper introduces LIMSAT, an efficient method for transforming large SAT problems into mixed integer linear programming models, enabling solutions for problems with thousands of variables and clauses.

Contribution

The paper proposes LIMSAT, a novel linear inequality model-based approach that efficiently converts large SAT problems into MILP, surpassing previous size limitations.

Findings

LIMSAT can handle SAT problems with thousands of variables and clauses.

The method outperforms existing approaches in efficiency for large-scale problems.

LIMSAT is validated on up-to-date benchmark problems.

Abstract

In computational complexity theory, a decision problem is NP-complete when it is both in NP and NP-hard. Although a solution to a NP-complete can be verified quickly, there is no known algorithm to solve it in polynomial time. There exists a method to reduce a SAT (Satifiability) problem to Subset Sum Problem (SSP) in the literature, however, it can only be applied to small or medium size problems. Our study is to find an efficient method to transform a SAT problem to a mixed integer linear programming problem in larger size. Observing the feature of variable-clauses constraints in SAT, we apply linear inequality model (LIM) to the problem and propose a method called LIMSAT. The new method can work efficiently for very large size problem with thousands of variables and clauses in SAT tested using up-to-date benchmarks.