Anil P. Kamath, Narendra K. Karmarkar, K.G. Ramakrishnan, Mauricio G.C. Resende
Annals of Operations Research, vol. 25, pp. 43-58, 1990
We apply the zero-one integer programming algorithm described in Karmarkar (1988) and Karmarkar, Resende and Ramakrishnan (1988) to solve randomly generated instances of the satisfiability problem (SAT). The interior point algorithm is briefly reviewed and shown to be easily adapted to solve large instances of SAT. Hundreds of instances of SAT (having from 100 to 1000 variables and 100 to 32,000 clauses) are randomly generated and solved. For comparison, we attempt to solve the problems via linear programming relaxation with MINOS.
PDF file of full paper
Mauricio G.C. Resende's Home PageLast modified: 11 April 2007