An empirical study for satisfiability problems in propositional logic using set covering formulation

A satisfiability problem in propositional logic is the problem of checking for the existence of a set of truth values of atomic proportions that renders an input propositional formula true. This paper describes an empirical investigation of a particular integer programming approach, using the set covering model, to solve satisfiability problems. Our satisfiability engine, SETSAT, is a fully integrated linear programming based, branch and bound method using various symbolic routines for the reduction of the logic formulas. SETSAT has been implemented in the integer programming shell MINTO which, in turn, uses the CPLEX linear programming system. The logic processing routines were written in C and integrated into the MINTO functions. The experiments were conducted on a benchmark set of satisfiability problems that were compiled at the University of Ulm in Germany. The computational results indicate that our approach is competitive with the state of the art.