Circuit satisfiability problem (original) (raw)
In der theoretischen Informatik (insbesondere in der Komplexitätstheorie) ist das Erfüllbarkeitsproblem für Schaltkreise (englisch Circuit Satisfiability Problem, CircuitSAT, CSAT) das Entscheidungsproblem, ob es für eine gegebene boolesche Schaltung eine Eingabe gibt, die den Ausgang wahr macht.
| Property | Value |
|---|---|
| dbo:abstract | In theoretical computer science, the circuit satisfiability problem (also known as CIRCUIT-SAT, CircuitSAT, CSAT, etc.) is the decision problem of determining whether a given Boolean circuit has an assignment of its inputs that makes the output true. In other words, it asks whether the inputs to a given Boolean circuit can be consistently set to 1 or 0 such that the circuit outputs 1. If that is the case, the circuit is called satisfiable. Otherwise, the circuit is called unsatisfiable. In the figure to the right, the left circuit can be satisfied by setting both inputs to be 1, but the right circuit is unsatisfiable. CircuitSAT is closely related to Boolean satisfiability problem (SAT), and likewise, has been proven to be NP-complete. It is a prototypical NP-complete problem; the Cook–Levin theorem is sometimes proved on CircuitSAT instead of on the SAT, and then CircuitSAT can be reduced to the other satisfiability problems to prove their NP-completeness. The satisfiability of a circuit containing arbitrary binary gates can be decided in time . (en) In der theoretischen Informatik (insbesondere in der Komplexitätstheorie) ist das Erfüllbarkeitsproblem für Schaltkreise (englisch Circuit Satisfiability Problem, CircuitSAT, CSAT) das Entscheidungsproblem, ob es für eine gegebene boolesche Schaltung eine Eingabe gibt, die den Ausgang wahr macht. (de) En informatique théorique, le problème de satisfaisabilité d'un circuit (aussi connu sous le nom de CIRCUIT-SAT, CircuitSAT, CSAT[réf. nécessaire], etc.) est le problème de décision consistant à déterminer si pour un circuit booléen donné, il existe une affectation de ses entrées qui rende la sortie vraie. En d'autres termes, on demande si les entrées d'un circuit booléen donné peuvent être réglées de manière cohérente sur 1 ou 0 de sorte que le circuit émette 1. Si tel est le cas, le circuit est dit satisfaisable. Sinon, le circuit est dit insatisfaisable. Sur la figure de droite, le circuit de gauche peut être satisfait en définissant les deux entrées sur 1, mais le circuit de droite n'est pas satisfaisable. CIRCUIT-SAT est étroitement lié au problème de satisfiabilité booléenne (SAT) et est NP-complet comme lui. Le théorème de Cook-Levin est parfois prouvé sur CIRCUIT-SAT plutôt que sur SAT, puis réduit aux autres problèmes de satisfiabilité pour prouver leur NP-complétude. La satisfaisabilité d'un circuit contenant portes binaires quelconques peut être décidée en temps . (fr) Na teoria da ciência da computação, o problema da satisfatibilidade de circuito (também conhecido como CIRCUITO-SAT, CircuitoSAT, CSAT, etc.) é o problema de decisão de determinar se um dado circuito Booleano tem uma atribuição das entradas, que torna a saída verdadeira. (pt) |
| dbo:thumbnail | wiki-commons:Special:FilePath/CircuitSAT.svg?width=300 |
| dbo:wikiPageID | 34599223 (xsd:integer) |
| dbo:wikiPageLength | 8679 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1121533454 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Sheffer_stroke dbr:Decision_problem dbc:NP-complete_problems dbr:NAND_gate dbr:NOR_gate dbr:Netlist dbr:NP-complete dbr:Conjunctive_normal_form dbr:Cook–Levin_theorem dbr:Functional_completeness dbr:Theoretical_computer_science dbr:Reduction_(complexity) dbc:Computational_problems dbc:Computability_theory dbr:Co-NP-complete dbr:3SAT dbr:Boolean_circuit dbr:Boolean_satisfiability_problem dbr:Planar_graph dbr:Circuit_Value_Problem dbr:Minesweeper_(video_game) dbr:NP-hardness dbr:Tseytin_transformation dbr:Satisfiability_problem dbr:File:CircuitSAT.svg |
| dbp:wikiPageUsesTemplate | dbt:Main dbt:Reflist |
| dct:subject | dbc:NP-complete_problems dbc:Computational_problems dbc:Computability_theory |
| gold:hypernym | dbr:Problem |
| rdf:type | yago:WikicatComputationalProblems yago:WikicatNP-completeProblems yago:Abstraction100002137 yago:Attribute100024264 yago:Condition113920835 yago:Difficulty114408086 yago:Problem114410605 dbo:Disease yago:State100024720 |
| rdfs:comment | In der theoretischen Informatik (insbesondere in der Komplexitätstheorie) ist das Erfüllbarkeitsproblem für Schaltkreise (englisch Circuit Satisfiability Problem, CircuitSAT, CSAT) das Entscheidungsproblem, ob es für eine gegebene boolesche Schaltung eine Eingabe gibt, die den Ausgang wahr macht. (de) Na teoria da ciência da computação, o problema da satisfatibilidade de circuito (também conhecido como CIRCUITO-SAT, CircuitoSAT, CSAT, etc.) é o problema de decisão de determinar se um dado circuito Booleano tem uma atribuição das entradas, que torna a saída verdadeira. (pt) In theoretical computer science, the circuit satisfiability problem (also known as CIRCUIT-SAT, CircuitSAT, CSAT, etc.) is the decision problem of determining whether a given Boolean circuit has an assignment of its inputs that makes the output true. In other words, it asks whether the inputs to a given Boolean circuit can be consistently set to 1 or 0 such that the circuit outputs 1. If that is the case, the circuit is called satisfiable. Otherwise, the circuit is called unsatisfiable. In the figure to the right, the left circuit can be satisfied by setting both inputs to be 1, but the right circuit is unsatisfiable. (en) En informatique théorique, le problème de satisfaisabilité d'un circuit (aussi connu sous le nom de CIRCUIT-SAT, CircuitSAT, CSAT[réf. nécessaire], etc.) est le problème de décision consistant à déterminer si pour un circuit booléen donné, il existe une affectation de ses entrées qui rende la sortie vraie. En d'autres termes, on demande si les entrées d'un circuit booléen donné peuvent être réglées de manière cohérente sur 1 ou 0 de sorte que le circuit émette 1. Si tel est le cas, le circuit est dit satisfaisable. Sinon, le circuit est dit insatisfaisable. Sur la figure de droite, le circuit de gauche peut être satisfait en définissant les deux entrées sur 1, mais le circuit de droite n'est pas satisfaisable. (fr) |
| rdfs:label | Erfüllbarkeitsproblem für Schaltkreise (de) Circuit satisfiability problem (en) Problème de satisfiabilité de circuit (fr) Problema da satisfatibilidade de circuito (pt) |
| owl:sameAs | freebase:Circuit satisfiability problem wikidata:Circuit satisfiability problem dbpedia-de:Circuit satisfiability problem dbpedia-fr:Circuit satisfiability problem dbpedia-pt:Circuit satisfiability problem https://global.dbpedia.org/id/4hpRY yago-res:Circuit satisfiability problem |
| prov:wasDerivedFrom | wikipedia-en:Circuit_satisfiability_problem?oldid=1121533454&ns=0 |
| foaf:depiction | wiki-commons:Special:FilePath/CircuitSAT.svg |
| foaf:isPrimaryTopicOf | wikipedia-en:Circuit_satisfiability_problem |
| is dbo:wikiPageRedirects of | dbr:Circuit_SAT dbr:Circuit-SAT dbr:CircuitSAT dbr:Circuit_satisfaction_problem dbr:Circuit_satisfiability dbr:CIRCUIT-SAT |
| is dbo:wikiPageWikiLink of | dbr:Light_Up_(puzzle) dbr:Circuit_SAT dbr:PLS_(complexity) dbr:List_of_NP-complete_problems dbr:Boolean_satisfiability_algorithm_heuristics dbr:Planar_SAT dbr:Minesweeper_(video_game) dbr:CSAT dbr:Non-interactive_zero-knowledge_proof dbr:Circuit-SAT dbr:CircuitSAT dbr:Circuit_satisfaction_problem dbr:Circuit_satisfiability dbr:CIRCUIT-SAT |
| is foaf:primaryTopic of | wikipedia-en:Circuit_satisfiability_problem |
