Sunday, March 23, 2014

SAT Solvers

SAT? No, not the scholastic test. Rather, this deals with Boolean satisfiability which is a hard problem. A comment of Moshe of ACM Communications motivated this post. He was at a workshop this year that looked at a couple of things. One was whether were new theoretical insights from practice of late. The other was a sampling of techniques that solves these types of problems, albeit by rule of thumb.

We earlier mentioned algorithms as having a firmer basis than heuristics. There are a lot of SAT approaches. Let's pause here for a couple of pointers: Understanding SAT solvers, Flow Control Analysis for SAT Solvers. We could find a lot more.

From his observing the state of the art at the workshop, Moshe says that the methods are mostly heuristic. We might say that there are two issues to consider. One is that the hardness of a problem relates to the difficulty of finding its solution in an effective (time, resource, money) manner. The other is that solutions, if found, can be verified quite easily (compared to the search).

What does this mean for truth engineering? Firstly, assessing truth is a hard problem, computationally. We know this. But, truth is hard in general, too. Efforts at determining truth need to be reasonably constrained, if possible.

So, it is nice that we see motivation to define and explore the efficacy of a solution approach. However, we must, too, remember that maintaining the truthful state is not a given. In some cases, the trouble related to maintenance may be even worse than the original determination.

Catch-22? Somewhat. But, not.

Remarks:   Modified: 05/30/2014

04/24/2014 -- For a recent discussion on the other SAT, see Rick's post (he mentions big data and analytics, thereof).

05/30/2014 -- The May CACM (Vol. 57, No. 5) had an interesting article title "Understanding the Empirical Hardness of NP-Complete Problems" in which the authors talk about helping resolve hardness, somewhat (taming the beast), via statistical means. Makes one almost thing that these issues are of no concern going forward (throw computational power at the problem). But, it cannot be as easy as that (to wit, at the end of the 18th century, the Illuminati was claiming that everything was known about physics - so everyone go home and twiddle your thumbs). As the authors say, has to do with whether you can get solutions and whether you can do so in a reasonable time. Yet, there is more (still to be characterized). If the spaces quake, solutions become more difficult. Say what? Yes, we'll be getting back to this.

No comments: