Reducing Signed SAT to Mixed Integer Linear Programming

We introduce a novel reduction from the satisfiability problem for a set of propositional signed clauses (Signed SAT) to Mixed Integer Linear Programming (MILP). This reduction provides a scalable and effective approach for solving Signed SAT instances via MILP and can be extended to address a broad class of NP-complete combinatorial decision problems through their reduction to Signed SAT. Furthermore, we present a reduction for a variant of Signed SAT in which each clause is expressed as a disjunction of signed literals rather than as a signed disjunction of literals. Finally, we discuss how these reductions can be adapted for pseudo-Boolean (PB) solving, enabling the use of PB solvers that exploit SAT-based techniques.