A Linear Algebra Formulation for Boolean Satisfiability Testing

TL;DR

This paper introduces a linear programming approach to Boolean satisfiability testing, aiming to find an alternative to traditional methods like DPLL, with promising results on many unsatisfiable instances.

Contribution

The paper presents a novel linear algebra formulation for SAT testing, offering a different perspective from classical algorithms and exploring its practical effectiveness.

Findings

Works on many unsatisfiable instances

Method is incomplete, aligning with complexity theory

Provides a new linear algebra perspective for SAT

Abstract

In the article \The State of SAT", the authors asked whether a procedure dramatically different from DPLL can be found for handling unsatisfiable instances. This study proposes a new linear programming approach to address this issue efficiently. Our experiments showed that the new method works for many unsatisfiable instances. However, we must concede that this method should be incomplete; otherwise, it will imply P=co-NP.