Using SAT for Computer Vision tasks

Could anyone please point to both introductory and advanced papers/books showing how to use SAT technology to solve Computer Vision tasks (e.g. edge detection, object recognition, facial recognition, ...)?

More precisely: I'm looking for SAT-based techniques to extract knowledge from images and reason about such knowledge (e.g. is object $X_1$ in front of object $X_2$? Is object $X_3$ partially hidden by object $X_4$? Is person $X_5$ in image $I_1$ the same as person $X_6$ in image $I_2$?).

• @supercooldave: Hi Dave, I've seen your answer about clique and max-clique. I was about to write a comment on that, but your answer disappeared. Oct 1 '10 at 10:50
• When the question changed, I thought my comment became irrelevant. Oct 1 '10 at 11:09

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.

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.)

• Montanari has done image processing work, too. That man has done everything. Oct 2 '10 at 16:01
• Thank you for this very interesting answer. As soon as I'll become a registered user, I'll vote it up. Oct 4 '10 at 7:34

Some computer vision problems rely on cliques and max cliques, which can be reduced to SAT.

• Very interesting, I didn't know that. Do you have links to any document showing such a connection between computer vision problems and clique/max-clique? Oct 1 '10 at 12:02
• One is: arxiv.org/abs/1009.4823. Some people refer to D.H. Ballard and M. Brown, Computer Vision, Prentice-Hall, Englewood Cliffs, N.J. 1982. Oct 1 '10 at 12:11
• The link with maximum clique is usually via the microstructure of the constraint satisfaction problem that underlies the problem. Specifically, the partial solutions of the problem correspond to cliques in the microstructure; the maximum clique then corresponds to a solution. Oct 2 '10 at 15:57