Consistency in valuation-based systems

This paper has three main results. First, we present a new computational technique for checking for inconsistencies in valuation-based systems. This technique is different from the implicit enumeration method of Davis–Putnam and its variants. Our technique uses the divide-and-conquer method of dynamic programming. The computational complexity of this technique depends on the sizes of the valuations and on the graphical structure of the valuation-based system. Second, if a valuation-based system is consistent, we describe a method for generating a model for the system, i.e. an assignment of values for each variable that is consistent with each valuation in the system. Third, if a valuation-based system is inconsistent, we describe a method for isolating a minimal inconsistent set of valuations.