On the Complexity of Derivation in Propositional Calculus

By G. S. Tseitin. 1983

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

Optimal Decision Lists using SAT (2020, background): “The model shown above represents a non-clausal Boolean formula, which can be clausiﬁed with the use of auxiliary variables (Tseitin 1968).”
Computing Optimal Decision Sets with SAT (2020, background): “be at least one leaf literal where it is valid: 8i2[M] _ j2[N] (sjc^vij) (6) The model shown above represents a non-clausal Boolean formula, which can be clausiﬁed with the use of auxiliary variables [54]. Also note that any of the known cardinality encodings can be used to represent constraint (1) ”
Conflict-driven answer set solving: From theory to practice (2012, background): “Such propositions are also introduced in Conjunctive Normal Form (CNF) transformations as abbreviations avoiding an exponential blow-up [123].”
Translating Pseudo-Boolean Constraints into SAT (2006, methodology): “The primary technique used by M INI S AT + is to ﬁrst convert each constraint into a single-output circuit, and then translate all circuits to clauses by a variation of the Tseitin transformation [32].”
Discovering Cyclic Causal Models with Latent Variables: A General SAT-Based Procedure (2013, methodology): “Any propositional formula can be represented in conjunctive normal form (CNF) using a standard linear-size encoding (Tseitin, 1983).”
Efficient implementation of property directed reachability (2011, methodology): “The netlist is transformed to CNF using the standard Tseitin transformation [9] plus variable elimination [6].”
Efficient E-Matching for SMT Solvers (2007, methodology): “example, when clausifying l1 ∨ (l2 ∧ l3) using a Tseitin [25] style algorithm we obtain the set of clauses:”
Effective Preprocessing in SAT Through Variable and Clause Elimination (2005, methodology): “If a circuit is encoded in CNF, typically using the Tseitin transformation [22], then many variables are actually functionally dependent on other variables, particularly those introduced for gate outputs.”
Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic (2014, unknown): “These symbols are known as logical connectives.”
Handbook of Satisfiability (2021, background): “The first results on the complexity of resolution were proved by Grighori Tseitin in 1968 (278).”
Towards an Optimal CNF Encoding of Boolean Cardinality Constraints (2005, methodology): “This technique, that preserves satisfiability of the whole set of equivalences, was introduced by Tseitin [7] and was later re-invented and extended by different authors [8–11].”
A SAT-Based Approach to Learn Explainable Decision Sets (2018, background): “Moreover, standard clausification techniques are assumed [39].”