Tseytin transformation

Last updated

The Tseytin transformation, alternatively written Tseitin transformation, takes as input an arbitrary combinatorial logic circuit and produces a boolean formula in conjunctive normal form (CNF), which can be solved by a CNF-SAT solver. The length of the formula is linear in the size of the circuit. Input vectors that make the circuit output "true" are in 1-to-1 correspondence with assignments that satisfy the formula. This reduces the problem of circuit satisfiability on any circuit (including any formula) to the satisfiability problem on 3-CNF formulas.

Contents

Motivation

The naive approach is to write the circuit as a Boolean expression, and use De Morgan's law and the distributive property to convert it to CNF. However, this can result in an exponential increase in equation size. The Tseytin transformation outputs a formula whose size grows linearly relative to the input circuit's.

Approach

The output equation is the constant 1 set equal to an expression. This expression is a conjunction of sub-expressions, where the satisfaction of each sub-expression enforces the proper operation of a single gate in the input circuit. The satisfaction of the entire output expression thus enforces that the entire input circuit is operating properly.

For each gate, a new variable representing its output is introduced. A small pre-calculated CNF expression that relates the inputs and outputs is appended (via the "and" operation) to the output expression. Note that inputs to these gates can be either the original literals or the introduced variables representing outputs of sub-gates.

Though the output expression contains more variables than the input, it remains equisatisfiable, meaning that it is satisfiable if, and only if, the original input equation is satisfiable. When a satisfying assignment of variables is found, those assignments for the introduced variables can simply be discarded.

A final clause is appended with a single literal: the final gate's output variable. If this literal is complemented, then the satisfaction of this clause enforces the output expression's to false; otherwise the expression is forced true.

Examples

Consider the following formula .

Consider all subformulas (excluding simple variables):

Introduce a new variable for each subformula:

Conjunct all substitutions and the substitution for :

All substitutions can be transformed into CNF, e.g.

Gate Sub-expressions

Listed are some of the possible sub-expressions that can be created for various logic gates. In an operation expression, C acts as an output; in a CNF sub-expression, C acts as a new Boolean variable. For each operation, the CNF sub-expression is true if and only if C adheres to the contract of the Boolean operation for all possible input values.

TypeOperation CNF Sub-expression
AND ANSI.svg AND
NAND ANSI.svg NAND
OR ANSI.svg OR
NOR ANSI.svg NOR
NOT ANSI.svg NOT
XOR ANSI.svg XOR
XNOR ANSI.svg XNOR

Simple combinatorial logic

The following circuit returns true when at least some of its inputs are true, but not more than two at a time. It implements the equation y = x1· x2 + x1 ·x2 + x2· x3. A variable is introduced for each gate's output; here each is marked in red:

Comb logic tseitin.svg

Notice that the output of the inverter with x2 as an input has two variables introduced. While this is redundant, it does not affect the equisatisfiability of the resulting equation. Now substitute each gate with its appropriate CNF sub-expression:

gate CNF sub-expression
gate1(gate1 x1) (gate1x1)
gate2(gate2 gate1) (gate2 x2) (x2 gate2 gate1)
gate3(gate3 x2) (gate3x2)
gate4(gate4 x1) (gate4 gate3) (gate3 gate4 x1)
gate5(gate5 x2) (gate5x2)
gate6(gate6 gate5) (gate6 x3) (x3 gate6 gate5)
gate7(gate7 gate2) (gate7 gate4) (gate2 gate7 gate4)
gate8(gate8 gate6) (gate8 gate7) (gate6 gate8 gate7)

The final output variable is gate8 so to enforce that the output of this circuit be true, one final simple clause is appended: (gate8). Combining these equations results in the final instance of SAT:

(gate1 x1) (gate1x1) (gate2 gate1) (gate2 x2)
(x2 gate2 gate1) (gate3 x2) (gate3x2) (gate4 x1)
(gate4 gate3) (gate3 gate4 x1) (gate5 x2)
(gate5x2) (gate6 gate5) (gate6 x3)
(x3 gate6 gate5) (gate7 gate2) (gate7 gate4)
(gate2 gate7 gate4) (gate8 gate6) (gate8 gate7)
(gate6 gate8 gate7) (gate8) = 1

One possible satisfying assignment of these variables is:

variablevalue
gate20
gate31
gate11
gate61
gate70
gate40
gate51
gate81
x20
x31
x10

The values of the introduced variables are usually discarded, but they can be used to trace the logic path in the original circuit. Here, indeed meets the criteria for the original circuit to output true. To find a different answer, the clause (x1 x2 x3) can be appended and the SAT solver executed again.

Derivation

Presented is one possible derivation of the CNF sub-expression for some chosen gates:

OR Gate

An OR gate with two inputs A and B and one output C is satisfies the following conditions:

  1. if the output C is true, then at least one of its inputs A or B is true,
  2. if the output C is false, then both its inputs A and B are false.

We can express these two conditions as the conjunction of two implications:

Replacing the implications with equivalent expressions involving only conjunctions, disjunctions, and negations yields

which is nearly in conjunctive normal form already. Distributing the rightmost clause twice yields

and applying the associativity of conjunction gives the CNF formula

NOT Gate

The NOT gate is operating properly when its input and output oppose each other. That is:

  1. if the output C is true, the input A is false
  2. if the output C is false, the input A is true

express these conditions as an expression that must be satisfied:

,

NOR Gate

The NOR gate is operating properly when the following conditions hold:

  1. if the output C is true, then neither A or B are true
  2. if the output C is false, then at least one of A and B were true

express these conditions as an expression that must be satisfied:

, , , ,

Related Research Articles

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

Logical conjunction Logical connective AND

In logic, mathematics and linguistics, And is the truth-functional operator of logical conjunction; the and of a set of operands is true if and only if all of its operands are true. The logical connective that represents this operator is typically written as or .

Logical connective Symbol connecting sentential formulas in logic

In logic, a logical connective is a logical constant. They can be used to connect logical formulas. For instance in the syntax of propositional logic, the binary connective can be used to join the two atomic formulas and , rendering the complex formula .

Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions and relations between propositions, including the construction of arguments based on them. Compound propositions are formed by connecting propositions by logical connectives. Propositions that contain no logical connectives are called atomic propositions.

Multiplexer A device that selects between several analog or digital input signals

In electronics, a multiplexer, also known as a data selector, is a device that selects between several analog or digital input signals and forwards the selected input to a single output line. The selection is directed by a separate set of digital inputs known as select lines. A multiplexer of inputs has select lines, which are used to select which input line to send to the output.

De Morgans laws Pair of logical equivalences

In propositional logic and Boolean algebra, De Morgan's laws are a pair of transformation rules that are both valid rules of inference. They are named after Augustus De Morgan, a 19th-century British mathematician. The rules allow the expression of conjunctions and disjunctions purely in terms of each other via negation.

In boolean logic, a disjunctive normal form (DNF) is a canonical normal form of a logical formula consisting of a disjunction of conjunctions; it can also be described as an OR of ANDs, a sum of products, or a cluster concept. As a normal form, it is useful in automated theorem proving.

In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs. As a canonical normal form, it is useful in automated theorem proving and circuit theory.

Exclusive or True when either but not both inputs are true

Exclusive or or exclusive disjunction is a logical operation that is true if and only if its arguments differ.

Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not include the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.

Logical biconditional

In logic and mathematics, the logical biconditional, sometimes known as the material biconditional, is the logical connective used to conjoin two statements P and Q to form the statement "P if and only if Q", where P is known as the antecedent, and Q the consequent. This is often abbreviated as "P iff Q". Other ways of denoting this operator may be seen occasionally, as a double-headed arrow, a prefixed E "Epq", an equality sign (=), an equivalence sign (≡), or EQV. It is logically equivalent to both and , and the XNOR boolean operator, which means "both or neither".

In mathematical logic, a formula is in negation normal form (NNF) if the negation operator is only applied to variables and the only other allowed Boolean operators are conjunction and disjunction.

In logic, a truth function is a function that accepts truth values as input and produces a unique truth value as output. In other words: The input and output of a truth function are all truth values; a truth function will always output exactly one truth value; and inputting the same truth value(s) will always output the same truth value. The typical example is in propositional logic, wherein a compound statement is constructed using individual statements connected by logical connectives; if the truth value of the compound statement is entirely determined by the truth value(s) of the constituent statement(s), the compound statement is called a truth function, and any logical connectives used are said to be truth functional.

Method of analytic tableaux

In proof theory, the semantic tableau is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic. An analytic tableau is a tree structure computed for a logical formula, having at each node a subformula of the original formula to be proved or refuted. Computation constructs this tree and uses it to prove or refute the whole formula. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure for modal logics.

Predicate transformer semantics were introduced by Edsger Dijkstra in his seminal paper "Guarded commands, nondeterminacy and formal derivation of programs". They define the semantics of an imperative programming paradigm by assigning to each statement in this language a corresponding predicate transformer: a total function between two predicates on the state space of the statement. In this sense, predicate transformer semantics are a kind of denotational semantics. Actually, in guarded commands, Dijkstra uses only one kind of predicate transformer: the well-known weakest preconditions.

In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically applying the resolution rule acts as a decision procedure for formula unsatisfiability, solving the Boolean satisfiability problem. For first-order logic, resolution can be used as the basis for a semi-algorithm for the unsatisfiability problem of first-order logic, providing a more practical method than one following from Gödel's completeness theorem.

In logic, a functionally complete set of logical connectives or Boolean operators is one which can be used to express all possible truth tables by combining members of the set into a Boolean expression. A well-known complete set of connectives is { AND, NOT }, consisting of binary conjunction and negation. Each of the singleton sets { NAND } and { NOR } is functionally complete.

In mathematical logic, monoidal t-norm based logic, the logic of left-continuous t-norms, is one of the t-norm fuzzy logics. It belongs to the broader class of substructural logics, or logics of residuated lattices; it extends the logic of commutative bounded integral residuated lattices by the axiom of prelinearity.

In mathematics and philosophy, Łukasiewicz logic is a non-classical, many-valued logic. It was originally defined in the early 20th century by Jan Łukasiewicz as a three-valued logic; it was later generalized to n-valued as well as infinitely-many-valued (0-valued) variants, both propositional and first-order. The ℵ0-valued version was published in 1930 by Łukasiewicz and Alfred Tarski; consequently it is sometimes called the Łukasiewicz–Tarski logic. It belongs to the classes of t-norm fuzzy logics and substructural logics.

References