Linear programs for constraint satisfaction problems

A novel representation is described that models some important NP-hard problems, such as the propositional satisfiability problem (SAT), the Traveling Salesperson Problem (TSP), the Quadratic Assignment Problem (QAP), and the Minimal Set Covering Problem (MSCP) by means of only two types of constraints: ‘choice constraints’ and ‘exclusion constraints’. In its main section the paper presents an approach for solving an m-CNF-SAT problem (Conjunctive Normal Form Satisfaction: n variables, p clauses, clause length m) by integer programming. The approach is unconventional, because 2n distinct 0–1 variables are used for each clause of the m-CNF-SAT problem. The constraint matrix A forces that for every clause exactly one 0–1 variable is set equal to 1 (choice constraint), and no two 0–1 variables, representing a literal and its complement, are both set equal to 1 (exclusion constraints). The particular m-CNF-SAT instance is coded in a cost vector, which serves for maximization of the number of satisfied clauses. The paper presents a modification of the Simplex for solving the obtained integer program. A main theorem of the paper is that this algorithm always finds a 0–1 integer solution. A solution of the integer program corresponds to a solution of the m-CNF-SAT and vice versa. The results of significant experimental tests are reported, and the procedure is compared to other approaches. The same modelling technique is then used for the Traveling Salesperson Problem, for the Minimal Set Covering, and for the Quadratic Assignment Problem: it is shown that a uniform approach is thus useful.