As I know, any SAT solver such as or-tools or cplex cp optimizer converts a given problem to CNF form in the first place. Is it possible to extract the resulting CNF representation from or-tools or cplex?
CP-SAT uses a SAT backend. But at any moment, just like with SMT solvers, the full model is never fully represented using clauses and Boolean literals. I recommend looking at the CPAIOR 2020 masterclass on CP (on YouTube) to get a better understanding of the architecture of the solver.