CAvSAT: A System for Query Answering over Inconsistent Databases

Research Fellow: Akhil Dixit 

Advisor: Phokion Kolaitis


Managing inconsistencies in databases is an old, but recurring, problem. An inconsistent database is a database that violates one or more integrity constraints, such as key constraints or inclusion dependencies. Inconsistent databases arise in several different contexts, including information integration, where dealing with inconsistency is regarded as a key challenge. Consistent Query Answering (CQA) is a principled and scientific approach for answering queries over inconsistent databases. The CAvSAT (Consistent Answers via Satisfiability) aims to build a scalable and comprehensive consistent query answering system over inconsistent databases.

The problem of finding query answers with the CQA semantics can be coNP-hard, thus, computationally harder than simply evaluating the query on the database. At its core, the CAvSAT system implements natural reductions from the complement of the problem of CQA to variants of Boolean Satisfiability problem, and uses state-of-the-art SAT solvers to compute the consistent answers. For some classes of queries, computing consistent answers has lower computational complexity, in which case CAvSAT opts for different approaches to compute consistent answers faster, via specially designed modules as shown in the architecture below.


Architecture of the CAvSAT system

Current Status

We have developed and tested the Query Pre-processor module, the SQL-rewritability module, and the SAT solving module. Our initial experiments provide evidence that a SAT-based approach can indeed give rise to a comprehensive and scalable system for consistent query answering.


Dixit, A., and Kolaitis, P. CAvSAT: Answering Aggregation Queries over Inconsistent Databases via SAT
Solving. In Proceedings of the 2021 ACM SIGMOD International Conference on Management of Data (Shaanxi,
China, 2021), SIGMOD ‘21, ACM.

Akhil A. Dixit and Phokion G. Kolaitis. Consistent answers of aggregation queries using SAT
solvers. CoRR, abs/2103.03314, 2021.

Dixit, A. A. and Kolaitis, P. G. "A SAT-based System for Consistent Query Answering." (2019). In the Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing 2019, Lisbon, Portugal. The Full version of the paper is available at


Akhil Dixit won the First Place for presenting the CAvSAT project at the 3rd ACM SIGMOD Student Research Competition, sponsored by Microsoft, hosted by the SIGMOD 2019 conference in Amsterdam, The Netherlands.

See Also