2-satisfiability (original) (raw)
En informatique théorique, le problème 2-SAT est un problème de décision. C'est une restriction du problème SAT qui peut être résolu en temps polynomial, alors que le problème général est NP complet. Le problème 2-SAT consiste à décider si une formule booléenne en forme normale conjonctive, dont toutes les clauses sont de taille 2, est satisfaisable. De telles formules sont appelées 2-CNF ou formules de Krom.
| Property | Value |
|---|---|
| dbo:abstract | تعرّف قابلية الإرضاء الثنائية، 2-إس إيه تي، في علوم الحاسوب، بأنها مسألة حاسوبية لتعيين قيم لمتغيرات، لكل منها قيمتان محتملتان، لإرضاء نظام القيود على أزواج المتغيرات. وتعد حالة خاصة من مسألة قابلية الإرضاء المنطقية العامة، التي يمكن أن تتضمن قيودًا على أكثر من متغيرين، ومن مسألة إرضاء القيد، التي يمكن أن تسمح بأكثر من خيارين لقيمة كل متغير. ولكن على عكس هذه المسائل الأكثر عمومية، التي تعد مسائل كثيرة حدود غير قطعية كاملة، يمكن حل قابلية الإرضاء الثنائية في زمن متعدد الحدود. يعبر عادةً عن مثيلات مسألة قابلية الإرضاء الثنائية بصيغ منطقية من نوع خاص، تدعى صيغ عطف طبيعي (سي إن إف-2) أو صيغ كروم. ويمكن التعبير عنها، بدلًا من ذلك، كنوع خاص من الرسم البياني الموجه، مخطط الاقتضاء، الذي يعبر عن متغيرات مثيل ونفيها كرؤوس في الرسم البياني، والقيود المفروضة على أزواج المتغيرات كحواف موجهة. يمكن حل نوعي المدخلات هذين في الوقت الخطي، إما بواسطة طريقة تعتمد على التتبع الخلفي أو باستخدام المكونات قوية التوصيل في مخطط الاقتضاء. يعد القرار طريقة للجمع بين أزواج القيود لإنشاء قيود صالحة إضافية، ويؤدي أيضًا إلى حل في زمن متعدد الحدود. توفر مسائل قابلية الإرضاء الثنائية أحد صنفي صيغ العطف الطبيعي الفرعيين الرئيسيين الذي يمكن حله في زمن متعدد الحدود؛ والصنف الآخر هو قابلية إرضاء هورن. يمكن تطبيق قابلية الإرضاء الثنائية على مسائل الهندسة والتجسيد المرئي التي تملك فيها كل مجموعة كائنات موقعان محتملان والهدف هو إيجاد موضع لكل كائن بحيث نتجنب التداخل مع الكائنات الأخرى. تتضمن التطبيقات الأخرى عنقدة البيانات لتقليل مجموع أقطار العناقيد، وجدولة الفصول الدراسية والرياضات، واستعادة الأشكال من المعلومات حول المقاطع العرضية. في نظرية التعقيد الحسابي، توفر قابلية الإرضاء الثنائية مثالًا لمسألة كثيرة حدود غير قطعية كاملة، التي يمكن حلها بطريقة غير حتمية باستخدام كمية تخزين لوغاريتمية وتعد من أصعب المسائل التي يمكن حلها في هذا المصدر المرتبط. يمكن إعطاء مجموعة كامل الحلول لمثيل قابلية الإرضاء الثنائية بنية الرسم البياني الوسيط، ولكن إحصاء هذه الحلول هو كثير حدود كامل وبالتالي من غير المتوقع أن يكون لها حل في زمن متعدد الحدود. تمر الحالات العشوائية بمرحلة انتقالية واضحة من الحالات القابلة للحل إلى الحالات غير القابلة للحل عندما تتجاوز نسبة القيود إلى المتغيرات السابقة القيمة 1، وهي ظاهرة متوقعة ولكنها غير مثبتة للأشكال الأكثر تعقيدًا من مسألة قابلية الإرضاء. تحتوي مسألة قابلية الإرضاء الثنائية تباين صعب حسابيًا، إيجاد تعيين صحيح يزيد عدد القيود المستوفاة، يملك خوارزمية تقريبية يعتمد استمثالها على تخمين الألعاب الفريد، وتحتوي تباين صعب آخر، إيجاد مهمة مرضية تقلل عدد المتغيرات الصحيحة، ويعد حالة اختبار مهمة للتعقيد ذات المعلمات. (ar) In computer science, 2-satisfiability, 2-SAT or just 2SAT is a computational problem of assigning values to variables, each of which has two possible values, in order to satisfy a system of constraints on pairs of variables. It is a special case of the general Boolean satisfiability problem, which can involve constraints on more than two variables, and of constraint satisfaction problems, which can allow more than two choices for the value of each variable. But in contrast to those more general problems, which are NP-complete, 2-satisfiability can be solved in polynomial time. Instances of the 2-satisfiability problem are typically expressed as Boolean formulas of a special type, called conjunctive normal form (2-CNF) or Krom formulas. Alternatively, they may be expressed as a special type of directed graph, the implication graph, which expresses the variables of an instance and their negations as vertices in a graph, and constraints on pairs of variables as directed edges. Both of these kinds of inputs may be solved in linear time, either by a method based on backtracking or by using the strongly connected components of the implication graph. Resolution, a method for combining pairs of constraints to make additional valid constraints, also leads to a polynomial time solution. The 2-satisfiability problems provide one of two major subclasses of the conjunctive normal form formulas that can be solved in polynomial time; the other of the two subclasses is Horn-satisfiability. 2-satisfiability may be applied to geometry and visualization problems in which a collection of objects each have two potential locations and the goal is to find a placement for each object that avoids overlaps with other objects. Other applications include clustering data to minimize the sum of the diameters of the clusters, classroom and sports scheduling, and recovering shapes from information about their cross-sections. In computational complexity theory, 2-satisfiability provides an example of an NL-complete problem, one that can be solved non-deterministically using a logarithmic amount of storage and that is among the hardest of the problems solvable in this resource bound. The set of all solutions to a 2-satisfiability instance can be given the structure of a median graph, but counting these solutions is #P-complete and therefore not expected to have a polynomial-time solution. Random instances undergo a sharp phase transition from solvable to unsolvable instances as the ratio of constraints to variables increases past 1, a phenomenon conjectured but unproven for more complicated forms of the satisfiability problem. A computationally difficult variation of 2-satisfiability, finding a truth assignment that maximizes the number of satisfied constraints, has an approximation algorithm whose optimality depends on the unique games conjecture, and another difficult variation, finding a satisfying assignment minimizing the number of true variables, is an important test case for parameterized complexity. (en) En informatique théorique, le problème 2-SAT est un problème de décision. C'est une restriction du problème SAT qui peut être résolu en temps polynomial, alors que le problème général est NP complet. Le problème 2-SAT consiste à décider si une formule booléenne en forme normale conjonctive, dont toutes les clauses sont de taille 2, est satisfaisable. De telles formules sont appelées 2-CNF ou formules de Krom. (fr) In informatica, 2-satisfiability, 2-SAT o semplicemente 2SAT è un problema di soddisfacibilità booleana con clausole composte da coppie di letterali. È un caso particolare (il più semplice) del problema n-SAT, ed è l'unico di cui è stata dimostrata la risolubilità in tempo polinomiale e spazio logaritmico. Più precisamente, si tratta di un problema . Al contrario, i problemi di soddisfacibilità con sono tutti NP-completi, essendo tali sia il generico SAT (per il teorema di Cook) che 3-SAT (poiché ogni problema n-SAT è riducibile a 3-SAT in tempo polinomiale). Le istanze di 2SAT sono tipicamente espresse come formule booleane di tipo particolare, dette in forma normale congiuntiva (2-CNF) o formule di Krom. In alternativa, possono essere espresse attraverso un grafo diretto, detto grafo delle implicazioni, in cui i letterali di un'istanza sono rappresentati dai vertici, e le clausole dagli archi diretti. Entrambi i tipi di istanze possono essere risolti in tempo lineare, sia con un metodo basato sul backtracking, sia utilizzando le componenti fortemente connesse del grafo delle implicazioni. La risoluzione, un metodo che combina coppie di clausole per creare ulteriori clausole valide, risolve il problema in tempo quadratico. 2SAT fornisce una delle due principali sottoclassi delle formule in CNF che possono essere risolte in tempo polinomiale, l'altra sottoclasse è la . 2SAT può essere applicato a problemi di geometria e di visualizzazione, in cui ciascun oggetto ha due possibili posizioni e l'obiettivo è trovare una posizione per ciascun oggetto che eviti sovrapposizioni con gli altri. Altre applicazioni includono il raggruppamento dei dati per ridurre al minimo la somma dei diametri dei cluster, la pianificazione delle classi e dei tornei e il riconoscimento delle forme dalle informazioni sulle loro sezioni trasversali. Nella teoria della complessità computazionale, 2SAT fornisce un esempio di problema NL-completo, che può essere risolto in modo non deterministico utilizzando una quantità di memoria logaritmica, e che è tra i problemi più difficili risolvibili con questi limiti sulle risorse. All'insieme di tutte le soluzioni per un'istanza di 2SAT può essere data la struttura di un grafo mediano, ma il conteggio di queste soluzioni è #P-completo, quindi non ci si aspetta che abbia una soluzione in tempo polinomiale. Le istanze casuali subiscono una netta transizione di fase da istanze risolvibili a istanze irrisolvibili quando il rapporto tra clausole e variabili aumenta oltre 1, un fenomeno ipotizzato ma non dimostrato per forme più complicate del problema di soddisfacibilità. Una variante computazionalmente difficile di 2SAT, trovare un'assegnazione di verità che massimizza il numero di clausole soddisfatte, ha un algoritmo di approssimazione la cui ottimalità dipende dalla congettura dei giochi unici; un'altra variante difficile, trovare un'assegnazione soddisfacente che riduce al minimo il numero di variabili vere, è un importante caso di test per la complessità parametrizzata. (it) |
| dbo:thumbnail | wiki-commons:Special:FilePath/Implication_graph.svg?width=300 |
| dbo:wikiPageID | 497640 (xsd:integer) |
| dbo:wikiPageLength | 65404 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1116600207 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:NP_(complexity) dbr:Approximation_algorithm dbr:Arc_diagram dbr:Resolution_(logic) dbr:Undirected_graph dbr:University_of_California,_Davis dbr:VLSI dbr:Vertex_cover_problem dbr:Davis–Putnam_algorithm dbr:Depth-first_search dbr:Independent_set_(graph_theory) dbr:Limit_of_a_sequence dbr:Complete_bipartite_graph dbr:Median_graph dbr:Tomography dbr:NL_(complexity) dbr:NP-complete dbr:NP-hard dbr:Conjunctive_normal_form dbr:Constraint_(mathematics) dbr:Constraint_satisfaction_problem dbr:Linear_time dbr:Logarithm dbr:Logical_conjunction dbr:Skew-symmetric_graph dbr:Clause_(logic) dbr:Completeness_(logic) dbr:Complexity_class dbr:Computational_complexity_theory dbr:Computational_problem dbr:Computer_science dbr:Horn-satisfiability dbr:Identity_matrix dbr:Majority_function dbr:Many-valued_logic dbr:Maximum_satisfiability_problem dbr:Topological_sorting dbr:Transitive_closure dbr:Transitive_relation dbr:Cut_(graph_theory) dbr:Dynamic_programming dbr:Equivalence_relation dbr:Evolutionary_tree dbr:Directed_graph dbr:Discrete_tomography dbr:Graph_automorphism dbr:Graph_drawing dbr:Graph_theory dbr:Necessary_and_sufficient_condition dbr:Strongly_connected_component dbr:Logical_equivalence dbc:NL-complete_problems dbc:Satisfiability_problems dbr:Hamming_distance dbr:Backtracking dbr:Counting_problem_(complexity) dbr:Fixed-parameter_tractable dbr:Binary_data dbr:Binary_image dbr:Heuristic dbr:Phase_transition dbr:Polyomino dbr:Tarjan's_strongly_connected_components_algorithm dbr:Diameter dbr:Directed_acyclic_graph dbr:Automatic_label_placement dbr:Boolean_expression dbr:Boolean_satisfiability_problem dbr:Pixel dbr:Polynomial-time_approximation_scheme dbr:Square_lattice dbr:Polynomial_time dbr:Approximation_ratio dbr:Data_clustering dbr:Maximum_flow dbr:Implicit_graph dbr:Kosaraju's_algorithm dbr:Metric_space dbr:RP_(complexity) dbr:Round-robin_tournament dbr:Unique_games_conjecture dbr:Vertex_(graph_theory) dbr:Exponential_time_hypothesis dbr:Immerman–Szelepcsényi_theorem dbr:Implication_graph dbr:Literal_(mathematical_logic) dbr:Path-based_strong_component_algorithm dbr:Sharp-P-complete dbr:NL-complete dbr:Semidefinite_programming dbr:Nonogram dbr:P_versus_NP_problem dbr:Parameterized_complexity dbr:True_quantified_Boolean_formula dbr:W(1) dbr:Orthogonal_convexity dbr:Boolean_logic dbr:First_order_logic dbr:Disjunction dbr:0-1_matrix dbr:Second_order_logic dbr:Existential_quantifier dbr:Truth_assignment dbr:Strongly_connected_components dbr:File:2SAT_median_graph.svg dbr:File:Implication_graph.svg dbr:File:Paint_by_numbers_Animation.gif dbr:Implicative_normal_form |
| dbp:last | Batenburg (en) Kosters (en) |
| dbp:wikiPageUsesTemplate | dbt:Good_article dbt:Harvtxt dbt:Math dbt:Mvar dbt:Reflist dbt:Short_description dbt:Harvs |
| dbp:year | 2008 (xsd:integer) 2009 (xsd:integer) |
| dct:subject | dbc:NL-complete_problems dbc:Satisfiability_problems |
| gold:hypernym | dbr:Problem |
| rdf:type | yago:WikicatNL-completeProblems yago:WikicatNP-hardProblems yago:WikicatSatisfiabilityProblems yago:Abstraction100002137 yago:Attribute100024264 yago:Condition113920835 yago:Difficulty114408086 yago:Problem114410605 dbo:Disease yago:State100024720 |
| rdfs:comment | En informatique théorique, le problème 2-SAT est un problème de décision. C'est une restriction du problème SAT qui peut être résolu en temps polynomial, alors que le problème général est NP complet. Le problème 2-SAT consiste à décider si une formule booléenne en forme normale conjonctive, dont toutes les clauses sont de taille 2, est satisfaisable. De telles formules sont appelées 2-CNF ou formules de Krom. (fr) تعرّف قابلية الإرضاء الثنائية، 2-إس إيه تي، في علوم الحاسوب، بأنها مسألة حاسوبية لتعيين قيم لمتغيرات، لكل منها قيمتان محتملتان، لإرضاء نظام القيود على أزواج المتغيرات. وتعد حالة خاصة من مسألة قابلية الإرضاء المنطقية العامة، التي يمكن أن تتضمن قيودًا على أكثر من متغيرين، ومن مسألة إرضاء القيد، التي يمكن أن تسمح بأكثر من خيارين لقيمة كل متغير. ولكن على عكس هذه المسائل الأكثر عمومية، التي تعد مسائل كثيرة حدود غير قطعية كاملة، يمكن حل قابلية الإرضاء الثنائية في زمن متعدد الحدود. (ar) In computer science, 2-satisfiability, 2-SAT or just 2SAT is a computational problem of assigning values to variables, each of which has two possible values, in order to satisfy a system of constraints on pairs of variables. It is a special case of the general Boolean satisfiability problem, which can involve constraints on more than two variables, and of constraint satisfaction problems, which can allow more than two choices for the value of each variable. But in contrast to those more general problems, which are NP-complete, 2-satisfiability can be solved in polynomial time. (en) In informatica, 2-satisfiability, 2-SAT o semplicemente 2SAT è un problema di soddisfacibilità booleana con clausole composte da coppie di letterali. È un caso particolare (il più semplice) del problema n-SAT, ed è l'unico di cui è stata dimostrata la risolubilità in tempo polinomiale e spazio logaritmico. Più precisamente, si tratta di un problema . Al contrario, i problemi di soddisfacibilità con sono tutti NP-completi, essendo tali sia il generico SAT (per il teorema di Cook) che 3-SAT (poiché ogni problema n-SAT è riducibile a 3-SAT in tempo polinomiale). (it) |
| rdfs:label | قابلية الإرضاء الثنائية (ar) 2-satisfiability (en) 2-satisfiability (it) Problème 2-SAT (fr) |
| owl:sameAs | freebase:2-satisfiability yago-res:2-satisfiability wikidata:2-satisfiability dbpedia-ar:2-satisfiability dbpedia-fr:2-satisfiability dbpedia-hu:2-satisfiability dbpedia-it:2-satisfiability https://global.dbpedia.org/id/4GDEo |
| prov:wasDerivedFrom | wikipedia-en:2-satisfiability?oldid=1116600207&ns=0 |
| foaf:depiction | wiki-commons:Special:FilePath/Paint_by_numbers_Animation.gif wiki-commons:Special:FilePath/2SAT_median_graph.svg wiki-commons:Special:FilePath/Implication_graph.svg |
| foaf:isPrimaryTopicOf | wikipedia-en:2-satisfiability |
| is dbo:wikiPageRedirects of | dbr:Maximum_2-satisfiability dbr:MAX-2-SAT dbr:2-CNF-SAT dbr:2SAT dbr:Max_2-sat dbr:Krom-clause dbr:Krom_formula dbr:Krom_formulae dbr:2-SAT dbr:MAX-2SAT |
| is dbo:wikiPageWikiLink of | dbr:List_of_computability_and_complexity_topics dbr:Book_embedding dbr:Arc_diagram dbr:Index_of_combinatorics_articles dbr:Interval_scheduling dbr:♯P-complete dbr:Maximal_independent_set dbr:Maximum_2-satisfiability dbr:Median_graph dbr:NL_(complexity) dbr:Conjunctive_normal_form dbr:MAX-2-SAT dbr:MAXEkSAT dbr:Skew-symmetric_graph dbr:Horn-satisfiability dbr:PLS_(complexity) dbr:P_(complexity) dbr:Maximum_satisfiability_problem dbr:Gadget_(computer_science) dbr:Adi_Shamir dbr:2-CNF-SAT dbr:Strongly_connected_component dbr:Harry_R._Lewis dbr:Birkhoff's_representation_theorem dbr:2SAT dbr:Automatic_label_placement dbr:Max_2-sat dbr:Satisfiability dbr:Unique_games_conjecture dbr:Uwe_Schöning dbr:Exponential_time_hypothesis dbr:Implication_graph dbr:NP-completeness dbr:NL-complete dbr:Nonogram dbr:True_quantified_Boolean_formula dbr:Krom-clause dbr:Krom_formula dbr:Krom_formulae dbr:2-SAT dbr:MAX-2SAT |
| is foaf:primaryTopic of | wikipedia-en:2-satisfiability |
