@prefix dbpprop: .
@prefix dbpedia: .
dbpprop:redirect dbpedia:Boolean_satisfiability_problem .
@prefix rdf: .
@prefix ns3: .
dbpedia:Boolean_satisfiability_problem rdf:type ns3:NP-completeProblems ,
ns3:SatisfiabilityProblems ,
ns3:FormalMethods .
@prefix owl: .
dbpedia:Boolean_satisfiability_problem owl:sameAs .
@prefix foaf: .
@prefix ns6: .
dbpedia:Boolean_satisfiability_problem foaf:page ns6:Boolean_satisfiability_problem ;
dbpprop:reference ,
,
.
@prefix ns7: .
dbpedia:Boolean_satisfiability_problem dbpprop:reference ns7:Spear ,
,
,
,
,
,
,
ns7:HyperSAT ,
,
,
,
,
,
,
.
@prefix ns8: .
dbpedia:Boolean_satisfiability_problem dbpprop:reference ns8:fss ,
.
@prefix rdfs: .
dbpedia:Boolean_satisfiability_problem rdfs:label "\u0417\u0430\u0434\u0430\u0447\u0430 \u0432\u044B\u043F\u043E\u043B\u043D\u0438\u043C\u043E\u0441\u0442\u0438 \u0431\u0443\u043B\u0435\u0432\u044B\u0445 \u0444\u043E\u0440\u043C\u0443\u043B"@ru ,
"Probl\u00E8me SAT"@fr ,
"\u5145\u8DB3\u53EF\u80FD\u6027\u554F\u984C"@ja ,
"Boolean satisfiability problem"@en ,
"Problema de satisfacibilidad booleana"@es ,
"Soddisfacibilit\u00E0 booleana"@it ,
"Problem spe\u0142nialno\u015Bci"@pl ,
"\u5E03\u5C14\u53EF\u6EE1\u8DB3\u6027\u95EE\u9898"@zh ,
"Erf\u00FCllbarkeitsproblem der Aussagenlogik"@de ,
"\u0417\u0430\u0434\u0430\u0447\u0430 \u0437\u0434\u0456\u0439\u0441\u043D\u0435\u043D\u043D\u043E\u0441\u0442\u0456\u0456 \u0431\u0443\u043B\u044C\u043E\u0432\u0438\u0445 \u0444\u043E\u0440\u043C\u0443\u043B"@uk ;
dbpprop:abstract "\u0417\u0430\u0434\u0430\u0447\u0430 \u0432\u044B\u043F\u043E\u043B\u043D\u0438\u043C\u043E\u0441\u0442\u0438 \u0431\u0443\u043B\u0435\u0432\u044B\u0445 \u0444\u043E\u0440\u043C\u0443\u043B (SAT \u0438\u043B\u0438 \u0412\u042B\u041F) \u2014 \u0437\u0430\u0434\u0430\u0447\u0430 \u0440\u0430\u0441\u043F\u043E\u0437\u043D\u0430\u0432\u0430\u043D\u0438\u044F, \u0432\u0430\u0436\u043D\u0430\u044F \u0434\u043B\u044F \u0442\u0435\u043E\u0440\u0438\u0438 \u0432\u044B\u0447\u0438\u0441\u043B\u0438\u0442\u0435\u043B\u044C\u043D\u043E\u0439 \u0441\u043B\u043E\u0436\u043D\u043E\u0441\u0442\u0438. \u042D\u043A\u0437\u0435\u043C\u043F\u043B\u044F\u0440\u043E\u043C \u0437\u0430\u0434\u0430\u0447\u0438 SAT \u044F\u0432\u043B\u044F\u0435\u0442\u0441\u044F \u0431\u0443\u043B\u0435\u0432\u0430 \u0444\u043E\u0440\u043C\u0443\u043B\u0430, \u0441\u043E\u0441\u0442\u043E\u044F\u0449\u0430\u044F \u0442\u043E\u043B\u044C\u043A\u043E \u0438\u0437 \u0438\u043C\u0435\u043D \u043F\u0435\u0440\u0435\u043C\u0435\u043D\u043D\u044B\u0445, \u0441\u043A\u043E\u0431\u043E\u043A \u0438 \u043E\u043F\u0435\u0440\u0430\u0446\u0438\u0439 <math>\\wedge</math> (\u0418), <math>\\vee</math> (\u0418\u041B\u0418) \u0438 <math>\\neg</math> (HE). \u0417\u0430\u0434\u0430\u0447\u0430 \u0437\u0430\u043A\u043B\u044E\u0447\u0430\u0435\u0442\u0441\u044F \u0432 \u0441\u043B\u0435\u0434\u0443\u044E\u0449\u0435\u043C: \u043C\u043E\u0436\u043D\u043E \u043B\u0438 \u043D\u0430\u0437\u043D\u0430\u0447\u0438\u0442\u044C \u0432\u0441\u0435\u043C \u043F\u0435\u0440\u0435\u043C\u0435\u043D\u043D\u044B\u043C, \u0432\u0441\u0442\u0440\u0435\u0447\u0430\u044E\u0449\u0438\u043C\u0441\u044F \u0432 \u0444\u043E\u0440\u043C\u0443\u043B\u0435, \u0437\u043D\u0430\u0447\u0435\u043D\u0438\u044F \u041B\u041E\u0416\u042C \u0438 \u0418\u0421\u0422\u0418\u041D\u0410 \u0442\u0430\u043A, \u0447\u0442\u043E\u0431\u044B \u0444\u043E\u0440\u043C\u0443\u043B\u0430 \u0441\u0442\u0430\u043B\u0430 \u0438\u0441\u0442\u0438\u043D\u043D\u043E\u0439. \u0421\u043E\u0433\u043B\u0430\u0441\u043D\u043E \u0442\u0435\u043E\u0440\u0435\u043C\u0435 \u041A\u0443\u043A\u0430, \u0434\u043E\u043A\u0430\u0437\u0430\u043D\u043D\u043E\u0439 \u0421\u0442\u0438\u0432\u0435\u043D\u043E\u043C \u041A\u0443\u043A\u043E\u043C \u0432 1971-\u043C \u0433\u043E\u0434\u0443, \u0437\u0430\u0434\u0430\u0447\u0430 SAT NP-\u043F\u043E\u043B\u043D\u0430."@ru ,
"\u5145\u8DB3\u53EF\u80FD\u6027\u554F\u984C\uFF08\u3058\u3085\u3046\u305D\u304F\u304B\u306E\u3046\u305B\u3044\u3082\u3093\u3060\u3044\u3001satisfiability problem, SAT\uFF09\u306F\u3001\u4E00\u3064\u306E\u4E57\u6CD5\u6A19\u6E96\u5F62 (CNF) \u304C\u4E0E\u3048\u3089\u308C\u305F\u3068\u304D\u3001\u305D\u308C\u306B\u542B\u307E\u308C\u308B\u3059\u3079\u3066\u306E\u5909\u6570\u306E\u5024\u3092\u507D (False) \u3042\u308B\u3044\u306F\u771F (True) \u306B\u3046\u307E\u304F\u5B9A\u3081\u308B\u3053\u3068\u306B\u3088\u3063\u3066\u5168\u4F53\u306E\u5024\u3092'\u771F'\u306B\u3067\u304D\u308B\u304B\u3001\u3068\u3044\u3046\u554F\u984C\u3092\u3044\u3046\u3002SATisfability\u306E\u982D3\u6587\u5B57\u3092\u53D6\u3063\u3066\u3057\u3070\u3057\u3070\u300CSAT\u300D\u3068\u547C\u3070\u308C\u308B\u3002"@ja ,
"Das Erf\u00FCllbarkeitsproblem der Aussagenlogik (SAT, von engl. satisfiability) ist ein Entscheidungsproblem. Es fragt, ob eine aussagenlogische Formel erf\u00FCllbar ist. Anwendungen finden sich unter anderem in der Komplexit\u00E4tstheorie, Verifikation und im Entwurf von logischen Schaltungen. Insbesondere in der Komplexit\u00E4tstheorie wird mit SAT auch nur der Spezialfall von Formeln bezeichnet, die in konjunktiver Normalform vorliegen. Das Erf\u00FCllbarkeitsproblem der Aussagenlogik ist in exponentieller Zeit in der Anzahl der Variablen entscheidbar, zum Beispiel durch das Aufstellen einer Wahrheitstabelle. Ob es auch einen Algorithmus gibt, der SAT in polynomieller Zeit l\u00F6st, ist nicht bekannt. Die Forschung besch\u00E4ftigt sich mit der Entwicklung m\u00F6glichst effizienter Verfahren (sogenannter SAT-Solver). Bekannte SAT-Solver sind Bin\u00E4re Entscheidungsdiagramme, oder das Davis-Putnam-Verfahren. Manche Solver verwenden stochastische oder systematische Suchverfahren zur Entscheidung der Erf\u00FCllbarkeit. Das bekannteste und am meisten verbreitete Verfahren zur systematischen Suche ist (Stand 2008) das DPLL-Verfahren (Davis-Putnam-Logemann-Loveland), welches in den letzten Jahrzehnten mit Hilfe von Heuristiken und Lernverfahren stark verbessert wurde. SAT geh\u00F6rt zur Klasse <math>\\mathcal{NP}</math> der Probleme, die in polynomieller Zeit mit einer nichtdeterministischen Turingmaschine gel\u00F6st werden k\u00F6nnen. Die noch ungel\u00F6ste Frage, ob SAT auch mit einer deterministischen Turingmaschine (also mit einem herk\u00F6mmlichen Rechner) in polynomialer Zeit gel\u00F6st werden kann, kann man formulieren als: Gilt <math>\\mbox{SAT} \\in \\mathcal{P}</math>? Das Erf\u00FCllbarkeitsproblem der Aussagenlogik ist NP-vollst\u00E4ndig. Das besagt, dass jedes Problem aus <math>\\mathcal{NP}</math> in polynomieller Zeit auf SAT zur\u00FCckgef\u00FChrt werden kann. Anfang der 1970er Jahre zeigten Stephen A. Cook und Leonid Levin unabh\u00E4ngig voneinander diese Eigenschaft, bekannt als der Satz von Cook. Cook zeigte hierf\u00FCr einen Algorithmus auf, mit dem die Berechnungsschritte einer nicht-deterministischen Turingmaschine in Aussagenlogik formuliert und damit auf SAT reduziert werden k\u00F6nnen. Richard Karp zeigte 1972 die NP-Vollst\u00E4ndigkeit weiterer Probleme. Er pr\u00E4gte damit das heutige Verst\u00E4ndnis von NP-Vollst\u00E4ndigkeit. Falls also <math>\\mbox{SAT} \\in \\mathcal{P}</math> gilt, dann ist jedes Problem aus <math>\\mathcal{NP}</math> auch in <math>\\mathcal{P}</math>, das hei\u00DFt, dann gilt <math>\\mathcal{P} = \\mathcal{NP}</math>. Auch die umgekehrte Richtung der Implikation gilt. Das P-NP-Problem \"gilt <math>\\mathcal{P} = \\mathcal{NP}</math> oder nicht?\" ist eine der gro\u00DFen ungel\u00F6sten Fragen der Komplexit\u00E4tstheorie. Ist ein Problem NP-vollst\u00E4ndig, so darf man annehmen, dass die Suche nach einem Polynomialzeit-Algorithmus daf\u00FCr aussichtslos ist."@de ,
"\u53EF\u6EFF\u8DB3\u6027\uFF08\u82F1\u8A9E\uFF1ASatisfiability\uFF09\u662F\u7528\u4F86\u89E3\u6C7A\u7D66\u5B9A\u7684\u5E03\u6797\u65B9\u7A0B\u5F0F\uFF0C\u662F\u5426\u5B58\u5728\u4E00\u7EC4\u53D8\u91CF\u8D4B\u503C\uFF0C\u4F7F\u554F\u984C\u4E3A\u53EF\u6EE1\u8DB3\u3002\u5E03\u6797\u53EF\u6EFF\u8DB3\u6027\u554F\u984C\uFF08Boolean satisfiability problem\uFF1BSAT)\uFF09\u5C6C\u65BC\u6C7A\u5B9A\u6027\u554F\u984C\uFF0C\u662F\u7B2C\u4E00\u4E2A\u88AB\u8BC1\u660ENP\u5B8C\u5168\u95EE\u9898\u3002\u70BA\u96FB\u8166\u79D1\u5B78\u4E0A\u8A31\u591A\u9818\u57DF\u7684\u91CD\u8981\u554F\u984C\uFF0C\u5305\u62EC\u96FB\u8166\u79D1\u5B78\u57FA\u790E\u7406\u8AD6\u3001\u6F14\u7B97\u6CD5\u3001\u4EBA\u5DE5\u667A\u6167\u3001\u786C\u9AD4\u8A2D\u8A08\u7B49\u7B49\u3002"@zh ,
"On nomme probl\u00E8me SAT un probl\u00E8me de d\u00E9cision visant \u00E0 savoir s'il existe une solution \u00E0 une s\u00E9rie d'\u00E9quations logiques donn\u00E9es. En termes plus pr\u00E9cis : une valuation sur un ensemble de variables propositionnelles telle qu'une formule propositionnelle donn\u00E9e soit alors logiquement vraie. Ce probl\u00E8me est tr\u00E8s important en th\u00E9orie de la complexit\u00E9 et a de nombreuses applications en planification classique, model checking, diagnostic, et jusqu'au configurateur d'un simple PC ou de son syst\u00E8me d'exploitation."@fr ,
"\u0417\u0430\u0434\u0430\u0301\u0447\u0430 \u0437\u0434\u0456\u0439\u0441\u043D\u0438\u0301\u043C\u043E\u0441\u0442\u0456 \u0431\u0443\u0301\u043B\u044C\u043E\u0432\u0438\u0445 \u0444\u043E\u0301\u0440\u043C\u0443\u043B (SAT) \u2014 \u0437\u0430\u0434\u0430\u0447\u0430 \u0440\u043E\u0437\u043F\u0456\u0437\u043D\u0430\u0432\u0430\u043D\u043D\u044F \u043E\u0431\u0440\u0430\u0437\u0456\u0432, \u0432\u0430\u0436\u043B\u0438\u0432\u0430 \u0434\u043B\u044F \u0442\u0435\u043E\u0440\u0456\u0457 \u043E\u0431\u0447\u0438\u0441\u043B\u044E\u0432\u0430\u043B\u044C\u043D\u043E\u0457 \u0441\u043A\u043B\u0430\u0434\u043D\u043E\u0441\u0442\u0456. \u041E\u0431'\u0454\u043A\u0442\u043E\u043C \u0437\u0430\u0434\u0430\u0447\u0438 SAT \u0454 \u0431\u0443\u043B\u0435\u0432\u0430 \u0444\u043E\u0440\u043C\u0443\u043B\u0430, \u0449\u043E \u0441\u043A\u043B\u0430\u0434\u0430\u0454\u0442\u044C\u0441\u044F \u0442\u0456\u043B\u044C\u043A\u0438 \u0437 \u0456\u043C\u0435\u043D \u0437\u043C\u0456\u043D\u043D\u0438\u0445, \u0434\u0443\u0436\u043E\u043A \u0456 \u043E\u043F\u0435\u0440\u0430\u0446\u0456\u0439 <math>\\wedge</math> (\u0406), <math>\\vee</math> (\u0410\u0411\u041E) \u0456 <math>\\neg</math> (H\u0406). \u0417\u0430\u0434\u0430\u0447\u0430 \u043F\u043E\u043B\u044F\u0433\u0430\u0454 \u0432 \u043D\u0430\u0441\u0442\u0443\u043F\u043D\u043E\u043C\u0443: \u0447\u0438 \u043C\u043E\u0436\u043D\u0430 \u043F\u0440\u0438\u0437\u043D\u0430\u0447\u0438\u0442\u0438 \u0432\u0441\u0456\u043C \u0437\u043C\u0456\u043D\u043D\u0438\u043C, \u0449\u043E \u0437\u0443\u0441\u0442\u0440\u0456\u0447\u0430\u044E\u0442\u044C\u0441\u044F \u0443 \u0444\u043E\u0440\u043C\u0443\u043B\u0456, \u0437\u043D\u0430\u0447\u0435\u043D\u043D\u044F \u041D\u0415\u0412\u0406\u0420\u041D\u041E \u0456 \u0412\u0406\u0420\u041D\u041E \u0442\u0430\u043A, \u0449\u043E\u0431 \u0444\u043E\u0440\u043C\u0443\u043B\u0430 \u0441\u0442\u0430\u043B\u0430 \u0456\u0441\u0442\u0438\u043D\u043D\u043E\u044E. \u0417\u0433\u0456\u0434\u043D\u043E \u0442\u0435\u043E\u0440\u0435\u043C\u0456 \u041A\u0443\u043A\u0430, \u0434\u043E\u0432\u0435\u0434\u0435\u043D\u043E\u044E \u0421\u0442\u0438\u0432\u0435\u043D\u043E\u043C \u041A\u0443\u043A\u043E\u043C \u0432 1971-\u043C\u0443 \u0440\u043E\u0446\u0456, \u043F\u0440\u043E\u0431\u043B\u0435\u043C\u0430 SAT \u0454 NP-\u043F\u043E\u0432\u043D\u043E\u044E."@uk ,
"Quello della Soddisfacibilit\u00E0 \u00E8 il problema di determinare se le variabili di una data formula booleana possano essere assegnate in modo che la formula sia valutata \"TRUE\". Ugualmente importante \u00E8 individuare che tale assegnamento non esiste, arrivando a concludere che la funzione espressa dalla formula \u00E8 identicamente \"FALSE\" per tutti i possibili assegnamenti delle sue variabili. In quest'ultimo caso si dice che la funzione \u00E8 insoddisfacibile; altrimenti, soddisfacibile. Per enfatizzare la natura binaria di tale problema, ad esso ci si riferisce spesso come al problema di soddisfacibilit\u00E0 booleana o soddisfacibilit\u00E0 proposizionale. Il diminuitivo \"SAT\" \u00E8 una sigla comunemente utilizzata per denotare tale problema, dove si intende implicitamente che la funzione e le sue variabili sono tutte valutate in modo binario."@it ,
"Problem spe\u0142nialno\u015Bci to pytanie rachunku zda\u0144 - czy dla danej formu\u0142y logicznej istnieje takie podstawienie (warto\u015Bciowanie) zmiennych zdaniowych, \u017Ceby formu\u0142a by\u0142a prawdziwa. Jest r\u00F3wnowa\u017Cne negacji pytania czy \"negacja tej formu\u0142y jest tautologi\u0105\". Problem spe\u0142nialno\u015Bci jest rozstrzygalny - mo\u017Cna wypr\u00F3bowa\u0107 wszystkich podstawie\u0144 kt\u00F3rych jest <math>2^N</math>, gdzie <math>N</math> to ilo\u015B\u0107 zmiennych w formule. Metoda ta ma wi\u0119c z\u0142o\u017Cono\u015B\u0107 wyk\u0142adnicz\u0105. Szczeg\u00F3lnie ciekawy jest problem spe\u0142nialno\u015Bci formu\u0142 w koniunkcyjnej postaci normalnej (ang. CNF - conjunctional normal form), kt\u00F3rych klauzule maj\u0105 nie wi\u0119cej ni\u017C k litera\u0142\u00F3w (k-SAT). Litera\u0142em nazywamy zmienn\u0105 lub zmienn\u0105 zanegowan\u0105, klauzul\u0105 nazywamy alternatyw\u0119 litera\u0142\u00F3w, natomiast formu\u0142a to koniunkcja klauzul. 1-SAT i 2-SAT maj\u0105 rozwi\u0105zania w P, czyli w deterministycznym czasie wielomianowym, natomiast ju\u017C 3-SAT jest NP-zupe\u0142ny, czyli takim, \u017Ce ka\u017Cdy problem z klasy NP jest do niego redukowalny przy pomocy redukcji w czasie wielomianowym."@pl ,
"Satisfiability is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE. Equally important is to determine whether no such assignments exist, which would imply that the function expressed by the formula is identically FALSE for all possible variable assignments. In this latter case, we would say that the function is unsatisfiable; otherwise it is satisfiable. To emphasize the binary nature of this problem, it is frequently referred to as Boolean or propositional satisfiability. The shorthand \"SAT\" is also commonly used to denote it, with the implicit understanding that the function and its variables are all binary-valued."@en ,
"En teor\u00EDa de la complejidad computacional, el Problema de satisfacibilidad booleana (SAT) fue el primer problema identificado como perteneciente a la clase de complejidad NP-completo. Se trata de un problema donde interesa saber si una expresi\u00F3n booleana con variables y sin cuantificadores tiene asociada una asignaci\u00F3n de valores para sus variables que hace que la expresi\u00F3n sea verdadera. Por ejemplo, una instancia de SAT ser\u00EDa el saber si existen valores para <math>x_1,\\, x_2, \\, x_3, \\, x_4</math> tales que la expresi\u00F3n: <math> (x_1 \\or \\neg x_3 \\or x_4) \\and (\\neg x_2 \\or x_3 \\or \\neg x_4)</math> es cierta. El SAT es el primer problema NP-completo conocido, y fue demostrado por Stephen Cook en 1971. Hasta entonces, el concepto de un problema NP-completo, no estaba definido. El SAT problema sigue siendo NP-completo, incluso si todas las f\u00F3rmulas est\u00E1n en forma normal conjuntiva (FNC) con 3 variables por cl\u00E1usula (3SAT-FNC) creando el problema (3SAT), o aun inclusive, en el caso en que solo se permita un solo valor verdadero en cada clusula (3SAT en 1). El problema sigue perteneciendo a la clase de complejidad NP-completo aunque se restrinja el n\u00FAmero de literales por cla\u00FAsula a un m\u00E1ximo de 3. En este caso se conoce como 3 SAT. Cuando el n\u00FAmero m\u00E1ximo de literales por cl\u00E1usula es dos, el problema tiene complejidad polin\u00F3mica y se conoce como problema 2 SAT. El Teorema de Cook demuestra que el problema de la satisfatibilidade booleana es NP-completo, y de hecho, este fue el primer problema de decisi\u00F3n que se demostr\u00F3 ser NP-completos. Sin embargo, m\u00E1s all\u00E1 de este teorema, algoritmos eficientes y resistentes al cambio de tama\u00F1o del problema para SAT se han desarrollado desde la \u00FAltima d\u00E9cada y han contribuido con poderosos avances en nuestra capacidad para resolver el problema de satisfactibilidad autom\u00E1ticamente. La 3-satisfactibilidad es un caso especial de -satisfactibilidad (-SAT), o simplemente satisfactibilidad (SAT), en la que cada cl\u00E1usula contiene exactamente = 3 literales. Fue uno de 21 problemas NP-completos de Karp. Partiendo de SAT (el caso general) se reduce a 3-SAT y SAT 3 -en 1 y se puede demostrar que son NP-completos, entonces podemos usarlos para demostrar tambi\u00E9n otros problemas NP-completos. Esto se hace mostrando c\u00F3mo una soluci\u00F3n a otro problema podr\u00EDa ser utilizado para resolver 3-SAT Un ejemplo de este tipo de reduccion es el problema del Clique. Por lo general, es m\u00E1s f\u00E1cil de utilizar reducci\u00F3n de 3-SAT que con duando se est\u00E1 tratando de probar que algun otro porblema es NP-completo. El SAT 3-puede ser m\u00E1s limitado a la 3SAT Uno-en-tres, cuando lo que pedimos sea s\u00F3lo una de las variables verdadera en cada cl\u00E1usula, en vez de por lo menos una. 3SAT Uno-en-tres sigue siendo NP-completo. Extensiones de SAT Una extensi\u00F3n significativa a la popularidad que gan\u00F3 desde 2003 es el problema de las teor\u00EDas satisfactibilidad m\u00F3dulo, que permite enriquecer las f\u00F3rmulas en la FNC con lineales, vectores, la restricci\u00F3n de que todas las variables sean distintas, y no interpretar funciones, etc. Estas extensiones son t\u00EDpicamente NP-completas, pero resultan bastante eficaces para la resoluci\u00F3n que son capaces de hacer frente a muchos tipos de restricciones de g\u00E9nero. El problema parece ser m\u00E1s dif\u00EDcil satisfactibilidad (PSPACE-completo) si permitimos que los cuantificadores \"para todos\" y \"existencial\", que enlace las variables booleanas. Si se utiliza s\u00F3lo cuantificadores Este sigue siendo el problema SAT Si permitimos que s\u00F3lo los cuantificadores Se convierte en el problema de la tautolog\u00EDa: Co-NP-completo. Si dejamos que ellos, el problema se llama el problema de la f\u00F3rmula booleana cuantificados (QBF), que puede se ha demostrado PSPACE completa. Se cree ampliamente que los problemas son PSPACE completa-es son m\u00E1s dif\u00EDciles que cualquier problema en NP, aunque esto a\u00FAn no ha sido demostrada. . El problema de la m\u00E1xima satisfactibilidad, una generalizaci\u00F3n de SAT, para pedir el n\u00FAmero m\u00E1ximo de cl\u00E1usulas que pueden ser satisfechas por ninguna asignaci\u00F3n. Este problema tiene aproximaci\u00F3n de con algoritmos eficientes, sino que es NP-dif\u00EDcil de resolver con precisi\u00F3n. Peor a\u00FAn, el problema es APX-completo, lo que significa que no hay ning\u00FAn sistema de aproximaci\u00F3n polinomial de tiempo a este problema a menos que P = NP. Hay diversas clases de algoritmos de alto rendimiento para la soluci\u00F3n de los casos de SAT en la pr\u00E1ctica: las variantes modernas de el Algoritmo DPLL, como el algoritmo de paja y los algoritmos estoc\u00E1sticos de b\u00FAsqueda local, como WalkSAT. Una resoluci\u00F3n del tipo SAT Algoritmo DPLL emplea un procedimiento sistem\u00E1tico de rastreo para buscar a explorar el espacio (del tama\u00F1o exponencial) los valores de las variables que se ajusten. El procedimiento b\u00E1sico de este sistema de b\u00FAsqueda fue innovador en dos art\u00EDculos a principios de los a\u00F1os 60 y es, hoy en d\u00EDa, normalmente se conoce como el algoritmo de Davis-Putnam-Loveland-Logemann Algoritmo DPLL. El solucionador SAT moderno (desarrollado en los \u00FAltimos diez a\u00F1os), mejora el algoritmo de base para encontrar el tipo de Algoritmo DPLL. eficiente con el an\u00E1lisis de conflictos, la cl\u00E1usula de aprendizaje, no cronol\u00F3gico de rastreo (alias backjumping) y la propagaci\u00F3n de la unidad \" vieron dos literales \"(Dos vistos literales), brazo ajustable, y reinicios aleatorios. Es emp\u00EDricamente que tales \"a\u00F1adidos\" a la b\u00FAsqueda sistem\u00E1tica de base son esenciales para resolver el problema de casos SAT extensos que se plantean en la automatizaci\u00F3n de dise\u00F1o electr\u00F3nico. Los modernos solucionadores SAT tambi\u00E9n est\u00E1n causando un impacto significativo en los \u00E1mbitos de la verificaci\u00F3n de software, la resoluci\u00F3n de las limitaciones en la inteligencia artificial, y la investigaci\u00F3n operativa, entre otros. Algunos salocucionadores potente disponibles entan en el dominio p\u00FAblico, y son muy f\u00E1ciles de usar. En particular, el MINISAT, que gan\u00F3 la competencia de la SAT de 2005, s\u00F3lo alrededor de 600 l\u00EDneas de c\u00F3digo. Algoritmos Gen\u00E9ticos y otros m\u00E9todos estoc\u00E1sticos de b\u00FAsqueda local para el uso general tambi\u00E9n se utilizan para resolver problemas SAT, especialmente cuando no hay o s\u00F3lo un conocimiento limitado de la estructura espec\u00EDfica de los casos del problema a ser resuelto. Ciertos tipos de casos al azar satisfat\u00EDveis largo de la SAT se puede resolver por la propagaci\u00F3n de la vio literales. En particular en el dise\u00F1o y verificaci\u00F3n de hardware, la l\u00F3gica satisfactibilidad y otras propiedades de una f\u00F3rmula proposicional a veces se decidi\u00F3 sobre la base de una representaci\u00F3n de la f\u00F3rmula como un diagrama de decisi\u00F3n binario (BDD). La satisfactibilidad proposicional tiene varias generalizaciones, incluyendo satisfactibilidad al problema de la f\u00F3rmula booleana cuantificados para la l\u00F3gica cl\u00E1sica de primer y segundo orden (LCPO y LCSO, respectivamente), a los problemas de la satisfacci\u00F3n de las limitaciones para la programaci\u00F3n de enteros 0 -- 1, y el problema de la satisfactibilidad m\u00E1ximo. Muchos otros problemas de la decisi\u00F3n, como los problemas de coloraci\u00F3n de grafos, problemas de planificaci\u00F3n y programaci\u00F3n de problemas, puede ser codificado en SAT"@es ;
rdfs:comment "Problem spe\u0142nialno\u015Bci to pytanie rachunku zda\u0144 - czy dla danej formu\u0142y logicznej istnieje takie podstawienie (warto\u015Bciowanie) zmiennych zdaniowych, \u017Ceby formu\u0142a by\u0142a prawdziwa. Jest r\u00F3wnowa\u017Cne negacji pytania czy \"negacja tej formu\u0142y jest tautologi\u0105\". Problem spe\u0142nialno\u015Bci jest rozstrzygalny - mo\u017Cna wypr\u00F3bowa\u0107 wszystkich podstawie\u0144 kt\u00F3rych jest <math>2^N</math>, gdzie <math>N</math> to ilo\u015B\u0107 zmiennych w formule."@pl ,
"Satisfiability is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE. Equally important is to determine whether no such assignments exist, which would imply that the function expressed by the formula is identically FALSE for all possible variable assignments. In this latter case, we would say that the function is unsatisfiable; otherwise it is satisfiable."@en ,
"\u53EF\u6EFF\u8DB3\u6027\uFF08\u82F1\u8A9E\uFF1ASatisfiability\uFF09\u662F\u7528\u4F86\u89E3\u6C7A\u7D66\u5B9A\u7684\u5E03\u6797\u65B9\u7A0B\u5F0F\uFF0C\u662F\u5426\u5B58\u5728\u4E00\u7EC4\u53D8\u91CF\u8D4B\u503C\uFF0C\u4F7F\u554F\u984C\u4E3A\u53EF\u6EE1\u8DB3\u3002\u5E03\u6797\u53EF\u6EFF\u8DB3\u6027\u554F\u984C\uFF08Boolean satisfiability problem\uFF1BSAT)\uFF09\u5C6C\u65BC\u6C7A\u5B9A\u6027\u554F\u984C\uFF0C\u662F\u7B2C\u4E00\u4E2A\u88AB\u8BC1\u660ENP\u5B8C\u5168\u95EE\u9898\u3002\u70BA\u96FB\u8166\u79D1\u5B78\u4E0A\u8A31\u591A\u9818\u57DF\u7684\u91CD\u8981\u554F\u984C\uFF0C\u5305\u62EC\u96FB\u8166\u79D1\u5B78\u57FA\u790E\u7406\u8AD6\u3001\u6F14\u7B97\u6CD5\u3001\u4EBA\u5DE5\u667A\u6167\u3001\u786C\u9AD4\u8A2D\u8A08\u7B49\u7B49\u3002"@zh ,
"Das Erf\u00FCllbarkeitsproblem der Aussagenlogik (SAT, von engl. satisfiability) ist ein Entscheidungsproblem. Es fragt, ob eine aussagenlogische Formel erf\u00FCllbar ist. Anwendungen finden sich unter anderem in der Komplexit\u00E4tstheorie, Verifikation und im Entwurf von logischen Schaltungen. Insbesondere in der Komplexit\u00E4tstheorie wird mit SAT auch nur der Spezialfall von Formeln bezeichnet, die in konjunktiver Normalform vorliegen."@de ,
"\u0417\u0430\u0434\u0430\u0301\u0447\u0430 \u0437\u0434\u0456\u0439\u0441\u043D\u0438\u0301\u043C\u043E\u0441\u0442\u0456 \u0431\u0443\u0301\u043B\u044C\u043E\u0432\u0438\u0445 \u0444\u043E\u0301\u0440\u043C\u0443\u043B (SAT) \u2014 \u0437\u0430\u0434\u0430\u0447\u0430 \u0440\u043E\u0437\u043F\u0456\u0437\u043D\u0430\u0432\u0430\u043D\u043D\u044F \u043E\u0431\u0440\u0430\u0437\u0456\u0432, \u0432\u0430\u0436\u043B\u0438\u0432\u0430 \u0434\u043B\u044F \u0442\u0435\u043E\u0440\u0456\u0457 \u043E\u0431\u0447\u0438\u0441\u043B\u044E\u0432\u0430\u043B\u044C\u043D\u043E\u0457 \u0441\u043A\u043B\u0430\u0434\u043D\u043E\u0441\u0442\u0456."@uk ,
"\u5145\u8DB3\u53EF\u80FD\u6027\u554F\u984C\uFF08\u3058\u3085\u3046\u305D\u304F\u304B\u306E\u3046\u305B\u3044\u3082\u3093\u3060\u3044\u3001satisfiability problem, SAT\uFF09\u306F\u3001\u4E00\u3064\u306E\u4E57\u6CD5\u6A19\u6E96\u5F62 (CNF) \u304C\u4E0E\u3048\u3089\u308C\u305F\u3068\u304D\u3001\u305D\u308C\u306B\u542B\u307E\u308C\u308B\u3059\u3079\u3066\u306E\u5909\u6570\u306E\u5024\u3092\u507D (False) \u3042\u308B\u3044\u306F\u771F (True) \u306B\u3046\u307E\u304F\u5B9A\u3081\u308B\u3053\u3068\u306B\u3088\u3063\u3066\u5168\u4F53\u306E\u5024\u3092'\u771F'\u306B\u3067\u304D\u308B\u304B\u3001\u3068\u3044\u3046\u554F\u984C\u3092\u3044\u3046\u3002SATisfability\u306E\u982D3\u6587\u5B57\u3092\u53D6\u3063\u3066\u3057\u3070\u3057\u3070\u300CSAT\u300D\u3068\u547C\u3070\u308C\u308B\u3002"@ja ,
"On nomme probl\u00E8me SAT un probl\u00E8me de d\u00E9cision visant \u00E0 savoir s'il existe une solution \u00E0 une s\u00E9rie d'\u00E9quations logiques donn\u00E9es. En termes plus pr\u00E9cis : une valuation sur un ensemble de variables propositionnelles telle qu'une formule propositionnelle donn\u00E9e soit alors logiquement vraie."@fr ,
"En teor\u00EDa de la complejidad computacional, el Problema de satisfacibilidad booleana (SAT) fue el primer problema identificado como perteneciente a la clase de complejidad NP-completo. Se trata de un problema donde interesa saber si una expresi\u00F3n booleana con variables y sin cuantificadores tiene asociada una asignaci\u00F3n de valores para sus variables que hace que la expresi\u00F3n sea verdadera."@es ,
"Quello della Soddisfacibilit\u00E0 \u00E8 il problema di determinare se le variabili di una data formula booleana possano essere assegnate in modo che la formula sia valutata \"TRUE\". Ugualmente importante \u00E8 individuare che tale assegnamento non esiste, arrivando a concludere che la funzione espressa dalla formula \u00E8 identicamente \"FALSE\" per tutti i possibili assegnamenti delle sue variabili. In quest'ultimo caso si dice che la funzione \u00E8 insoddisfacibile; altrimenti, soddisfacibile."@it ,
"\u0417\u0430\u0434\u0430\u0447\u0430 \u0432\u044B\u043F\u043E\u043B\u043D\u0438\u043C\u043E\u0441\u0442\u0438 \u0431\u0443\u043B\u0435\u0432\u044B\u0445 \u0444\u043E\u0440\u043C\u0443\u043B (SAT \u0438\u043B\u0438 \u0412\u042B\u041F) \u2014 \u0437\u0430\u0434\u0430\u0447\u0430 \u0440\u0430\u0441\u043F\u043E\u0437\u043D\u0430\u0432\u0430\u043D\u0438\u044F, \u0432\u0430\u0436\u043D\u0430\u044F \u0434\u043B\u044F \u0442\u0435\u043E\u0440\u0438\u0438 \u0432\u044B\u0447\u0438\u0441\u043B\u0438\u0442\u0435\u043B\u044C\u043D\u043E\u0439 \u0441\u043B\u043E\u0436\u043D\u043E\u0441\u0442\u0438."@ru .
@prefix skos: .
@prefix ns11: .
dbpedia:Boolean_satisfiability_problem skos:subject ns11:Formal_methods ,
ns11:Satisfiability_problems ,
ns11:Logic_in_computer_science ,
ns11:NP-complete_problems ,
ns11:Electronic_design_automation ,
ns11:Boolean_algebra .
@prefix ns12: .
dbpedia:Boolean_satisfiability_problem dbpprop:relatedInstance ns12:doi-inline10 ,
ns12:doi-inline11 ,
ns12:doi-inline6 ,
ns12:doi-inline7 ,
ns12:doi-inline8 ,
ns12:doi-inline9 ,
ns12:doi-inline2 ,
ns12:doi-inline3 ,
ns12:doi-inline4 ,
ns12:doi-inline5 ,
ns12:doi-inline1 .
@prefix ns13: .
dbpedia:Boolean_satisfiability_problem dbpprop:hasPhotoCollection ns13:Boolean_satisfiability_problem .
dbpprop:redirect dbpedia:Boolean_satisfiability_problem ,
dbpedia:Boolean_satisfiability_problem .
dbpedia:Boolean dbpprop:disambiguates dbpedia:Boolean_satisfiability_problem .
dbpedia:Boolean_Satisfiability dbpprop:redirect dbpedia:Boolean_satisfiability_problem .
dbpedia:Boolean_satisfiability dbpprop:redirect dbpedia:Boolean_satisfiability_problem .
dbpedia:Counted_Boolean_Satisfiability_Problem dbpprop:redirect dbpedia:Boolean_satisfiability_problem .
dbpedia:K-cnf-sat dbpprop:redirect dbpedia:Boolean_satisfiability_problem .
dbpedia:Satisfiability_Problem dbpprop:redirect dbpedia:Boolean_satisfiability_problem .
dbpedia:Satisfiability_problem dbpprop:redirect dbpedia:Boolean_satisfiability_problem .
dbpedia:K-SAT dbpprop:redirect dbpedia:Boolean_satisfiability_problem .
dbpedia:Propositional_satisfiability dbpprop:redirect dbpedia:Boolean_satisfiability_problem .
dbpprop:redirect dbpedia:Boolean_satisfiability_problem .
dbpedia:CNFSAT dbpprop:redirect dbpedia:Boolean_satisfiability_problem .
dbpedia:Satisfiability_of_boolean_expressions dbpprop:redirect dbpedia:Boolean_satisfiability_problem .
@prefix yago: .
yago:Boolean_satisfiability_problem owl:sameAs dbpedia:Boolean_satisfiability_problem .