Satisfiability via Smooth Pictures

Abstract

A picture over a finite alphabet $\varGamma$ is a matrix whose entries are drawn from $\varGamma$. Let $\pi :\varSigma \rightarrow \varGamma$ be a function between finite alphabets $\varSigma$ and $\varGamma$, and let $V,H\subseteq \varSigma \times \varSigma$ be binary relations over $\varSigma$. Given a picture $N$ over $\varGamma$, the picture satisfiability problem consists in determining whether there exists a picture M over $\varSigma$ such that $\pi (M_{ij})=N_{ij}$, and such that the constraints imposed by V and H on adjacent vertical and horizontal positions of M are respectively satisfied. This problem can be easily shown to be NP-complete. In this work we introduce the notion of s-smooth picture. Our main result states the satisfiability problem for s-smooth pictures can be solved in time polynomial on s and on the size of the input picture. With each picture $N$, one can naturally associate a CNF formula $F(N)$ which is satisfiable if and only if $N$ is satisfiable. In our second result, we define an infinite family of unsatisfiable pictures which intuitively encodes the pigeonhole principle. We show that this family of pictures is polynomially smooth. In contrast we show that the formulas which naturally arise from these pictures are hard for bounded-depth Frege proof systems. This shows that there are families of pictures for which our algorithm for the satisfiability for smooth pictures performs exponentially better than certain classical variants of SAT solvers based on the technique of conflict-driven clause-learning (CDCL).