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 t wo types of constraints: 'choice constraints' and 'exclusion constrain ts'. 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 u nconventional, because 2n distinct 0-1 variables are used for each cla use 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 constr aint), and no two 0-1 variables, representing a literal and its comple ment, are both set equal to 1 (exclusion constraints). The particular m-CNF-SAT instance is coded in a cost vector, which serves for maximiz ation of the number of satisfied clauses. The paper presents a modific ation 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 experimen tal tests are reported, and the procedure is compared to other approac hes. The same modelling technique is then used for the Traveling Sales person Problem, for the Minimal Set Covering, and for the Quadratic As signment Problem: it is shown that a uniform approach is thus useful.