| http://dbpedia.org/ontology/abstract
|
In de complexiteitstheorie verwijst het ve … 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. zodanig dat de gehele propositie waar is.
, La soddisfacibilità booleana, o soddisfaci … 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).essa dalla formula è identicamente falsa).
, 可滿足性（英語：Satisfiability）是用來解決給定的真值方程式，是否存在一组变量赋值，使問題为可满足。布尔可滿足性問題（Boolean satisfiability problem；SAT ）屬於決定性問題，也是第一个被证明屬於NP完全的问题。此問題在電腦科學上許多的領域皆相當重要，包括、演算法、人工智慧、等等。
, En informatique théorique, le problème SAT … 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.sitionnelles et on utilise un solveur SAT.
, Na teoria da complexidade computacional, o … 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.e suas variáveis recebem valores binários.
, Зада́ча выполни́мости бу́левых фо́рмул (SA … Зада́ча выполни́мости бу́левых фо́рмул (SAT, ВЫП) — важная для теории вычислительной сложности алгоритмическая задача. Экземпляром задачи является булева формула, состоящая только из имён переменных, скобок и операций (И), (ИЛИ) и (HE).Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной. Согласно теореме Кука, доказанной Стивеном Куком в 1971 году, задача SAT для булевых формул, записанных в конъюнктивной нормальной форме, является NP-полной. Требование о записи в конъюнктивной форме существенно, так как, например, задача SAT для формул, представленных в дизъюнктивной нормальной форме, тривиально решается за линейное время в зависимости от размера записи формулы (для выполнимости формулы требуется только наличие хотя бы одной конъюнкции, не содержащей одновременно и отрицание для некоторой переменной ).но и отрицание для некоторой переменной ).
, Problém splnitelnosti booleovské formule ( … 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 ., např. v oblastech umělé inteligence, a .
, 充足可能性問題（じゅうそくかのうせいもんだい、satisfiability problem, SAT）は、一つの命題論理式が与えられたとき、それに含まれる変数の値を偽 (False) あるいは真 (True) にうまく定めることによって全体の値を'真'にできるか、という問題をいう。SATisfiabilityの頭3文字を取ってしばしば「SAT」と呼ばれる。
, In logic and computer science, the Boolean … 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.uit design, and automatic theorem proving.
, Зада́ча здійсне́нності бу́левих фо́рмул (S … Зада́ча здійсне́нності бу́левих фо́рмул (SAT, від англ. satisfiability) — важлива для теорії обчислювальної складності алгоритмічна задача. Об'єктом задачі SAT є , що складається тільки з назв змінних, дужок і операцій (І) (АБО) і (НІ).Задача полягає в наступному: чи можна призначити усім змінним, що трапляються у формулі, значення хибність і істина так, щоб формула стала істинною. Згідно з теоремою Кука, доведеною Стівеном Куком в 1971-му році, задача SAT для булевих формул, записаних в кон'юнктивній нормальній формі, є NP-повною. Вимога про запис у кон'юнктивній формі є важливою, оскільки, наприклад, для формул, представлених в диз'юнктивній нормальній формі, задача SAT тривіально вирішується за лінійний час від розміру запису формули.а лінійний час від розміру запису формули.
, 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.
, En teoria de complexitat computacional, el … 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. i demostracions automàtiques de teoremes.
, Das Erfüllbarkeitsproblem der Aussagenlogi … 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).en Constraint Satisfaction Problems (CSP).
, Kontentigeblo estas la problemo decidi ĉu … 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.aj ĉiuj ties variabloj estas duum-valoraj.
, 충족 가능성 문제(充足可能性問題, satisfiability problem, SAT)는 어떠한 변수들로 이루어진 논리식이 주어졌을 때, 그 논리식이 참이 되는 변수값이 존재하는지를 찾는 문제이다. 만족성 문제, 만족도 문제, 만족 문제, 불린 충족 가능성 문제(boolean satisfiability problem)라고도 부른다.
, Problem spełnialności – zagadnienie rachun … 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.zy pomocy redukcji w czasie wielomianowym.
, مسألة قابلية الإرضاء المنطقية، في المنطق و … مسألة قابلية الإرضاء المنطقية، في المنطق وعلوم الحاسوب، (تسمى أحيانًا مسألة قابلية الإرضاء الافتراضية وتختصر إلى قابلية الإرضاء أو إس إيه تي أو بي-إس إيه تي) هي مسألة تحديد وجود ترجمة تفسيرية ترضي صيغة منطقية معينة. بمعنى آخر، تستعلم ما إذا كان يمكن استبدال متغيرات صيغة منطقية معينة باستمرار بالقيم TRUE (صح) أو FALSE (خطأ) بطريقة تكون نتيجة الصيغة TRUE. إذا طبقت هذه الحالة، تسمى الصيغة مرضية. من ناحية أخرى، في حالة عدم وجود تعيين كهذا، تكون الوظيفة المعبر عنها بواسطة الصيغة FALSE لجميع تعيينات المتغيرات المحتملة وتكون الصيغة غير مرضية. مثلًا، تعد الصيغة «a AND NOT b (إيه و نفي بي) مرضية لأنه يمكن إيجاد قيمتين a = TRUE و b = FALSE، تحققان الصيغة (a AND NOT b = TRUE). في المقابل، تعد الصيغة «a AND NOT a» غير مُرضية. تعد المسألة كثيرة الحدود غير القطعية الكاملة أول مسألة يثبت أنها مسألة قابلة للإرضاء منطقية؛ انظر مبرهنة كوك وليفين. يعني هذا أن جميع المسائل من فئة تعقيد المسألة كثيرة الحدود غير القطعية، والتي تتضمن مجموعة واسعة من مسائل القرار والتحسين الطبيعية، يصعب حلها كمسألة قابلية الإرضاء. لا توجد خوارزمية معروفة تعمل على حل جميع مسائل قابلية الإرضاء بكفاءة، ويُعتقد عمومًا أنه لا توجد خوارزمية كهذه؛ ولكن، لم يثبت هذا الاعتقاد رياضيًا، يكافئ حل سؤال ما إذا كانت مسألة قابلية الإرضاء تملك خوارزمية حدودية الزمن مسألة كثير حدود وكثير حدود غير قطعي، وهي مسألة مفتوحة شهيرة في نظرية الحوسبة. أصبحت خوارزميات مسألة قابلية الإرضاء المنطقية التجريبية منذ عام 2007 قادرة على حل حالات المسائل التي تتضمن عشرات الآلاف من المتغيرات والصيغ التي تتكون من ملايين الرموز، أي ما يكفي للعديد من مسائل قابلية الإرضاء العملية في الذكاء الاصطناعي وتصميم الدوائر الكهربائية وإثبات النظرية التلقائية مثلًا.الكهربائية وإثبات النظرية التلقائية مثلًا.
|
| http://dbpedia.org/ontology/thumbnail
|
http://commons.wikimedia.org/wiki/Special:FilePath/Sat_reduced_to_Clique_from_Sipser.svg?width=300 +
|
| http://dbpedia.org/ontology/wikiPageExternalLink
|
http://www.satlive.org +
, http://www.domagoj-babic.com/uploads/Pubs/TCOM06/tcom06.pdf%7C +
, https://eprints.soton.ac.uk/265003/1/jpms-date99a.pdf +
, http://www.sigda.org +
, https://web.archive.org/web/20060219180520/http:/jsat.ewi.tudelft.nl/ +
, http://www.cc.pol.una.py/lcca/publicaciones/optimizacion/2007/Asynchronous%20Team%20Algorithms%20for%20Boolean%20Satisfiability.pdf%7C +
, https://web.archive.org/web/20070208034716/http:/www.sigda.org/newsletter/index.html +
, http://www.maxsat.udl.cat/ +
, http://www.eecs.umich.edu/~karem +
, https://ghostarchive.org/archive/20221009/http:/eprints.soton.ac.uk/265003/1/jpms-date99a.pdf +
, http://www.cril.univ-artois.fr/~roussel/satgame/satgame.php%3Flang=eng +
, https://web.archive.org/web/20070708233347/http:/www.sigda.org/newsletter/2006/eNews_061201.html +
, http://www.satcompetition.org/ +
, http://www.satisfiability.org/ +
, http://eprints.soton.ac.uk/265003/1/jpms-date99a.pdf +
|
| http://dbpedia.org/ontology/wikiPageID
|
4715
|
| http://dbpedia.org/ontology/wikiPageLength
|
52424
|
| http://dbpedia.org/ontology/wikiPageRevisionID
|
1117934167
|
| http://dbpedia.org/ontology/wikiPageWikiLink
|
http://dbpedia.org/resource/Horn_clause +
, http://dbpedia.org/resource/PP_%28complexity%29 +
, http://dbpedia.org/resource/FPGA +
, http://dbpedia.org/resource/Automated_planning_and_scheduling +
, http://dbpedia.org/resource/Stephen_Cook +
, http://dbpedia.org/resource/Polynomial-time_reduction +
, http://dbpedia.org/resource/Variable_%28mathematics%29 +
, http://dbpedia.org/resource/%E2%88%83 +
, http://dbpedia.org/resource/Boolean_function +
, http://dbpedia.org/resource/%E2%88%80 +
, http://dbpedia.org/resource/Satisfiability_modulo_theories +
, http://dbpedia.org/resource/BPP_%28complexity%29 +
, http://dbpedia.org/resource/DPLL_algorithm +
, http://dbpedia.org/resource/Logical_value +
, http://dbpedia.org/resource/RP_%28complexity%29 +
, http://dbpedia.org/resource/Promise_problem +
, http://dbpedia.org/resource/Cook%E2%80%93Levin_theorem +
, http://dbpedia.org/resource/Tautology_%28logic%29 +
, http://dbpedia.org/resource/Automatic_test_pattern_generation +
, http://dbpedia.org/resource/Formal_verification +
, http://dbpedia.org/resource/Boolean_logic +
, http://dbpedia.org/resource/Model_checking +
, http://dbpedia.org/resource/Substitution_%28logic%29 +
, http://dbpedia.org/resource/Graph_%28discrete_mathematics%29 +
, http://dbpedia.org/resource/PSPACE-complete +
, http://dbpedia.org/resource/NP_%28complexity%29 +
, http://dbpedia.org/resource/Polynomial_hierarchy +
, http://dbpedia.org/resource/Search_problem +
, http://dbpedia.org/resource/FNP_%28complexity%29 +
, http://dbpedia.org/resource/University_of_Toronto +
, http://dbpedia.org/resource/Constraint_satisfaction_problem +
, http://dbpedia.org/resource/Logical_conjunction +
, http://dbpedia.org/resource/Approximation_algorithm +
, http://dbpedia.org/resource/Disjunctive_normal_form +
, http://dbpedia.org/resource/Cryptography +
, http://dbpedia.org/resource/Clique_problem +
, http://dbpedia.org/resource/Satisfiability +
, http://dbpedia.org/resource/Entailment +
, http://dbpedia.org/resource/David_S._Johnson +
, http://dbpedia.org/resource/Graph_coloring +
, http://dbpedia.org/resource/Second-order_logic +
, http://dbpedia.org/resource/Decision_problem +
, http://dbpedia.org/resource/Interpretation_%28logic%29 +
, http://dbpedia.org/resource/FP_%28complexity%29 +
, http://dbpedia.org/resource/Logically_equivalent +
, http://dbpedia.org/resource/First-order_predicate_calculus +
, http://dbpedia.org/resource/Category:Formal_methods +
, http://dbpedia.org/resource/Category:Logic_in_computer_science +
, http://dbpedia.org/resource/Circuit_design +
, http://dbpedia.org/resource/L_%28complexity%29 +
, http://dbpedia.org/resource/APX +
, http://dbpedia.org/resource/Formula_%28mathematical_logic%29 +
, http://dbpedia.org/resource/Polynomial-time_approximation_scheme +
, http://dbpedia.org/resource/Thomas_Jerome_Schaefer +
, http://dbpedia.org/resource/Computational_complexity_theory +
, http://dbpedia.org/resource/Contradiction +
, http://dbpedia.org/resource/P_%28complexity%29 +
, http://dbpedia.org/resource/PH_%28complexity%29 +
, http://dbpedia.org/resource/P_versus_NP_problem +
, http://dbpedia.org/resource/Theoretical_computer_science +
, http://dbpedia.org/resource/Polynomial-time +
, http://dbpedia.org/resource/Reduction_%28complexity%29 +
, http://dbpedia.org/resource/Maximum_satisfiability_problem +
, http://dbpedia.org/resource/Finite_field +
, http://dbpedia.org/resource/Artificial_intelligence +
, http://dbpedia.org/resource/Turing_machine +
, http://dbpedia.org/resource/Category:Boolean_algebra +
, http://dbpedia.org/resource/Bounded-error_probabilistic_polynomial +
, http://dbpedia.org/resource/Boolean_algebra_%28structure%29 +
, http://dbpedia.org/resource/Exclusive_or +
, http://dbpedia.org/resource/Leonid_Levin +
, http://dbpedia.org/resource/Planar_graph +
, http://dbpedia.org/resource/Sharp-SAT +
, http://dbpedia.org/resource/Russian_Academy_of_Sciences +
, http://dbpedia.org/resource/Exponential_time_hypothesis +
, http://dbpedia.org/resource/Planar_SAT +
, http://dbpedia.org/resource/Scheduling_algorithm +
, http://dbpedia.org/resource/Co-NP-complete +
, http://dbpedia.org/resource/Logical_disjunction +
, http://dbpedia.org/resource/Uninterpreted_function +
, http://dbpedia.org/resource/Unsatisfiable_core +
, http://dbpedia.org/resource/P_system +
, http://dbpedia.org/resource/Stochastic +
, http://dbpedia.org/resource/Karp%E2%80%93Lipton_theorem +
, http://dbpedia.org/resource/P_%28complexity_class%29 +
, http://dbpedia.org/resource/P_=_NP_problem +
, http://dbpedia.org/resource/Automatic_theorem_proving +
, http://dbpedia.org/resource/Boolean_rings +
, http://dbpedia.org/resource/Unit_propagation +
, http://dbpedia.org/resource/WalkSAT +
, http://dbpedia.org/resource/Sharp-P-complete +
, http://dbpedia.org/resource/NL-complete +
, http://dbpedia.org/resource/Michael_R._Garey +
, http://dbpedia.org/resource/NP_%28complexity_class%29 +
, http://dbpedia.org/resource/Algorithmics +
, http://dbpedia.org/resource/Quantified_Boolean_formula_problem +
, http://dbpedia.org/resource/Quantifier_%28logic%29 +
, http://dbpedia.org/resource/Small_o_notation +
, http://dbpedia.org/resource/Circuit_satisfiability +
, http://dbpedia.org/resource/Davis%E2%80%93Putnam%E2%80%93Logemann%E2%80%93Loveland_algorithm +
, http://dbpedia.org/resource/Valiant-Vazirani_theorem +
, http://dbpedia.org/resource/P/poly +
, http://dbpedia.org/resource/2-SAT +
, http://dbpedia.org/resource/File:Schaefer%27s_3-SAT_to_1-in-3-SAT_reduction.gif +
, http://dbpedia.org/resource/Negation +
, http://dbpedia.org/resource/US_%28complexity%29 +
, http://dbpedia.org/resource/File:Boolean_satisfiability_vs_true_literal_counts.png +
, http://dbpedia.org/resource/File:Sat_reduced_to_Clique_from_Sipser.svg +
, http://dbpedia.org/resource/0-1_integer_programming +
, http://dbpedia.org/resource/SL_%28complexity%29 +
, http://dbpedia.org/resource/Microprocessor +
, http://dbpedia.org/resource/NP-complete +
, http://dbpedia.org/resource/Category:Satisfiability_problems +
, http://dbpedia.org/resource/Complexity_class +
, http://dbpedia.org/resource/Karp%27s_21_NP-complete_problems +
, http://dbpedia.org/resource/P-complete +
, http://dbpedia.org/resource/Formal_equivalence_checking +
, http://dbpedia.org/resource/Category:NP-complete_problems +
, http://dbpedia.org/resource/Karloff%E2%80%93Zwick_algorithm +
, http://dbpedia.org/resource/Local_search_%28constraint_satisfaction%29 +
, http://dbpedia.org/resource/Conflict-driven_clause_learning +
, http://dbpedia.org/resource/Conjunctive_normal_form +
, http://dbpedia.org/resource/Logic +
, http://dbpedia.org/resource/Schaefer%27s_dichotomy_theorem +
, http://dbpedia.org/resource/Equisatisfiable +
, http://dbpedia.org/resource/NP-hard +
, http://dbpedia.org/resource/Electronic_design_automation +
, http://dbpedia.org/resource/Category:Electronic_design_automation +
, http://dbpedia.org/resource/Gaussian_elimination +
, http://dbpedia.org/resource/Computer_science +
, http://dbpedia.org/resource/Routing_%28electronic_design_automation%29 +
, http://dbpedia.org/resource/Propositional_logic +
, http://dbpedia.org/resource/NL_%28complexity%29 +
, http://dbpedia.org/resource/Tseytin_transformation +
|
| http://dbpedia.org/property/wikiPageUsesTemplate
|
http://dbpedia.org/resource/Template:Logic +
, http://dbpedia.org/resource/Template:Refbegin +
, http://dbpedia.org/resource/Template:Refend +
, http://dbpedia.org/resource/Template:Additional_citations_needed +
, http://dbpedia.org/resource/Template:Refn +
, http://dbpedia.org/resource/Template:Cite_book +
, http://dbpedia.org/resource/Template:Color +
, http://dbpedia.org/resource/Template:Fontcolor +
, http://dbpedia.org/resource/Template:Commons_category +
, http://dbpedia.org/resource/Template:Short_description +
, http://dbpedia.org/resource/Template:Redirect +
, http://dbpedia.org/resource/Template:Citation_needed +
, http://dbpedia.org/resource/Template:Main +
, http://dbpedia.org/resource/Template:Math +
, http://dbpedia.org/resource/Template:Cite_journal +
, http://dbpedia.org/resource/Template:Tmath +
, http://dbpedia.org/resource/Template:Reflist +
, http://dbpedia.org/resource/Template:Mvar +
|
| http://purl.org/dc/terms/subject
|
http://dbpedia.org/resource/Category:Electronic_design_automation +
, http://dbpedia.org/resource/Category:NP-complete_problems +
, http://dbpedia.org/resource/Category:Boolean_algebra +
, http://dbpedia.org/resource/Category:Satisfiability_problems +
, http://dbpedia.org/resource/Category:Formal_methods +
, http://dbpedia.org/resource/Category:Logic_in_computer_science +
|
| http://purl.org/linguistics/gold/hypernym
|
http://dbpedia.org/resource/Problem +
|
| http://www.w3.org/ns/prov#wasDerivedFrom
|
http://en.wikipedia.org/wiki/Boolean_satisfiability_problem?oldid=1117934167&ns=0 +
|
| http://xmlns.com/foaf/0.1/depiction
|
http://commons.wikimedia.org/wiki/Special:FilePath/Sat_reduced_to_Clique_from_Sipser.svg +
, http://commons.wikimedia.org/wiki/Special:FilePath/Boolean_satisfiability_vs_true_literal_counts.png +
, http://commons.wikimedia.org/wiki/Special:FilePath/Schaefer%27s_3-SAT_to_1-in-3-SAT_reduction.gif +
|
| http://xmlns.com/foaf/0.1/isPrimaryTopicOf
|
http://en.wikipedia.org/wiki/Boolean_satisfiability_problem +
|
| owl:sameAs |
http://fr.dbpedia.org/resource/Probl%C3%A8me_SAT +
, https://global.dbpedia.org/id/51oKL +
, http://th.dbpedia.org/resource/%E0%B8%9B%E0%B8%B1%E0%B8%8D%E0%B8%AB%E0%B8%B2%E0%B8%84%E0%B8%A7%E0%B8%B2%E0%B8%A1%E0%B8%AA%E0%B8%AD%E0%B8%94%E0%B8%84%E0%B8%A5%E0%B9%89%E0%B8%AD%E0%B8%87%E0%B9%81%E0%B8%9A%E0%B8%9A%E0%B8%9A%E0%B8%B9%E0%B8%A5 +
, http://es.dbpedia.org/resource/Problema_de_satisfacibilidad_booleana +
, http://hu.dbpedia.org/resource/Logikai_kiel%C3%A9g%C3%ADt%C3%A9si_probl%C3%A9ma +
, http://it.dbpedia.org/resource/Soddisfacibilit%C3%A0_booleana +
, http://nl.dbpedia.org/resource/Vervulbaarheidsprobleem +
, http://yago-knowledge.org/resource/Boolean_satisfiability_problem +
, http://sh.dbpedia.org/resource/SAT_problem +
, http://www.wikidata.org/entity/Q875276 +
, http://ar.dbpedia.org/resource/%D9%85%D8%B3%D8%A3%D9%84%D8%A9_%D9%82%D8%A7%D8%A8%D9%84%D9%8A%D8%A9_%D8%A7%D9%84%D8%A5%D8%B1%D8%B6%D8%A7%D8%A1_%D8%A7%D9%84%D9%85%D9%86%D8%B7%D9%82%D9%8A%D8%A9 +
, http://de.dbpedia.org/resource/Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik +
, http://ca.dbpedia.org/resource/Problema_de_satisfacibilitat_booleana +
, http://ko.dbpedia.org/resource/%EC%B6%A9%EC%A1%B1_%EA%B0%80%EB%8A%A5%EC%84%B1_%EB%AC%B8%EC%A0%9C +
, http://zh.dbpedia.org/resource/%E5%B8%83%E5%B0%94%E5%8F%AF%E6%BB%A1%E8%B6%B3%E6%80%A7%E9%97%AE%E9%A2%98 +
, http://pt.dbpedia.org/resource/Problema_de_satisfatibilidade_booliana +
, http://ja.dbpedia.org/resource/%E5%85%85%E8%B6%B3%E5%8F%AF%E8%83%BD%E6%80%A7%E5%95%8F%E9%A1%8C +
, http://ru.dbpedia.org/resource/%D0%97%D0%B0%D0%B4%D0%B0%D1%87%D0%B0_%D0%B2%D1%8B%D0%BF%D0%BE%D0%BB%D0%BD%D0%B8%D0%BC%D0%BE%D1%81%D1%82%D0%B8_%D0%B1%D1%83%D0%BB%D0%B5%D0%B2%D1%8B%D1%85_%D1%84%D0%BE%D1%80%D0%BC%D1%83%D0%BB +
, http://uk.dbpedia.org/resource/%D0%97%D0%B0%D0%B4%D0%B0%D1%87%D0%B0_%D0%B7%D0%B4%D1%96%D0%B9%D1%81%D0%BD%D0%B5%D0%BD%D0%BD%D0%BE%D1%81%D1%82%D1%96_%D0%B1%D1%83%D0%BB%D0%B5%D0%B2%D0%B8%D1%85_%D1%84%D0%BE%D1%80%D0%BC%D1%83%D0%BB +
, http://sr.dbpedia.org/resource/%D0%A1%D0%90%D0%A2_%D0%BF%D1%80%D0%BE%D0%B1%D0%BB%D0%B5%D0%BC +
, http://fa.dbpedia.org/resource/%D9%85%D8%B3%D8%A6%D9%84%D9%87_%D8%B5%D8%AF%D9%82%E2%80%8C%D9%BE%D8%B0%DB%8C%D8%B1%DB%8C_%D8%A8%D9%88%D9%84%DB%8C +
, http://he.dbpedia.org/resource/%D7%91%D7%A2%D7%99%D7%99%D7%AA_%D7%94%D7%A1%D7%A4%D7%99%D7%A7%D7%95%D7%AA +
, http://rdf.freebase.com/ns/m.01hmj +
, http://simple.dbpedia.org/resource/Boolean_satisfiability_problem +
, http://cs.dbpedia.org/resource/Probl%C3%A9m_splnitelnosti_booleovsk%C3%A9_formule +
, http://eo.dbpedia.org/resource/Bulea_plenumebloproblemo +
, http://pl.dbpedia.org/resource/Problem_spe%C5%82nialno%C5%9Bci +
, http://dbpedia.org/resource/Boolean_satisfiability_problem +
|
| rdf:type |
http://dbpedia.org/class/yago/Abstraction100002137 +
, http://dbpedia.org/class/yago/Know-how105616786 +
, http://dbpedia.org/class/yago/Method105660268 +
, http://dbpedia.org/class/yago/WikicatFormalMethods +
, http://dbpedia.org/class/yago/Attribute100024264 +
, http://dbpedia.org/class/yago/State100024720 +
, http://dbpedia.org/class/yago/Difficulty114408086 +
, http://dbpedia.org/ontology/Disease +
, http://dbpedia.org/class/yago/Cognition100023271 +
, http://dbpedia.org/class/yago/WikicatNP-hardProblems +
, http://dbpedia.org/class/yago/WikicatSatisfiabilityProblems +
, http://dbpedia.org/class/yago/Condition113920835 +
, http://dbpedia.org/class/yago/PsychologicalFeature100023100 +
, http://dbpedia.org/class/yago/Ability105616246 +
, http://dbpedia.org/class/yago/Problem114410605 +
, http://dbpedia.org/class/yago/WikicatNP-completeProblems +
|
| rdfs:comment |
Зада́ча здійсне́нності бу́левих фо́рмул (S … Зада́ча здійсне́нності бу́левих фо́рмул (SAT, від англ. satisfiability) — важлива для теорії обчислювальної складності алгоритмічна задача. Об'єктом задачі SAT є , що складається тільки з назв змінних, дужок і операцій (І) (АБО) і (НІ).Задача полягає в наступному: чи можна призначити усім змінним, що трапляються у формулі, значення хибність і істина так, щоб формула стала істинною. і істина так, щоб формула стала істинною.
, La soddisfacibilità booleana, o soddisfaci … 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).essa dalla formula è identicamente falsa).
, Das Erfüllbarkeitsproblem der Aussagenlogi … 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).en Constraint Satisfaction Problems (CSP).
, In logic and computer science, the Boolean … 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 Aes a = TRUE and b = FALSE, which make (a A
, مسألة قابلية الإرضاء المنطقية، في المنطق و … مسألة قابلية الإرضاء المنطقية، في المنطق وعلوم الحاسوب، (تسمى أحيانًا مسألة قابلية الإرضاء الافتراضية وتختصر إلى قابلية الإرضاء أو إس إيه تي أو بي-إس إيه تي) هي مسألة تحديد وجود ترجمة تفسيرية ترضي صيغة منطقية معينة. بمعنى آخر، تستعلم ما إذا كان يمكن استبدال متغيرات صيغة منطقية معينة باستمرار بالقيم TRUE (صح) أو FALSE (خطأ) بطريقة تكون نتيجة الصيغة TRUE. إذا طبقت هذه الحالة، تسمى الصيغة مرضية. من ناحية أخرى، في حالة عدم وجود تعيين كهذا، تكون الوظيفة المعبر عنها بواسطة الصيغة FALSE لجميع تعيينات المتغيرات المحتملة وتكون الصيغة غير مرضية. مثلًا، تعد الصيغة «a AND NOT b (إيه و نفي بي) مرضية لأنه يمكن إيجاد قيمتين a = TRUE و b = FALSE، تحققان الصيغة (a AND NOT b = TRUE). في المقابل، تعد الصيغة «a AND NOT a» غير مُرضية.قابل، تعد الصيغة «a AND NOT a» غير مُرضية.
, En teoria de complexitat computacional, el … 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.onar CERT i no es pot satisfer en cap cas.
, Problem spełnialności – zagadnienie rachun … 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ą.a więc złożoność obliczeniową wykładniczą.
, 충족 가능성 문제(充足可能性問題, satisfiability problem, SAT)는 어떠한 변수들로 이루어진 논리식이 주어졌을 때, 그 논리식이 참이 되는 변수값이 존재하는지를 찾는 문제이다. 만족성 문제, 만족도 문제, 만족 문제, 불린 충족 가능성 문제(boolean satisfiability problem)라고도 부른다.
, Problém splnitelnosti booleovské formule ( … 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).formule vyjadřuje protimluv, kontradikci).
, En informatique théorique, le problème SAT … 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.opositionnelles qui rend la formule vraie.
, 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.
, Зада́ча выполни́мости бу́левых фо́рмул (SA … Зада́ча выполни́мости бу́левых фо́рмул (SAT, ВЫП) — важная для теории вычислительной сложности алгоритмическая задача. Экземпляром задачи является булева формула, состоящая только из имён переменных, скобок и операций (И), (ИЛИ) и (HE).Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной. истина так, чтобы формула стала истинной.
, 充足可能性問題（じゅうそくかのうせいもんだい、satisfiability problem, SAT）は、一つの命題論理式が与えられたとき、それに含まれる変数の値を偽 (False) あるいは真 (True) にうまく定めることによって全体の値を'真'にできるか、という問題をいう。SATisfiabilityの頭3文字を取ってしばしば「SAT」と呼ばれる。
, Kontentigeblo estas la problemo decidi ĉu … 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.aj ĉiuj ties variabloj estas duum-valoraj.
, Na teoria da complexidade computacional, o … 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 évaliação da fórmula como verdadeira, ela é
, In de complexiteitstheorie verwijst het ve … 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. zodanig dat de gehele propositie waar is.
, 可滿足性（英語：Satisfiability）是用來解決給定的真值方程式，是否存在一组变量赋值，使問題为可满足。布尔可滿足性問題（Boolean satisfiability problem；SAT ）屬於決定性問題，也是第一个被证明屬於NP完全的问题。此問題在電腦科學上許多的領域皆相當重要，包括、演算法、人工智慧、等等。
|
| rdfs:label |
Задача выполнимости булевых формул
, Задача здійсненності булевих формул
, Problem spełnialności
, Problema de satisfacibilidad booleana
, 充足可能性問題
, 布尔可满足性问题
, Problema de satisfatibilidade booliana
, Problema de satisfacibilitat booleana
, Soddisfacibilità booleana
, Problém splnitelnosti booleovské formule
, مسألة قابلية الإرضاء المنطقية
, Vervulbaarheidsprobleem
, 충족 가능성 문제
, Erfüllbarkeitsproblem der Aussagenlogik
, Problème SAT
, Boolean satisfiability problem
, Bulea plenumebloproblemo
|
