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.
The Tseytin transformation, alternatively written Tseitin transformation, takes as input an arbitrary combinatorial logic circuit and produces an equisatisfiable boolean formula in conjunctive normal form (CNF). 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. It was discovered by the Russian scientist Grigori Tseitin.
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.
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.
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.
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.
| Type | Operation | CNF sub-expression |
|---|---|---|
 AND | ||
 NAND | ||
 OR | ||
 NOR | ||
 NOT | ||
 XOR | ||
 XNOR | ||
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:
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) ∧ (gate1∨x1) |
| gate2 | (gate2∨ gate1) ∧ (gate2∨ x2) ∧ (x2∨ gate2 ∨gate1) |
| gate3 | (gate3 ∨ x2) ∧ (gate3∨x2) |
| gate4 | (gate4∨ x1) ∧ (gate4∨ gate3) ∧ (gate3∨ gate4 ∨x1) |
| gate5 | (gate5 ∨ x2) ∧ (gate5∨x2) |
| 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:
One possible satisfying assignment of these variables is:
| variable | value |
|---|---|
| gate2 | 0 |
| gate3 | 1 |
| gate1 | 1 |
| gate6 | 1 |
| gate7 | 0 |
| gate4 | 0 |
| gate5 | 1 |
| gate8 | 1 |
| x2 | 0 |
| x3 | 1 |
| x1 | 0 |
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.
Presented is one possible derivation of the CNF sub-expression for some chosen gates:
An OR gate with two inputs A and B and one output C is satisfies the following conditions:
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
The NOT gate is operating properly when its input and output oppose each other. That is:
express these conditions as an expression that must be satisfied:
The NOR gate is operating properly when the following conditions hold:
express these conditions as an expression that must be satisfied:
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.
In logic, a logical connective is a logical constant. Connectives 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 .
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.
In propositional logic and Boolean algebra, De Morgan's laws, also known as De Morgan's theorem, 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 — in philosophical logic — 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, exclusive disjunction, exclusive alternation, logical non-equivalence, or logical inequality is a logical operator whose negation is the logical biconditional. With two inputs, XOR is true if and only if the inputs differ. With multiple inputs, XOR is true if and only if the number of true inputs is odd.
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 assume the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.
In logic and mathematics, statements and are said to be logically equivalent if they have the same truth value in every model. The logical equivalence of and is sometimes expressed as , , , or , depending on the notation being used. However, these symbols are also used for material equivalence, so proper interpretation would depend on the context. Logical equivalence is different from material equivalence, although the two concepts are intrinsically related.
In Boolean logic, logical NOR, non-disjunction, or joint denial is a truth-functional operator which produces a result that is the negation of logical or. That is, a sentence of the form (p NOR q) is true precisely when neither p nor q is true—i.e. when both p and q are false. It is logically equivalent to and , where the symbol signifies logical negation, signifies OR, and signifies AND.
In logic and mathematics, the logical biconditional, also known as material biconditional or equivalence or biimplication or bientailment, is the logical connective used to conjoin two statements and to form the statement " if and only if ", where is known as the antecedent, and the consequent.
In computer science, a binary decision diagram (BDD) or branching program is a data structure that is used to represent a Boolean function. On a more abstract level, BDDs can be considered as a compressed representation of sets or relations. Unlike other compressed representations, operations are performed directly on the compressed representation, i.e. without decompression.
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.
In proof theory, the semantic tableau (; plural: tableaux, also called an analytic tableau, truth tree, or simply tree, 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.
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.
The XNOR gate is a digital logic gate whose function is the logical complement of the Exclusive OR (XOR) gate. It is equivalent to the logical connective from mathematical logic, also known as the material biconditional. The two-input version implements logical equality, behaving according to the truth table to the right, and hence the gate is sometimes called an "equivalence gate". A high output (1) results if both of the inputs to the gate are the same. If one but not both inputs are high (1), a low output (0) results.
In logic, a functionally complete set of logical connectives or Boolean operators is one that 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 }. Each of the singleton sets { NAND } and { NOR } is functionally complete. However, the set { AND, OR } is incomplete, due to its inability to express NOT.
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 modal 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.
Rayo's number is a large number named after Mexican philosophy professor Agustín Rayo which has been claimed to be the largest named number. It was originally defined in a "big number duel" at MIT on 26 January 2007.
