# Conjunctive Query Containment as SAT

The problem of conjunctive query containment is known to be NP-Complete (originated at Chandra&Merlin 1977). Typically it's shown by reducing 3SAT or 3-colorability into this problem, and the other direction is typically proven by declaring it "trivial" (as it indeed looks trivial to see that the problem is in NP).

My question is how to practically translate the problem of query containment of two datalog rules (plain, without constraints or equalities) into the boolean satisfiability problem (not necessarily in CNF), and by listing the solutions of that latter problem, to see which variable substitutions would recover the containment? In other words, how to solve this problem using a SAT solver in practice?

Probably not the answer you are looking for, but if conjunctive query containment is in $$\mathsf{NP}$$, then there is a nondeterministic Turing machine which solves it. Hence, given an instance $$x$$ of CQC, you can use the construction in (the proof of) the Cook-Levin theorem to encode the behavior of said NTM on $$x$$ as a SAT formula (and decide $$x$$).