Title: Using the unconstrained quadratic program to model and solve Max 2-SAT problems

Authors: Gary Kochenberger, Fred Glover, Bahram Alidaee, Karen Lewis

Addresses: School of Business, Campus Box 165, University of Colorado, Denver, CO 80217-3364, USA ' Leeds School of Business, UCB 419 University of Colorado, Boulder, CO 80309-0419, USA. ' MIS/POM Department, Hearin Center for Enterprise Science, School of Business Administration, The University of Mississippi, University, MS 38677, USA. ' 231 Holman, School of Business Administration, University of Mississippi, University, MS 38677, USA

Abstract: Satisfiability (SAT) and Max-SAT problems have been the object of considerable research effort over the past few decades. They remain a very important research area today due to their computational challenge and application importance. In this paper, we investigate the use of penalty functions to recast SAT problems into the modelling framework offered by the unconstrained quadratic binary program. Computational experience is presented, illustrating how promising this approach is for Max 2-Sat problems.

Keywords: satisfiability; metaheuristics; Tabu search; penalty functions; unconstrained quadratic program; Max 2-SAT problems; combinatorial optimisation.

DOI: 10.1504/IJOR.2005.007435

International Journal of Operational Research, 2005 Vol.1 No.1/2, pp.89 - 100

Published online: 20 Jul 2005 *

Full-text access for editors Access for subscribers Purchase this article Comment on this article