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: 03/23/2014