SAT-based Compressive Sensing.

We propose to reduce the original problem of compressive sensing to the weighted-MAX-SAT. Compressive sensing is a novel randomized data acquisition method that outperforms the traditional signal processing approaches (namely, the Nyquist-Shannon technique) in acquiring and reconstructing sparse or compressible signals. The original problem of compressive sensing in sparse recovery has a combinatorial nature so that one needs to apply severe constraints on the design matrix to handle it by its convex or nonconvex relaxations. In practice, such constraints are not only intractable to be verified but also invalid in broad applications. This paper bridges the gap between employing the modern SAT solvers and a vast variety of compressive sensing based real-world applications -ranging from imaging, video processing, remote sensing, communication systems, electronics and VLSI to machine learning, data fusion, manifold processing, natural language and speech processing, and processing the biological signals. We first divide the original problem of compressive sensing into relaxed sub-problems and represent them as separate SAT instances in conjunctive normal form (CNF). Afterward, we assign the weights to the clauses in such a way that the aggregated weighted-MAX-SAT problem can guarantee a successful recovery of the original signal. As proof of concept, we demonstrate the applicability of our approach in tackling the original problem of binary compressive sensing with Bernoulli design matrices.