# Low-rank semidefinite programming for the MAX2SAT problem

## TL;DR

This paper introduces a low-rank semidefinite programming algorithm integrated with search methods, significantly improving the speed of solving MAX2SAT problems compared to existing solvers.

## Contribution

It presents a novel low-rank semidefinite programming approach tailored for incremental exact search algorithms for MAX2SAT, enhancing efficiency and applicability.

## Key findings

- Faster solution times than state-of-the-art solvers
- Applicable to both complete and incomplete search methods
- Demonstrated effectiveness on recent competition problems

## Abstract

This paper proposes a new algorithm for solving MAX2SAT problems based on combining search methods with semidefinite programming approaches. Semidefinite programming techniques are well-known as a theoretical tool for approximating maximum satisfiability problems, but their application has traditionally been very limited by their speed and randomized nature. Our approach overcomes this difficult by using a recent approach to low-rank semidefinite programming, specialized to work in an incremental fashion suitable for use in an exact search algorithm. The method can be used both within complete or incomplete solver, and we demonstrate on a variety of problems from recent competitions. Our experiments show that the approach is faster (sometimes by orders of magnitude) than existing state-of-the-art complete and incomplete solvers, representing a substantial advance in search methods specialized for MAX2SAT problems.