Using SAT for Computer Vision tasks
Many problems in computer vision are naturally expressed as constraint satisfaction problems.  There is a history going back several decades of applying constraint programming to such problems.  One of the key early papers in constraint satisfaction was completely motivated by problems from computer vision.


Ugo Montanari, Networks of constraints: Fundamental properties and applications to picture processing, Information Sciences 7 95–132, 1974. doi: 10.1016/0020-0255(74)90008-5


See this book for a recent overview of the application of constraints to particular problems in computer vision.


Martin Cooper, Line Drawing Interpretation. Springer-Verlag, 2008. (publisher's site)


If you really do want SAT and would like to avoid constraint satisfaction, then you can translate the constraint formulation into SAT, either manually or using an automated translation tool like Sugar.  Note that Chapter 2 of the recent Handbook of Satisfiability claims that it is common to first express one's problem as a constraint satisfaction problem, and only then to translate this formulation to SAT.  So constraint satisfaction should probably be considered even when one wants to work with SAT.

There is one big advantage of staying within a more expressive paradigm.  The constraint satisfaction framework allows the use of interval and numeric constraints.  These often occur in computer vision, but can lead to SAT instances that are infeasibly large.  Specialised constraint solvers may be greatly preferable to SAT solvers in such cases.

(A final aside: I have heard that the computer vision community tends not to be aware of constraint satisfaction approaches, and that this has led to the reinvention of well-known constraints techniques and results.  I do not know if this is a correct assessment, but if it is, then it would be worth translating constraints results to the terminology and specific concerns of computer vision.)