11
$\begingroup$

What are obstacles to making SAT solvers competitive with specialized graph algorithms? In other words, is it feasible to expect SAT solvers that can replace the role of algorithm designer -- ie, be able to automatically recognize problem structure and then solve it as quickly as a specialized algorithm?

Here some examples I think are challenging for today's SAT solvers:

  • Counting independent sets of size $k$. Encoding "x is an independent set of size k" gives a large formula which is hard to solve. An ideal SAT solver would recognize that this problem is easy on bounded tree-width graph with an addition of an extra "count" variable for bags.

  • Finding minimum Steiner tree. Again, "Steiner tree" has a global constraint, however, a specialized algorithm (like here) makes the task easier by adding an extra variable

  • Any problem that reduces to planar perfect matchings.

Improve this question
$\endgroup$
2
  • $\begingroup$ isn't this already happening ? It's a popular trick to reduce a problem to SAT and then run a solver. $\endgroup$
    – Suresh Venkat
    Jan 14, 2011 at 23:08
  • $\begingroup$ Yes, but are they competitive? I'm wondering if there is any SAT solver which could take a simple set of constraints describing Eulerian subgraph of a planar graph, and do #SAT in polynomial time $\endgroup$
    – Yaroslav Bulatov
    Jan 14, 2011 at 23:37

1 Answer 1

Reset to default
7
$\begingroup$

There is a nice paper that helps visualize the internal structure of SAT instances. See Visualizing SAT Instances and Runs of the DPLL Algorithm by Carsten Sienz (Appeared in SAT 2004). Basically, it draws a graph which the author calls "variable interaction graph" (according to some rules) to visualize the relation between the satisfied clauses. The author shows this by several partial runs of DPLL.

The main claim is that these visualization techniques could be used to detect structure and design an appropiate algorithm for it. However, it is still not clear how can we detect efficiently structures like the one presented in the paper. It is well known that SAT algorithms for one specific problem behave poorly in other problems. So there is "no-free-lunch", although this claim cannot be formally stated as far as I know.

Improve this answer
$\endgroup$
1
  • $\begingroup$ I think the relevant "no-free-lunch" theorem is the "no free lunch for search" no-free-lunch.org . Basically we can't afford search over all possible problem structures, and have to bias our search towards particular structures. I think that's OK since human algorithm designers do that already $\endgroup$
    – Yaroslav Bulatov
    Jan 14, 2011 at 23:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.