Conjunctive Query Containment as SAT The problem of conjunctive query containment is known to be NP-Complete (originated at Chandra&amp;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?
I will try to answer your question limiting to Datalog without recursive predicates. Indeed, I suspect that recursive predicates are beyond conjunctive queries (conjunctive queries are a subset of FOL, and Datalog with recursion can compute Transitive Closures, which are impossible to express in FOL). Furthermore, I will assume that all derived datalog predicates have been unfolded.
As you probably know, a conjunctive query CQ1 contains CQ2 if you can establish an homomorphism of terms from CQ1 into CQ2. Hence, a possible reduction into SAT can be done by considering a boolean variable v for each pair of terms from Terms(CQ1)xTerms(CQ2). Intuitively, the meaning of such variables would be &quot;we map term t1 to term t2&quot;. Then, we must ensure that the set of all variables &quot;v&quot; that evaluates to true encodes a correct homomorphism.
More formally, the reduction can be done as follows:

For each term $t^1_i \in Terms(CQ1)$, and for each term $t^2_j \in Terms(CQ2)$, consider a boolean variable $v_{t^1_i, t^2_j}$. Note that all the boolean variables evaluating to true encodes a mapping.
The encoded mapping must be functional. That is, for each term $t^1_i$, we need a constraint to state that $t^1_i$ is mapped to one term, and only one. Hence, we should add, for each term $t^1_i$, a constraint $(v_{t^1_i, t^2_1} \lor v_{t^1_i, t^2_2} \lor ... \lor v_{t^1_i, t^2_n})$, and for each triple of terms $t^1_i$, $t^2_j$, $t^2_k$ (with j!=k), $(\neg (v_{t^1_i, t^2_j} \land v_{t^1_i, t^2_k}))$
The encoded mapping must preserve constants. Hence, for each constant term $t^1_c$, we add the constraint: $(v_{t^1_c t^2_c})$
The encoded mapping must be a homomorphism. To do so, for each literal $L^1 \in Literals(CQ1)$, let $\{L^2_1 ... L^2_n\}$ be the set of all literals from $Literals(CQ2)$ with the same predicate. Then, we must ensure that, when mapping the terms of $L^1$ we obtain one literal from $\{L^2_1 ... L^2_n\}$. To do so, we build a disjunction where each disjunct $i$ means &quot;$L_1$ is mapped to $L_i$&quot;. In particular, each one of these disjuncts can be built by iterating all the variables from $L^1$ and mapping them to $L^2_i$ variables. For instance, consider $L^1$ to be  $P(x, x, y)$, and considere $\{L^2_1 ... L^2_n\}$ to be $\{P(a, b, a), P(c, c, d)\}$; in this case we would build the constraint: $(v_{x a} \land v_{x b} \land v_{y a}) \lor (v_{x c} \land v_{x c} \land v_{y d})$

This reduction is polynomial. Indeed, the number of boolean variables is quadratic (w.r.t. the number of terms in CQ1 and CQ2), and all the constraints considered can be built with a several (nested) foreach loops that iterates the conjunctive queries terms and literals.