An Entity of Type: disease, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

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.

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
dbo:wikiPageID
  • 497640 (xsd:integer)
dbo:wikiPageLength
  • 65404 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 1116600207 (xsd:integer)
dbo:wikiPageWikiLink
dbp:last
  • Batenburg (en)
  • Kosters (en)
dbp:wikiPageUsesTemplate
dbp:year
  • 2008 (xsd:integer)
  • 2009 (xsd:integer)
dcterms:subject
gold:hypernym
rdf:type
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
prov:wasDerivedFrom
foaf:depiction
foaf:isPrimaryTopicOf
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License