My question in general asks how to transform a sequential circuit/FSM into a combinational circuit.
The reason why I'm asking is in SAT solving, we can use only combinational circuits. And so in order to use sequential circuit, we need to "unroll" them into a combinational circuit. I don't quite understand this.
By definition, a sequential circuit has "state" (memory), and its outputs are a function of both its inputs and its internal state. This can only be done if it contains one or more internal feedback paths. Usually this feedback is embodied in the form of flip-flops and latches, but there are other kinds of feedback that can be used to create sequential circuits as well.
Also by definition, a combinatorial (combinational) circuit always has the same output for a given input, which means that it has no internal state and no internal feedback.
So, if you add feedback to a combinatorial circuit, it becomes a sequential circuit, and if you remove all feedback from a sequential circuit, it becomes a combinatorial circuit. But there really isn't any kind of functional equivalence that can be established between the two types of circuits, so I'm not sure what kind of "transformation" you're looking for.
OK, I finally looked up "SAT solving", so now I understand where you're coming from.
Most sequential circuits can be clearly divided into one or more "registers" (groups of flip-flops or latches) on one hand, and network(s) of purely-combinatorial logic that connect the registers to each other and to the inputs and outputs of the circuit on the other hand.
Basically, each single bit of register input or circuit output is one combinatorial result — the root of a "tree" of logic, if you will — whose input variables (leaves) are either circuit inputs or register outputs. You perform the SAT solving on each of those trees, one at a time.
For example, here's the schematic of a 4-bit counter chip. I've highlighted the tree of combinatorial logic that drives the D input of FF2. Starting with that pin, I highlighted the net back to the source that drives it (the NOR gate). I then found the sources that drive all of the inputs to that gate (the two AND gates). For each new gate found this way, I kept working my way to the sources of its inputs until I got to either the output of one of the internal flip-flops or an external input to the chip. Therefore, the input variables (leaves) for this tree of logic are the \$\overline{Q}\$ outputs of FF1 and FF2, along with the external inputs \$CEP\$, \$CET\$, \$\overline{PE}\$, \$\overline{MR}\$ and \$D1\$.
