Abstract (100 words or less): |  | The satisfiability (SAT) problem is a well-known NP-complete problem in mathematical logic with applications in many areas, including artificial intelligence, circuit testing, and software verification. An instance of SAT is specified by a set of Boolean variables and a propositional formula in conjunctive normal form. Given such an instance, the SAT problem asks whether there is a truth assignment to the variables such that the formula is satisfied. Recent research has shown the potential of semidefinite optimization-based approaches for complementing existing techniques for SAT. We report the latest progress in the application of semidefinite optimization to SAT, particularly for obtaining proofs of unsatisfiability. |