Solving satisfiability and implication problems in database systems

Satisfiability, implication, and equivalence problems involving conjunctive inequalities are important and widely encountered database problems that need to be efficiently and effectively processed. In this article we consider two popular types of arithmetic inequalities, (X op Y) and (Y op C), where X and Y are attributes, C is a constant of the domain or X, and op is an element of {<, less than or equal to, =, not equal, >, greater than or equal to}. These inequalities are most frequently used in a database system, inasmuch as the former type of inequality represents a theta-join, and the latter is a selection We study the satisfiability and implication problems under the integer domain and the real domain, as well as under two different operator sets ({<, less than or equal to, =, greater than or equal to, >} and {<, less than or equal to, =, not equal, greater than or equal to, >}). Our results show that solutions under different domains and/or different operator sets are quite different. Out of these eight cases, excluding two cases that had been shown to be NP-hard, we either report the first necessary and sufficient conditions for these problems as well as their efficient algorithms with complexity analysis (for four cases), or provide an improved algorithm (for two cases). These iff conditions and algorithms are essential to database designers, practitioners, and researchers. These algorithms have been implemented and an experimental study comparing the proposed algorithms and those previously known is conducted. Our experiments show that the proposed algorithms are more efficient than previously known algorithms even for small input.