Functional treewidth: Bounding complexity in the presence of functional dependencies

Many reasoning problems in logic and constraint satisfaction have been shown to be exponential only in the treewidth of their interaction graph: a graph which captures the structural interactions among variables in a problem. It has long been observed in both logic and constraint satisfaction, however, that problems may be easy even when their treewidth is quite high. To bridge some of the gap between theoretical bounds and actual runtime, we propose a complexity parameter, called functional treewidth, which refines treewidth by being sensitive to nonstructural aspects of a problem: functional dependencies in particular. This measure dominates treewidth and can be used to bound the size of CNF compilations, which permit a variety of queries in polytime, including clausal implication, existential quantification, and model counting. We present empirical results which show how the new measure can predict the complexity of certain benchmarks, that would have been considered quite difficult based on treewidth alone.