Boolean satisfiability problem (original) (raw)
Kontentigeblo estas la problemo decidi ĉu la variabloj de donita formulo povas esti asignitaj vervaloroj (VERO aŭ FALSO) tiamaniere, ke la tuta formulo valoriĝas VERA. Egale gravas decidi, ke tia asignado ne ekzistas, implicante ke la funkcio esprimata de la formulo estas FALSA por ĉiaj asignadoj variablaj. En la lasta kazo oni diras, ke la funkcio estas nekontentigebla; alie ĝi estas kontentigebla. Por emfazi la duuma naturo de tiu problemo oni nomas ĝin kiel bulea aŭ propozicia kontentigeblo. Subkomprenate estas ke la funkcio kaj ĉiuj ties variabloj estas duum-valoraj.
| Property | Value |
|---|---|
| dbo:abstract | مسألة قابلية الإرضاء المنطقية، في المنطق وعلوم الحاسوب، (تسمى أحيانًا مسألة قابلية الإرضاء الافتراضية وتختصر إلى قابلية الإرضاء أو إس إيه تي أو بي-إس إيه تي) هي مسألة تحديد وجود ترجمة تفسيرية ترضي صيغة منطقية معينة. بمعنى آخر، تستعلم ما إذا كان يمكن استبدال متغيرات صيغة منطقية معينة باستمرار بالقيم TRUE (صح) أو FALSE (خطأ) بطريقة تكون نتيجة الصيغة TRUE. إذا طبقت هذه الحالة، تسمى الصيغة مرضية. من ناحية أخرى، في حالة عدم وجود تعيين كهذا، تكون الوظيفة المعبر عنها بواسطة الصيغة FALSE لجميع تعيينات المتغيرات المحتملة وتكون الصيغة غير مرضية. مثلًا، تعد الصيغة «a AND NOT b (إيه و نفي بي) مرضية لأنه يمكن إيجاد قيمتين a = TRUE و b = FALSE، تحققان الصيغة (a AND NOT b = TRUE). في المقابل، تعد الصيغة «a AND NOT a» غير مُرضية. تعد المسألة كثيرة الحدود غير القطعية الكاملة أول مسألة يثبت أنها مسألة قابلة للإرضاء منطقية؛ انظر مبرهنة كوك وليفين. يعني هذا أن جميع المسائل من فئة تعقيد المسألة كثيرة الحدود غير القطعية، والتي تتضمن مجموعة واسعة من مسائل القرار والتحسين الطبيعية، يصعب حلها كمسألة قابلية الإرضاء. لا توجد خوارزمية معروفة تعمل على حل جميع مسائل قابلية الإرضاء بكفاءة، ويُعتقد عمومًا أنه لا توجد خوارزمية كهذه؛ ولكن، لم يثبت هذا الاعتقاد رياضيًا، يكافئ حل سؤال ما إذا كانت مسألة قابلية الإرضاء تملك خوارزمية حدودية الزمن مسألة كثير حدود وكثير حدود غير قطعي، وهي مسألة مفتوحة شهيرة في نظرية الحوسبة. أصبحت خوارزميات مسألة قابلية الإرضاء المنطقية التجريبية منذ عام 2007 قادرة على حل حالات المسائل التي تتضمن عشرات الآلاف من المتغيرات والصيغ التي تتكون من ملايين الرموز، أي ما يكفي للعديد من مسائل قابلية الإرضاء العملية في الذكاء الاصطناعي وتصميم الدوائر الكهربائية وإثبات النظرية التلقائية مثلًا. (ar) En teoria de complexitat computacional, el problema de satisfacibilitat booleana (també conegut per les sigles SAT) és el problema de determinar si existeix una interpretació que satisfà una fórmula booleana donada. En altres paraules, es qüestiona si les variables d'una fórmula booleana es poden reemplaçar de forma consistent pels valors CERT o FALS de manera que la fórmula s'avalui a CERT. Per exemple, la fórmula "a AND NOT b" es pot satisfer amb els valors a = CERT i b = FALS, que fan la fórmula doni CERT. En canvi, la fórmula "a AND NOT a" no té cap valor d'entrada que pugui donar CERT i no es pot satisfer en cap cas. Aquest problema va ser el primer problema identificat dins la classe de complexitat NP-complet, i per tant, tots els problemes dins de la classe NP son tant complexos com SAT però no més que aquest. No es coneix cap algorisme que resolgui el problema SAT de forma òptima i es creu que no existeix, tot i que no s'ha pogut demostrar. De fet, resoldre el problema SAT amb un algorisme de temps polinòmic és equivalent a demostrar que P = NP. Tot i això, existeixen algorismes heurístics per resoldre SAT capaços de treballar amb instàncies del problema amb desenes de milers de variables i fórmules amb milions de símbols. Aquests algorismes tenen aplicacions pràctiques en problemes d'inteli·lgència artificial, disseny de circuits i demostracions automàtiques de teoremes. (ca) Problém splnitelnosti booleovské formule (anglickou zkratkou SATISFIABILITY nebo SAT) je v matematické logice úloha zjistit, zda existuje interpretace, která vyhovuje dané booleovské formuli. Jinými slovy zda proměnné daného booleovského výrazu s proměnnými (formule) mohou být nahrazeny hodnotami TRUE (pravda) nebo FALSE (nepravda) takovým způsobem, že se výsledný výraz vyhodnotí jako pravdivý (TRUE). Pokud je tomu tak, formule se nazývá splnitelná. V opačném případě výraz má hodnotu FALSE pro všechna možná přiřazení proměnných a formule je nesplnitelná. Například formule „a AND NOT b“ je splnitelná, protože po dosazení a = TRUE a b = FALSE je výraz (TRUE AND NOT FALSE) = TRUE. Naopak formule „a AND NOT a“ je nesplnitelná (jinými slovy tato formule vyjadřuje protimluv, kontradikci). SAT byl první problém, u kterého se ukázalo, že je NP-úplný; viz . To znamená, že všechny problémy ve třídě složitosti NP, která zahrnuje širokou škálu přirozených rozhodovacích a optimalizačních problémů, jsou nejméně tak obtížné jako SAT. Neexistuje žádný známý algoritmus, který by účinně (tj. v polynomiálním čase) vyřešil libovolný problém SAT, a obecně se věří, že takový algoritmus neexistuje. Přesto to nebylo dokázáno a otázka, zda pro SAT existuje polynomiálně složitý algoritmus, je ekvivalentem problému P versus NP, což je slavný otevřený problém teorie algoritmů. Existují však heuristické algoritmy schopné řešit úlohy SAT s desítkami tisíc proměnných a s vzorci sestávajícími z milionů symbolů, což je dostačující pro mnoho praktických problémů SAT, např. v oblastech umělé inteligence, a . (cs) Das Erfüllbarkeitsproblem der Aussagenlogik (SAT, von englisch satisfiability‚ Erfüllbarkeit‘) ist ein Entscheidungsproblem der theoretischen Informatik. Es beschäftigt sich mit der Frage, ob eine gegebene aussagenlogische Formel erfüllbar ist. Mit anderen Worten: Existiert eine Belegung der Variablen von mit den Werten wahr oder falsch, sodass zu wahr ausgewertet wird? SAT gehört zur Komplexitätsklasse NP der Probleme, die von einer nichtdeterministischen Turingmaschine in polynomieller Zeit gelöst werden können. Außerdem war SAT das erste Problem, für das NP-Vollständigkeit nachgewiesen wurde (Satz von Cook). Damit kann jedes Problem aus NP in polynomieller Zeit auf SAT zurückgeführt werden (Polynomialzeitreduktion). NP-vollständige Probleme stellen also eine Art obere Schranke für die Schwierigkeit von Problemen in NP dar. Eine deterministische Turingmaschine (etwa ein konventioneller Computer) kann SAT in exponentieller Zeit entscheiden, zum Beispiel durch das Aufstellen einer Wahrheitstabelle. Es ist kein effizienter Algorithmus für SAT bekannt und es wird allgemein vermutet, dass ein solcher Polynomialzeitalgorithmus nicht existiert. Die Frage, ob SAT in polynomieller Zeit gelöst werden kann, ist äquivalent zum P-NP-Problem, einem der bekanntesten offenen Probleme der theoretischen Informatik Ein Großteil der Forschung beschäftigt sich mit der Entwicklung möglichst effizienter Verfahren zur Lösung von SAT in der Praxis (sogenannter SAT-Solver). Moderne SAT-Solver können Instanzen mittlerer Schwierigkeit mit hunderten Millionen Variablen oder Klauseln in praktikabler Zeit lösen. Das ist ausreichend für praktische Anwendungen, z. B. in der formalen Verifikation, in der künstlichen Intelligenz, in der Electronic Design Automation und in verschiedenen Planungs- und Schedulingalgorithmen. Sie gehören zu den Constraint Satisfaction Problems (CSP). (de) Kontentigeblo estas la problemo decidi ĉu la variabloj de donita formulo povas esti asignitaj vervaloroj (VERO aŭ FALSO) tiamaniere, ke la tuta formulo valoriĝas VERA. Egale gravas decidi, ke tia asignado ne ekzistas, implicante ke la funkcio esprimata de la formulo estas FALSA por ĉiaj asignadoj variablaj. En la lasta kazo oni diras, ke la funkcio estas nekontentigebla; alie ĝi estas kontentigebla. Por emfazi la duuma naturo de tiu problemo oni nomas ĝin kiel bulea aŭ propozicia kontentigeblo. Subkomprenate estas ke la funkcio kaj ĉiuj ties variabloj estas duum-valoraj. (eo) In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable. SAT is the first problem that was proved to be NP-complete; see Cook–Levin theorem. This means that all problems in the complexity class NP, which includes a wide range of natural decision and optimization problems, are at most as difficult to solve as SAT. There is no known algorithm that efficiently solves each SAT problem, and it is generally believed that no such algorithm exists; yet this belief has not been proved mathematically, and resolving the question of whether SAT has a polynomial-time algorithm is equivalent to the P versus NP problem, which is a famous open problem in the theory of computing. Nevertheless, as of 2007, heuristic SAT-algorithms are able to solve problem instances involving tens of thousands of variables and formulas consisting of millions of symbols, which is sufficient for many practical SAT problems from, e.g., artificial intelligence, circuit design, and automatic theorem proving. (en) En teoría de la complejidad computacional, el Problema de satisfacibilidad booleana (también llamado SAT) fue el primer problema identificado como perteneciente a la clase de complejidad NP-completo. (es) En informatique théorique, le problème SAT ou problème de satisfaisabilité booléenne est le problème de décision, qui, étant donnée une formule de logique propositionnelle, détermine s'il existe une assignation des variables propositionnelles qui rend la formule vraie. Ce problème est important en théorie de la complexité. Il a été mis en lumière par le théorème de Cook, qui est à la base de la théorie de la NP-complétude et du problème P = NP. Le problème SAT a aussi de nombreuses applications notamment en satisfaction de contraintes, planification classique, model checking, diagnostic, et jusqu'au configurateur d'un PC ou de son système d'exploitation : on se ramène à des formules propositionnelles et on utilise un solveur SAT. (fr) 充足可能性問題（じゅうそくかのうせいもんだい、satisfiability problem, SAT）は、一つの命題論理式が与えられたとき、それに含まれる変数の値を偽 (False) あるいは真 (True) にうまく定めることによって全体の値を'真'にできるか、という問題をいう。SATisfiabilityの頭3文字を取ってしばしば「SAT」と呼ばれる。 (ja) La soddisfacibilità booleana, o soddisfacibilità proposizionale o SAT, è il problema di determinare se una formula booleana è soddisfacibile o insoddisfacibile. La formula si dice soddisfacibile se le variabili possono essere assegnate in modo che la formula assuma il valore di verità vero. Viceversa, si dice insoddisfacibile se tale assegnamento non esiste (pertanto, la funzione espressa dalla formula è identicamente falsa). (it) 충족 가능성 문제(充足可能性問題, satisfiability problem, SAT)는 어떠한 변수들로 이루어진 논리식이 주어졌을 때, 그 논리식이 참이 되는 변수값이 존재하는지를 찾는 문제이다. 만족성 문제, 만족도 문제, 만족 문제, 불린 충족 가능성 문제(boolean satisfiability problem)라고도 부른다. (ko) Problem spełnialności – zagadnienie rachunku zdań, określające czy dla danej formuły logicznej istnieje takie podstawienie (wartościowanie) zmiennych zdaniowych, żeby formuła była prawdziwa. Jest ono równoważne negacji odpowiedzi na pytanie czy „negacja tej formuły jest tautologią”. Własność polegająca na posiadaniu przez formułę logiczną takiego wartościowania, które czyni ją prawdziwą nazywana jest spełnialnością formuł logicznych. O takim wartościowaniu mówimy, że spełnia ono daną formułę i nazywamy je wartościowaniem spełniającym. Formuła zdaniowa A języka L jest spełnialna wtedy i tylko wtedy, gdy istnieją: interpretacja M języka L oraz M-wartościowanie s takie, że M╞ A [s]; w przeciwnym przypadku mówimy, że A jest niespełnialna. Problem stwierdzania, czy zadana formuła logiczna jest spełnialna, to zagadnienie istotne dla teorii złożoności obliczeniowej. W zależności od postaci formuły jest on uważany za problem łatwy (tj. istnieje algorytm wielomianowy pozwalający na jego rozwiązanie) lub trudny (tj. prawdopodobnie algorytm wielomianowy dla niego nie istnieje). Problem spełnialności jest rozstrzygalny – można wypróbować wszystkie podstawienia, których jest gdzie to liczba zmiennych w formule. Metoda ta ma więc złożoność obliczeniową wykładniczą. Istnieje też problem spełnialności formuł w koniunkcyjnej postaci normalnej (ang. CNF – conjunctional normal form), których klauzule mają nie więcej niż k literałów (k-SAT). Literałem nazywamy zmienną lub zmienną zanegowaną, klauzulą nazywamy alternatywę literałów, natomiast formuła to koniunkcja klauzul. 1-SAT i 2-SAT mają rozwiązania w P, czyli w deterministycznym czasie wielomianowym, natomiast już 3-SAT jest NP-zupełny, czyli taki, że każdy problem z klasy NP jest do niego redukowalny przy pomocy redukcji w czasie wielomianowym. (pl) In de complexiteitstheorie verwijst het vervulbaarheidsprobleem (ook bekend als SAT, van het Engelse satisfiability) naar het bepalen of een logische propositie vervuld kan worden; een propositie kan vervuld worden als er een toekenning van waar of onwaar aan de atomaire formules bestaat zodanig dat de gehele propositie waar is. (nl) Na teoria da complexidade computacional, o problema de satisfatibilidade booliana (do inglês boolean satisfiability problem, muitas vezes abreviado como SATISFIABILITY ou SAT) foi o primeiro problema identificado como pertencente à classe de complexidade NP-completo.O problema de satisfatibilidade booliana é o problema de determinar se existe uma determinada valoração para as variáveis de uma determinada fórmula booliana tal que esta valoração satisfaça esta fórmula em questão. Por exemplo, tomando como as variáveis boolianas e a expressão caso exista uma atribuição de valores de verdade para as variáveis da fórmula que torne a fórmula avaliada VERDADEIRA, esta fórmula é considera satisfatível, em contrapartida se nenhuma atribuição levou a uma avaliação da fórmula como verdadeira, ela é considerada insatisfatível. Para salientar a natureza binária deste problema, ele é referenciado freqüentemente como o problema de satisfatibilidade booliana ou proposicional. A sigla SAT também é geralmente utilizada para denotá-lo, com o entendimento implícito de que a função e suas variáveis recebem valores binários. (pt) Зада́ча здійсне́нності бу́левих фо́рмул (SAT, від англ. satisfiability) — важлива для теорії обчислювальної складності алгоритмічна задача. Об'єктом задачі SAT є , що складається тільки з назв змінних, дужок і операцій (І) (АБО) і (НІ).Задача полягає в наступному: чи можна призначити усім змінним, що трапляються у формулі, значення хибність і істина так, щоб формула стала істинною. Згідно з теоремою Кука, доведеною Стівеном Куком в 1971-му році, задача SAT для булевих формул, записаних в кон'юнктивній нормальній формі, є NP-повною. Вимога про запис у кон'юнктивній формі є важливою, оскільки, наприклад, для формул, представлених в диз'юнктивній нормальній формі, задача SAT тривіально вирішується за лінійний час від розміру запису формули. (uk) 可滿足性（英語：Satisfiability）是用來解決給定的真值方程式，是否存在一组变量赋值，使問題为可满足。布尔可滿足性問題（Boolean satisfiability problem；SAT ）屬於決定性問題，也是第一个被证明屬於NP完全的问题。此問題在電腦科學上許多的領域皆相當重要，包括、演算法、人工智慧、等等。 (zh) Зада́ча выполни́мости бу́левых фо́рмул (SAT, ВЫП) — важная для теории вычислительной сложности алгоритмическая задача. Экземпляром задачи является булева формула, состоящая только из имён переменных, скобок и операций (И), (ИЛИ) и (HE).Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной. Согласно теореме Кука, доказанной Стивеном Куком в 1971 году, задача SAT для булевых формул, записанных в конъюнктивной нормальной форме, является NP-полной. Требование о записи в конъюнктивной форме существенно, так как, например, задача SAT для формул, представленных в дизъюнктивной нормальной форме, тривиально решается за линейное время в зависимости от размера записи формулы (для выполнимости формулы требуется только наличие хотя бы одной конъюнкции, не содержащей одновременно и отрицание для некоторой переменной ). (ru) |
| dbo:thumbnail | wiki-commons:Special:FilePath/Sat_reduced_to_Clique_from_Sipser.svg?width=300 |
| dbo:wikiPageExternalLink | https://web.archive.org/web/20070208034716/http:/www.sigda.org/newsletter/index.html http://www.sigda.org http://eprints.soton.ac.uk/265003/1/jpms-date99a.pdf http://www.cc.pol.una.py/lcca/publicaciones/optimizacion/2007/Asynchronous%20Team%20Algorithms%20for%20Boolean%20Satisfiability.pdf%7C http://www.cril.univ-artois.fr/~roussel/satgame/satgame.php%3Flang=eng http://www.domagoj-babic.com/uploads/Pubs/TCOM06/tcom06.pdf%7C http://www.maxsat.udl.cat/ http://www.satcompetition.org/ http://www.satisfiability.org/ http://www.satlive.org https://eprints.soton.ac.uk/265003/1/jpms-date99a.pdf https://ghostarchive.org/archive/20221009/http:/eprints.soton.ac.uk/265003/1/jpms-date99a.pdf https://web.archive.org/web/20060219180520/http:/jsat.ewi.tudelft.nl/ https://web.archive.org/web/20070708233347/http:/www.sigda.org/newsletter/2006/eNews_061201.html http://www.eecs.umich.edu/~karem |
| dbo:wikiPageID | 4715 (xsd:integer) |
| dbo:wikiPageLength | 52424 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1117934167 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Electronic_design_automation dbr:NP_(complexity) dbr:Bounded-error_probabilistic_polynomial dbr:David_S._Johnson dbr:Algorithmics dbc:Electronic_design_automation dbr:Approximation_algorithm dbr:DPLL_algorithm dbr:University_of_Toronto dbr:Decision_problem dbr:∀ dbr:∃ dbr:Interpretation_(logic) dbr:PSPACE-complete dbr:0-1_integer_programming dbc:NP-complete_problems dbr:Cryptography dbr:Russian_Academy_of_Sciences dbr:SL_(complexity) dbr:Negation dbr:Schaefer's_dichotomy_theorem dbr:Circuit_design dbr:Clique_problem dbr:Equisatisfiable dbr:Gaussian_elimination dbr:Graph_(discrete_mathematics) dbr:Graph_coloring dbr:Model_checking dbr:NL_(complexity) dbr:NP-complete dbr:NP-hard dbr:Conflict-driven_clause_learning dbr:Conjunctive_normal_form dbr:Constraint_satisfaction_problem dbr:Contradiction dbr:Cook–Levin_theorem dbr:L_(complexity) dbr:Leonid_Levin dbr:Logic dbr:Logical_conjunction dbr:Logical_value dbr:Stephen_Cook dbr:Stochastic dbr:Complexity_class dbr:Computational_complexity_theory dbr:Computer_science dbr:Horn_clause dbr:PH_(complexity) dbr:P_(complexity) dbr:Propositional_logic dbr:Substitution_(logic) dbr:Theoretical_computer_science dbr:Maximum_satisfiability_problem dbr:P/poly dbr:BPP_(complexity) dbr:Karloff–Zwick_algorithm dbr:Karp's_21_NP-complete_problems dbr:Local_search_(constraint_satisfaction) dbr:Polynomial-time_reduction dbr:P-complete dbr:Promise_problem dbr:Exclusive_or dbr:FPGA dbr:Finite_field dbr:Formal_verification dbr:PP_(complexity) dbr:Formal_equivalence_checking dbr:Entailment dbr:Logical_disjunction dbr:First-order_predicate_calculus dbr:Quantifier_(logic) dbr:Reduction_(complexity) dbc:Boolean_algebra dbc:Satisfiability_problems dbr:Tautology_(logic) dbr:Unsatisfiable_core dbr:Artificial_intelligence dbr:APX dbc:Formal_methods dbc:Logic_in_computer_science dbr:Karp–Lipton_theorem dbr:Co-NP-complete dbr:Uninterpreted_function dbr:Disjunctive_normal_form dbr:Automated_planning_and_scheduling dbr:Automatic_test_pattern_generation dbr:Boolean_algebra_(structure) dbr:Boolean_function dbr:Planar_SAT dbr:Planar_graph dbr:Polynomial-time_approximation_scheme dbr:Polynomial_hierarchy dbr:Scheduling_algorithm dbr:Microprocessor dbr:RP_(complexity) dbr:Search_problem dbr:Second-order_logic dbr:Turing_machine dbr:Routing_(electronic_design_automation) dbr:Satisfiability dbr:Satisfiability_modulo_theories dbr:Variable_(mathematics) dbr:Logically_equivalent dbr:Sharp-SAT dbr:Exponential_time_hypothesis dbr:FNP_(complexity) dbr:FP_(complexity) dbr:Thomas_Jerome_Schaefer dbr:Sharp-P-complete dbr:NL-complete dbr:Unit_propagation dbr:Tseytin_transformation dbr:P_system dbr:P_versus_NP_problem dbr:WalkSAT dbr:Automatic_theorem_proving dbr:Boolean_rings dbr:Boolean_logic dbr:P_(complexity_class) dbr:P_=_NP_problem dbr:Valiant-Vazirani_theorem dbr:2-SAT dbr:Circuit_satisfiability dbr:Davis–Putnam–Logemann–Loveland_algorithm dbr:Polynomial-time dbr:Quantified_Boolean_formula_problem dbr:Small_o_notation dbr:Formula_(mathematical_logic) dbr:Michael_R._Garey dbr:NP_(complexity_class) dbr:File:Boolean_satisfiability_vs_true_literal_counts.png dbr:File:Sat_reduced_to_Clique_from_Sipser.svg dbr:File:Schaefer's_3-SAT_to_1-in-3-SAT_reduction.gif dbr:US_(complexity) |
| dbp:wikiPageUsesTemplate | dbt:Citation_needed dbt:Cite_book dbt:Cite_journal dbt:Color dbt:Commons_category dbt:Fontcolor dbt:Main dbt:Math dbt:Mvar dbt:Redirect dbt:Refbegin dbt:Refend dbt:Reflist dbt:Refn dbt:Short_description dbt:Tmath dbt:Logic dbt:Additional_citations_needed |
| dct:subject | dbc:Electronic_design_automation dbc:NP-complete_problems dbc:Boolean_algebra dbc:Satisfiability_problems dbc:Formal_methods dbc:Logic_in_computer_science |
| gold:hypernym | dbr:Problem |
| rdf:type | yago:WikicatNP-completeProblems yago:WikicatNP-hardProblems yago:WikicatSatisfiabilityProblems yago:Ability105616246 yago:Abstraction100002137 yago:Attribute100024264 yago:Cognition100023271 yago:Condition113920835 yago:Difficulty114408086 yago:Know-how105616786 yago:Method105660268 yago:Problem114410605 yago:PsychologicalFeature100023100 dbo:Disease yago:State100024720 yago:WikicatFormalMethods |
| rdfs:comment | Kontentigeblo estas la problemo decidi ĉu la variabloj de donita formulo povas esti asignitaj vervaloroj (VERO aŭ FALSO) tiamaniere, ke la tuta formulo valoriĝas VERA. Egale gravas decidi, ke tia asignado ne ekzistas, implicante ke la funkcio esprimata de la formulo estas FALSA por ĉiaj asignadoj variablaj. En la lasta kazo oni diras, ke la funkcio estas nekontentigebla; alie ĝi estas kontentigebla. Por emfazi la duuma naturo de tiu problemo oni nomas ĝin kiel bulea aŭ propozicia kontentigeblo. Subkomprenate estas ke la funkcio kaj ĉiuj ties variabloj estas duum-valoraj. (eo) En teoría de la complejidad computacional, el Problema de satisfacibilidad booleana (también llamado SAT) fue el primer problema identificado como perteneciente a la clase de complejidad NP-completo. (es) 充足可能性問題（じゅうそくかのうせいもんだい、satisfiability problem, SAT）は、一つの命題論理式が与えられたとき、それに含まれる変数の値を偽 (False) あるいは真 (True) にうまく定めることによって全体の値を'真'にできるか、という問題をいう。SATisfiabilityの頭3文字を取ってしばしば「SAT」と呼ばれる。 (ja) La soddisfacibilità booleana, o soddisfacibilità proposizionale o SAT, è il problema di determinare se una formula booleana è soddisfacibile o insoddisfacibile. La formula si dice soddisfacibile se le variabili possono essere assegnate in modo che la formula assuma il valore di verità vero. Viceversa, si dice insoddisfacibile se tale assegnamento non esiste (pertanto, la funzione espressa dalla formula è identicamente falsa). (it) 충족 가능성 문제(充足可能性問題, satisfiability problem, SAT)는 어떠한 변수들로 이루어진 논리식이 주어졌을 때, 그 논리식이 참이 되는 변수값이 존재하는지를 찾는 문제이다. 만족성 문제, 만족도 문제, 만족 문제, 불린 충족 가능성 문제(boolean satisfiability problem)라고도 부른다. (ko) In de complexiteitstheorie verwijst het vervulbaarheidsprobleem (ook bekend als SAT, van het Engelse satisfiability) naar het bepalen of een logische propositie vervuld kan worden; een propositie kan vervuld worden als er een toekenning van waar of onwaar aan de atomaire formules bestaat zodanig dat de gehele propositie waar is. (nl) 可滿足性（英語：Satisfiability）是用來解決給定的真值方程式，是否存在一组变量赋值，使問題为可满足。布尔可滿足性問題（Boolean satisfiability problem；SAT ）屬於決定性問題，也是第一个被证明屬於NP完全的问题。此問題在電腦科學上許多的領域皆相當重要，包括、演算法、人工智慧、等等。 (zh) مسألة قابلية الإرضاء المنطقية، في المنطق وعلوم الحاسوب، (تسمى أحيانًا مسألة قابلية الإرضاء الافتراضية وتختصر إلى قابلية الإرضاء أو إس إيه تي أو بي-إس إيه تي) هي مسألة تحديد وجود ترجمة تفسيرية ترضي صيغة منطقية معينة. بمعنى آخر، تستعلم ما إذا كان يمكن استبدال متغيرات صيغة منطقية معينة باستمرار بالقيم TRUE (صح) أو FALSE (خطأ) بطريقة تكون نتيجة الصيغة TRUE. إذا طبقت هذه الحالة، تسمى الصيغة مرضية. من ناحية أخرى، في حالة عدم وجود تعيين كهذا، تكون الوظيفة المعبر عنها بواسطة الصيغة FALSE لجميع تعيينات المتغيرات المحتملة وتكون الصيغة غير مرضية. مثلًا، تعد الصيغة «a AND NOT b (إيه و نفي بي) مرضية لأنه يمكن إيجاد قيمتين a = TRUE و b = FALSE، تحققان الصيغة (a AND NOT b = TRUE). في المقابل، تعد الصيغة «a AND NOT a» غير مُرضية. (ar) En teoria de complexitat computacional, el problema de satisfacibilitat booleana (també conegut per les sigles SAT) és el problema de determinar si existeix una interpretació que satisfà una fórmula booleana donada. En altres paraules, es qüestiona si les variables d'una fórmula booleana es poden reemplaçar de forma consistent pels valors CERT o FALS de manera que la fórmula s'avalui a CERT. Per exemple, la fórmula "a AND NOT b" es pot satisfer amb els valors a = CERT i b = FALS, que fan la fórmula doni CERT. En canvi, la fórmula "a AND NOT a" no té cap valor d'entrada que pugui donar CERT i no es pot satisfer en cap cas. (ca) Problém splnitelnosti booleovské formule (anglickou zkratkou SATISFIABILITY nebo SAT) je v matematické logice úloha zjistit, zda existuje interpretace, která vyhovuje dané booleovské formuli. Jinými slovy zda proměnné daného booleovského výrazu s proměnnými (formule) mohou být nahrazeny hodnotami TRUE (pravda) nebo FALSE (nepravda) takovým způsobem, že se výsledný výraz vyhodnotí jako pravdivý (TRUE). Pokud je tomu tak, formule se nazývá splnitelná. V opačném případě výraz má hodnotu FALSE pro všechna možná přiřazení proměnných a formule je nesplnitelná. Například formule „a AND NOT b“ je splnitelná, protože po dosazení a = TRUE a b = FALSE je výraz (TRUE AND NOT FALSE) = TRUE. Naopak formule „a AND NOT a“ je nesplnitelná (jinými slovy tato formule vyjadřuje protimluv, kontradikci). (cs) In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a A (en) Das Erfüllbarkeitsproblem der Aussagenlogik (SAT, von englisch satisfiability‚ Erfüllbarkeit‘) ist ein Entscheidungsproblem der theoretischen Informatik. Es beschäftigt sich mit der Frage, ob eine gegebene aussagenlogische Formel erfüllbar ist. Mit anderen Worten: Existiert eine Belegung der Variablen von mit den Werten wahr oder falsch, sodass zu wahr ausgewertet wird? Sie gehören zu den Constraint Satisfaction Problems (CSP). (de) En informatique théorique, le problème SAT ou problème de satisfaisabilité booléenne est le problème de décision, qui, étant donnée une formule de logique propositionnelle, détermine s'il existe une assignation des variables propositionnelles qui rend la formule vraie. (fr) Problem spełnialności – zagadnienie rachunku zdań, określające czy dla danej formuły logicznej istnieje takie podstawienie (wartościowanie) zmiennych zdaniowych, żeby formuła była prawdziwa. Jest ono równoważne negacji odpowiedzi na pytanie czy „negacja tej formuły jest tautologią”. Problem spełnialności jest rozstrzygalny – można wypróbować wszystkie podstawienia, których jest gdzie to liczba zmiennych w formule. Metoda ta ma więc złożoność obliczeniową wykładniczą. (pl) Na teoria da complexidade computacional, o problema de satisfatibilidade booliana (do inglês boolean satisfiability problem, muitas vezes abreviado como SATISFIABILITY ou SAT) foi o primeiro problema identificado como pertencente à classe de complexidade NP-completo.O problema de satisfatibilidade booliana é o problema de determinar se existe uma determinada valoração para as variáveis de uma determinada fórmula booliana tal que esta valoração satisfaça esta fórmula em questão. Por exemplo, tomando como as variáveis boolianas e a expressão caso exista uma atribuição de valores de verdade para as variáveis da fórmula que torne a fórmula avaliada VERDADEIRA, esta fórmula é considera satisfatível, em contrapartida se nenhuma atribuição levou a uma avaliação da fórmula como verdadeira, ela é (pt) Зада́ча выполни́мости бу́левых фо́рмул (SAT, ВЫП) — важная для теории вычислительной сложности алгоритмическая задача. Экземпляром задачи является булева формула, состоящая только из имён переменных, скобок и операций (И), (ИЛИ) и (HE).Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной. (ru) Зада́ча здійсне́нності бу́левих фо́рмул (SAT, від англ. satisfiability) — важлива для теорії обчислювальної складності алгоритмічна задача. Об'єктом задачі SAT є , що складається тільки з назв змінних, дужок і операцій (І) (АБО) і (НІ).Задача полягає в наступному: чи можна призначити усім змінним, що трапляються у формулі, значення хибність і істина так, щоб формула стала істинною. (uk) |
| rdfs:label | مسألة قابلية الإرضاء المنطقية (ar) Problema de satisfacibilitat booleana (ca) Problém splnitelnosti booleovské formule (cs) Erfüllbarkeitsproblem der Aussagenlogik (de) Bulea plenumebloproblemo (eo) Problema de satisfacibilidad booleana (es) Boolean satisfiability problem (en) Problème SAT (fr) Soddisfacibilità booleana (it) 충족 가능성 문제 (ko) 充足可能性問題 (ja) Vervulbaarheidsprobleem (nl) Problema de satisfatibilidade booliana (pt) Problem spełnialności (pl) Задача выполнимости булевых формул (ru) Задача здійсненності булевих формул (uk) 布尔可满足性问题 (zh) |
| owl:sameAs | freebase:Boolean satisfiability problem yago-res:Boolean satisfiability problem wikidata:Boolean satisfiability problem dbpedia-ar:Boolean satisfiability problem dbpedia-ca:Boolean satisfiability problem dbpedia-cs:Boolean satisfiability problem dbpedia-de:Boolean satisfiability problem dbpedia-eo:Boolean satisfiability problem dbpedia-es:Boolean satisfiability problem dbpedia-fa:Boolean satisfiability problem dbpedia-fr:Boolean satisfiability problem dbpedia-he:Boolean satisfiability problem dbpedia-hu:Boolean satisfiability problem dbpedia-it:Boolean satisfiability problem dbpedia-ja:Boolean satisfiability problem dbpedia-ko:Boolean satisfiability problem dbpedia-nl:Boolean satisfiability problem dbpedia-pl:Boolean satisfiability problem dbpedia-pt:Boolean satisfiability problem dbpedia-ru:Boolean satisfiability problem dbpedia-sh:Boolean satisfiability problem dbpedia-simple:Boolean satisfiability problem dbpedia-sr:Boolean satisfiability problem dbpedia-th:Boolean satisfiability problem dbpedia-uk:Boolean satisfiability problem dbpedia-zh:Boolean satisfiability problem https://global.dbpedia.org/id/51oKL |
| prov:wasDerivedFrom | wikipedia-en:Boolean_satisfiability_problem?oldid=1117934167&ns=0 |
| foaf:depiction | wiki-commons:Special:FilePath/Boolean_satisfiability_vs_true_literal_counts.png wiki-commons:Special:FilePath/Sat_reduced_to_Clique_from_Sipser.svg wiki-commons:Special:FilePath/Schaefer's_3-SAT_to_1-in-3-SAT_reduction.gif |
| foaf:isPrimaryTopicOf | wikipedia-en:Boolean_satisfiability_problem |
| is dbo:wikiPageDisambiguates of | dbr:Boolean dbr:SAT_(disambiguation) |
| is dbo:wikiPageRedirects of | dbr:K-SAT dbr:K-cnf-sat dbr:1-in-3-SAT dbr:One-in-three_3SAT dbr:3-satisfiability dbr:3cnf dbr:3cnf-sat dbr:3cnfsat dbr:Algorithms_for_solving_SAT dbr:Parallel_SAT_solver dbr:Boolean_SAT_solver dbr:3-SAT dbr:3SAT dbr:Methods_for_solving_SAT dbr:Algorithms_for_solving_the_boolean_satisfiability_problem dbr:CNF-SAT dbr:CNFSAT dbr:List_of_SAT_solvers dbr:Boolean_SAT dbr:Boolean_Satisfiability dbr:Boolean_satisfiability dbr:Linear_SAT dbr:Propositional_satisfiability dbr:Propositional_satisfiability_problem dbr:Satisfiability_Problem dbr:Satisfiability_of_boolean_expressions dbr:XOR-SAT dbr:XOR-satisfiability dbr:SAT_problem dbr:SAT_solving dbr:Counted_Boolean_Satisfiability_Problem dbr:Unique-SAT dbr:Unambiguous_SAT |
| is dbo:wikiPageWikiLink of | dbr:BSAT dbr:Program_synthesis dbr:Quine–McCluskey_algorithm dbr:Satz_(SAT_solver) dbr:Science_and_technology_in_Ukraine dbr:Elimination_theory dbr:Entropy_compression dbr:Entscheidungsproblem dbr:Enumeration_algorithm dbr:List_of_computability_and_complexity_topics dbr:Millennium_Prize_Problems dbr:NP_(complexity) dbr:Negation_normal_form dbr:MAX-3SAT dbr:Membrane_computing dbr:Symmetric_Boolean_function dbr:Probabilistic_programming dbr:Bart_Selman dbr:Book_embedding dbr:Deterministic_finite_automaton dbr:Algorithm_selection dbr:Algorithmic_Lovász_local_lemma dbr:Algorithmic_efficiency dbr:Alloy_(specification_language) dbr:List_of_important_publications_in_theoretical_computer_science dbr:Resolution_(logic) dbr:Richard_Lipton dbr:Richard_M._Karp dbr:DIMACS dbr:DPLL(T) dbr:DPLL_algorithm dbr:Vertex_cover dbr:Vertex_cover_in_hypergraphs dbr:Decision_problem dbr:Index_of_combinatorics_articles dbr:Interval_scheduling dbr:Quantum_computing dbr:List_of_mathematical_proofs dbr:PSPACE-complete dbr:K-SAT dbr:K-cnf-sat dbr:Not-all-equal_3-satisfiability dbr:Timeline_of_artificial_intelligence dbr:♯P dbr:♯P-completeness_of_01-permanent dbr:1-in-3-SAT dbr:Cristopher_Moore dbr:SL_(complexity) dbr:Oracle_machine dbr:Valiant–Vazirani_theorem dbr:Schaefer's_dichotomy_theorem dbr:One-in-three_3SAT dbr:Clique_problem dbr:Co-NP dbr:Gap_reduction dbr:George_Boole dbr:George_Logemann dbr:Glossary_of_artificial_intelligence dbr:Model_checking dbr:NLTS_Conjecture dbr:Concolic_testing dbr:Conflict-driven_clause_learning dbr:Conjunctive_normal_form dbr:Constraint_programming dbr:Constraint_satisfaction dbr:Constraint_satisfaction_problem dbr:Cook–Levin_theorem dbr:Optical_computing dbr:Leonard_Adleman dbr:MAXEkSAT dbr:Simulated_annealing dbr:Stephen_Cook dbr:Computational_complexity dbr:Computational_complexity_theory dbr:Computational_hardness_assumption dbr:ZYpp dbr:Function_problem dbr:Horn-satisfiability dbr:Horn_clause dbr:PCP_theorem dbr:PLS_(complexity) dbr:Post_correspondence_problem dbr:Propositional_directed_acyclic_graph dbr:Spectrum_of_a_sentence dbr:Max/min_CSP/Ones_classification_theorems dbr:Maximum_satisfiability_problem dbr:Time_complexity dbr:TwixT dbr:GRASP_(SAT_solver) dbr:Galactic_algorithm dbr:Karloff–Zwick_algorithm dbr:Karp's_21_NP-complete_problems dbr:List_of_Boolean_algebra_topics dbr:Local_search_(optimization) dbr:Logic_programming dbr:Minimum-weight_triangulation dbr:P-complete dbr:3-satisfiability dbr:3cnf dbr:3cnf-sat dbr:3cnfsat dbr:Algorithms_for_solving_SAT dbr:3-dimensional_matching dbr:Daniel_J._Hulme dbr:Alternating_Turing_machine dbr:NuSMV dbr:PP_(complexity) dbr:Pangram dbr:Parallel_SAT_solver dbr:Cavity_method dbr:Difference-map_algorithm dbr:Differential_cryptanalysis dbr:Formal_equivalence_checking dbr:Isolation_lemma dbr:João_Marques_Silva dbr:Kazuo_Iwama_(computer_scientist) dbr:Knowledge-based_configuration dbr:List_of_NP-complete_problems dbr:Reduction_(complexity) dbr:2-satisfiability dbr:Harry_R._Lewis dbr:Heyting_algebra dbr:Hilary_Putnam dbr:Tautology_(logic) dbr:Boolean_SAT_solver dbr:Hyper-heuristic dbr:Unsatisfiable_core dbr:Social_golfer_problem dbr:APX dbr:Karp–Lipton_theorem dbr:Binary_decision_diagram dbr:Symbolic_artificial_intelligence dbr:SystemVerilog dbr:Co-NP-complete dbr:Heyawake dbr:Holographic_algorithm dbr:Taut dbr:Disjunctive_normal_form dbr:3-SAT dbr:3SAT dbr:Automated_reasoning dbr:Automatic_test_pattern_generation dbr:Boole's_expansion_theorem dbr:Boolean dbr:Boolean_algebra dbr:Boolean_satisfiability_algorithm_heuristics dbr:Planar_SAT dbr:Polynomial_hierarchy dbr:Circuit_Value_Problem dbr:Circuit_satisfiability_problem dbr:Methods_for_solving_SAT dbr:Ian_Gent dbr:Algorithms_for_solving_the_boolean_satisfiability_problem dbr:Rainbow-independent_set dbr:Chaff_algorithm dbr:CNF-SAT dbr:CNFSAT dbr:Model-based_testing dbr:SAT_(disambiguation) dbr:SAT_solver dbr:SNP_(complexity) dbr:Satisfiability dbr:Satisfiability_modulo_theories dbr:System_on_a_chip dbr:USAT dbr:Vienna_Summer_of_Logic dbr:Vijay_Vazirani dbr:Nerode_Prize dbr:Nike_Sun dbr:Uwe_Schöning dbr:Satplan dbr:Sharp-SAT dbr:Expert_system dbr:Exponential_time_hypothesis dbr:FKT_algorithm dbr:Implication_graph dbr:List_of_volunteer_computing_projects dbr:Thomas_Jerome_Schaefer dbr:NP-completeness dbr:NP-hardness dbr:NP-intermediate dbr:Natural_proof dbr:Planning_Domain_Definition_Language dbr:Tseytin_transformation dbr:Solver dbr:Second-order_propositional_logic dbr:List_of_SAT_solvers dbr:P_system dbr:P_versus_NP_problem dbr:WalkSAT dbr:True_quantified_Boolean_formula dbr:Structural_complexity_theory dbr:Tentai_Show dbr:Boolean_SAT dbr:Boolean_Satisfiability dbr:Boolean_satisfiability dbr:Linear_SAT dbr:Propositional_satisfiability dbr:Propositional_satisfiability_problem dbr:Satisfiability_Problem dbr:Satisfiability_of_boolean_expressions dbr:XOR-SAT dbr:XOR-satisfiability dbr:SAT_problem dbr:SAT_solving dbr:Counted_Boolean_Satisfiability_Problem dbr:Unique-SAT dbr:Unambiguous_SAT |
| is dbp:class of | dbr:DPLL_algorithm |
| is foaf:primaryTopic of | wikipedia-en:Boolean_satisfiability_problem |
