💾 Archived View for dcreager.net › papers › Creager2007b.gmi captured on 2023-07-22 at 16:23:35. Gemini links have been rewritten to link to archived content
-=-=-=-=-=-=-
DA Creager and AC Simpson. “Empirical analysis and optimization of an NP-hard algorithm using CSP and FDR.” In Proceedings of the Brazilian Symposium on Formal Methods (SBMF 2007). ENTCS, to appear.
This is an extended version of [Creager2007a], which I presented at SBMF 2007 in Ouro Preto, Brazil.
In many cases where an algorithm is provably NP-hard, this intractability is a worst-case bound that only applies to pathological inputs. In these cases, by exploiting knowledge of the specific structure of “real-world” inputs, the algorithm can be shown to be much more efficient in the “normal” case. However, when studying a new problem, this can be hard to show if it is not obvious which structural constraints exist, and which ones would lead to increases in efficiency. In this paper, we show how one can describe the underlying problem declaratively as a CSP process and use the FDR refinement checker to explore the complexity space of the problem. By knowing which optimizations FDR uses to find solutions more efficiently, we can determine under which conditions the worst-case intractable algorithm executes efficiently, and incorporate analogous optimizations into the algorithm to exploit these conditions.