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.
| Attributes | Values |
|---|
| rdf:type
| |
| rdfs:label
| - Zeitin-Transformation (de)
- Transformation de Tseitin (fr)
- Tseitin-transformatie (nl)
- Transformação de Tseytin (pt)
- Tseytin transformation (en)
|
| rdfs:comment
| - Die Zeitin-Transformation (auch Zeitin-Verfahren, Tseitin-Transformation, Tseitin-Verfahren) bezeichnet eine Methode, mit der Formeln aus der Aussagenlogik auf eine konjunktive Normalform (KNF) gebracht werden können. Die resultierende konjunktive Normalform ist dabei im Allgemeinen nicht äquivalent, sondern nur erfüllbarkeitsäquivalent. Das Verfahren wurde von Grigori Zeitin entwickelt. (de)
- En logique, la transformation de Tseitin prend un circuit logique et produit une formule booléenne équisatisfiable en forme normale conjonctive. La transformation est linéaire. (fr)
- 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. (en)
- In de logica is de Tseitin-transformatie (ook Tseitin-afgeleide genoemd) een manier om een propositie in lineaire tijd om te zetten naar een vervulbaarheidsequivalente propositie in conjunctieve normaalvorm. De Tseitin-transformatie kan bijvoorbeeld worden gebruikt bij het DPLL-algoritme en resolutie, bewijstechnieken in . De Tseitin-transformatie is vernoemd naar G.S. Tseitin die het publiceerde in 1968. (nl)
- A transformação de Tseytin, alternativamente escrita como transformação de Tseitin tem como entrada um circuito lógico combinatório arbitrário e produz uma fórmula booleana na forma normal conjuntiva (FNC), o que pode ser resolvido através de um solucionador FNC-SAT. O comprimento da fórmula é linear no tamanho do circuito. Vetores de entrada que fazem a saída do circuito ser "verdadeira" estão na correspondência 1-para-1 com as atribuições que satisfazem a fórmula. Isto reduz o problema da satisfatibilidade do circuito em qualquer circuito (incluindo qualquer fórmula) para o problema da satisfatibilidade nas fórmulas 3-FNC. (pt)
|
| foaf:depiction
| |
| dcterms:subject
| |
| Wikipage page ID
| |
| Wikipage revision ID
| |
| Link from a Wikipage to another Wikipage
| |
| Link from a Wikipage to an external page
| |
| sameAs
| |
| dbp:wikiPageUsesTemplate
| |
| thumbnail
| |
| has abstract
| - Die Zeitin-Transformation (auch Zeitin-Verfahren, Tseitin-Transformation, Tseitin-Verfahren) bezeichnet eine Methode, mit der Formeln aus der Aussagenlogik auf eine konjunktive Normalform (KNF) gebracht werden können. Die resultierende konjunktive Normalform ist dabei im Allgemeinen nicht äquivalent, sondern nur erfüllbarkeitsäquivalent. Das Verfahren wurde von Grigori Zeitin entwickelt. (de)
- En logique, la transformation de Tseitin prend un circuit logique et produit une formule booléenne équisatisfiable en forme normale conjonctive. La transformation est linéaire. (fr)
- 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. (en)
- In de logica is de Tseitin-transformatie (ook Tseitin-afgeleide genoemd) een manier om een propositie in lineaire tijd om te zetten naar een vervulbaarheidsequivalente propositie in conjunctieve normaalvorm. De Tseitin-transformatie kan bijvoorbeeld worden gebruikt bij het DPLL-algoritme en resolutie, bewijstechnieken in . De Tseitin-transformatie is vernoemd naar G.S. Tseitin die het publiceerde in 1968. (nl)
- A transformação de Tseytin, alternativamente escrita como transformação de Tseitin tem como entrada um circuito lógico combinatório arbitrário e produz uma fórmula booleana na forma normal conjuntiva (FNC), o que pode ser resolvido através de um solucionador FNC-SAT. O comprimento da fórmula é linear no tamanho do circuito. Vetores de entrada que fazem a saída do circuito ser "verdadeira" estão na correspondência 1-para-1 com as atribuições que satisfazem a fórmula. Isto reduz o problema da satisfatibilidade do circuito em qualquer circuito (incluindo qualquer fórmula) para o problema da satisfatibilidade nas fórmulas 3-FNC. (pt)
|
| prov:wasDerivedFrom
| |
| page length (characters) of wiki page
| |
| foaf:isPrimaryTopicOf
| |
| is Link from a Wikipage to another Wikipage
of | |
| is Wikipage redirect
of | |
| is foaf:primaryTopic
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)
