Conjunctive Query Containment as SAT
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.