On Wiki Tseytin transformation we have (example):
$(gate1\vee x1)\wedge (\overline{gate1}\vee \overline{x1})\wedge (\overline{gate2}\vee gate1)\wedge (\overline{gate2}\vee x2)\wedge $
$(\overline{x2}\vee gate2\vee \overline{gate1})\wedge (gate3\vee x2)\wedge (\overline{gate3}\vee \overline{x2})\wedge (\overline{gate4}\vee x1)\wedge $
$(\overline{gate4}\vee gate3)\wedge (\overline{gate3}\vee gate4\vee \overline{x1})\wedge (gate5\vee x2)\wedge $
$(\overline{gate5}\vee \overline{x2})\wedge (\overline{gate6}\vee gate5)\wedge (\overline{gate6}\vee x3)\wedge $
$(\overline{x3}\vee gate6\vee \overline{gate5})\wedge (gate7\vee \overline{gate2})\wedge (gate7\vee \overline{gate4})\wedge $
$(gate2\vee \overline{gate7}\vee gate4)\wedge (gate8\vee \overline{gate6})\wedge (gate8\vee \overline{gate7})\wedge $
$(gate6\vee \overline{gate8}\vee gate7)\wedge (gate8) = 1$
This is CNF sub-expression.
Is it possible to direct the use of such data in the SAT problem?
The Tseitin transformation may look very bad at first because of all the variables that are introduced. The auxiliary variables expand the search space, but the effect on search time isn't as bad as most would think at first.
First of all, what's the alternative? Computing a CNF formula that is equivalent to the given circuit may incur an exponential blow-up, whereas the equisatisfiable CNF formula that results from the transformation is within a constant factor of the given circuit.
Second, modern propositional SAT solvers usually apply partial resolution as they preprocess the given CNF formula. So, some of these auxiliary variables disappear before the search actually begins.
Third, a lot of the introduced clauses have two literals, hence represent implications. As soon as one of the variables of such a clause is assigned a value, the clause either is satisfied, or forces the value of the other variable.
Finally, the best Conflict-Driven Clause-Learning SAT solvers are very sophisticated pieces of software, and can often deal with SAT instances that have millions of clauses and hundreds of thousands of variables. Of course, they get stumped by some formulae that are much smaller than that, but many variables and many clauses are not the main obstacle.
All in all, the Tseitin transformation is a practical, widely adopted approach to reducing Boolean circuits to CNF. There are variants of the transformation that occasionally perform a bit better. (They would be significantly better if SAT solvers didn't preprocess their input. As things stand, they are sometime even worse.)