3
$\begingroup$

Let $\phi$ be a Boolean formula and $\mathrm{Tseitin}(\phi)$ the corresponding Tseitin transformed equisatifiable formula.

It is well-known that one can get a variable assignment for $\phi$ by solving $\mathrm{Tseitin}(\phi)$ and dropping the auxiliary variables. For example, see Wiki, quote: "When a satisfying assignment of variables is found, those assignments for the introduced variables can simply be discarded."

After a long search through SAT papers I just could not find any paper which proves this statement. Because I do not want to re-invent the wheel: Does anyone know such a reference I can use to cite?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
1
$\begingroup$

Given a circuit $C$ on variables $V$ which has gates $G$, the Tseitin transformation produces a formula $T(C)$ on the set of variables $V \cup G$, with the property that the formula holds iff

  1. The value of every gate variable $g \in G$ is exactly the value of this gate given the assignment to the inputs, and
  2. The circuit outputs TRUE.

You can prove property (1) by induction. Property (2) holds since you add a specific clause stating that the top gate in the circuit is TRUE. Given this, there is an assignment causing the circuit $C$ to output true iff $T(C)$ is satisfiable, and moreover you can read this assignment from a satisfying assignment to $T(C)$ — just ignore the gate variables.

The crucial point is that in any satisfying assignment of $T(C)$, the value of the gate variables is completely determined by the value of the input variables.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thank you for your illustrating explanation. I appreciate that. But what I really would like to know is if there is a reference I can use to cite. I would like to use this well-known property in my research without re-inventing the wheel and page limits are restrictive. :-/ $\endgroup$
    – John Threepwood
    Feb 12, 2015 at 20:10
  • $\begingroup$ I would say this property is trivial, so there is no need to cite anything. The property is probably proved (in some different language) in any original paper describing this transformation. I suspect this transformation was described several times, the first time perhaps indeed by Tseitin. So if you really want a citation, you might have to look at some old Russian papers. $\endgroup$
    – Yuval Filmus
    Feb 12, 2015 at 20:15
1
$\begingroup$

There is no need to cite anything. This is known in the Tseitin transform and it is well-known in the SAT / formal methods community. Therefore, if you are writing for that community, there's no need to formally cite anything.

It is so well-known that it is covered on Wikipedia: https://en.wikipedia.org/wiki/Tseitin_transformation. In the theoretical computer science community, this is the classic reduction from CircuitSAT to SAT. That reduction is proven or sketched in many undergraduate textbooks on theoretical computer science / algorithms / textbooks. I think it was also proven in Cook's seminal paper.

If you feel you absolutely want to cite something, you could look at the Tseitin paper cited on the Wikipedia page; that might have the earliest standard description.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.