Tseytin變換，也可以寫成Tseitin變換，把一個任意的組合邏輯電路作為輸入，產生一個共軛正常形式（CNF）的布爾公式，可以用CNF-SAT求解器來解決。公式的長度與電路的大小呈線性關系。使電路輸出為真的輸入向量與滿足該公式的賦值有1對1的對應關系。這就把任何電路（包括任何公式）上的電路可滿足性問題簡化為3-CNF公式的可滿足性問題。

天真的方法是把電路寫成布爾表達式，然后用DeMorgan定律和分布屬性把它轉換成CNF。然而，這可能會導致方程大小的指數級增長。Tseytin轉換法輸出的公式的大小相對于輸入電路的大小是線性增長的。

輸出的方程是常數1設置為等于一個表達式。這個表達式是一個子表達式的組合，其中每個子表達式的滿足都會使輸入電路中的一個門正常工作。因此，整個輸出表達式的滿足就意味著整個輸入電路的正常運行。對于每一個門，都會引入一個代表其輸出的新變量。一個預先計算好的與輸入和輸出相關的小型CNF表達式被附加到輸出表達式上（通過and操作）。請注意，這些門的輸入可以是原來的字詞，也可以是代表子門輸出的引入變量。盡管輸出表達式比輸入表達式包含更多的變量，但它仍然是可滿足的，也就是說，當且僅當原始輸入方程是可滿足的，它才是可滿足的。當找到一個滿意的變量賦值時，可以簡單地丟棄那些引入變量的賦值。最后一個子句附加了一個字詞：最后一個門的輸出變量。如果這個字詞是補足的，那么這個子句的滿足將輸出表達式強制為假；否則表達式將強制為真。

下面列出了一些可能的子表達式，可以為各種邏輯門創建。在操作表達式中，C作為一個輸出；在CNF子表達式中，C作為一個新的布爾變量。對于每個操作，CNF子表達式是真的，當且僅當C在所有可能的輸入值中遵守布爾操作的契約。

下面的電路在至少有一些輸入為真時返回真，但一次不能超過兩個。它實現了方程式y=x1-x2+x1-x2+x2-x3。每個門的輸出都引入了一個變量；這里每個都用紅色標記。請注意，以x2為輸入的反相器的輸出引入了兩個變量。雖然這是多余的，但它并不影響所得方程的等價性。現在用適當的CNF子表達式替換每個門。