This HTML5 document contains 522 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dbpedia-dehttp://de.dbpedia.org/resource/
xsdhhttp://www.w3.org/2001/XMLSchema#
n11https://ghostarchive.org/archive/20221009/http:/eprints.soton.ac.uk/265003/1/
yagohttp://dbpedia.org/class/yago/
n58https://eprints.soton.ac.uk/265003/1/
dbohttp://dbpedia.org/ontology/
n52http://dbpedia.org/resource/P/
dbpedia-kohttp://ko.dbpedia.org/resource/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n33http://
n44https://web.archive.org/web/20070208034716/http:/www.sigda.org/newsletter/
dbpedia-simplehttp://simple.dbpedia.org/resource/
n19http://www.cril.univ-artois.fr/~roussel/satgame/
n13https://web.archive.org/web/20070708233347/http:/www.sigda.org/newsletter/2006/
wikidatahttp://www.wikidata.org/entity/
owlhttp://www.w3.org/2002/07/owl#
n36https://web.archive.org/web/20060219180520/http:/jsat.ewi.tudelft.nl/
dbpedia-ithttp://it.dbpedia.org/resource/
n34https://global.dbpedia.org/id/
goldhttp://purl.org/linguistics/gold/
n31http://dbpedia.org/resource/Max/min_CSP/
dbpedia-thhttp://th.dbpedia.org/resource/
dbpedia-frhttp://fr.dbpedia.org/resource/
n10http://dbpedia.org/resource/File:
n26http://commons.wikimedia.org/wiki/Special:FilePath/
dbrhttp://dbpedia.org/resource/
n54http://www.satcompetition.org/
dbpedia-huhttp://hu.dbpedia.org/resource/
dbpedia-cahttp://ca.dbpedia.org/resource/
dbpedia-eshttp://es.dbpedia.org/resource/
dbpedia-pthttp://pt.dbpedia.org/resource/
n55http://www.satisfiability.org/
dbpedia-ruhttp://ru.dbpedia.org/resource/
dbpedia-shhttp://sh.dbpedia.org/resource/
dbpedia-nlhttp://nl.dbpedia.org/resource/
provhttp://www.w3.org/ns/prov#
freebasehttp://rdf.freebase.com/ns/
yago-reshttp://yago-knowledge.org/resource/
dbpedia-jahttp://ja.dbpedia.org/resource/
dbpedia-arhttp://ar.dbpedia.org/resource/
dbphttp://dbpedia.org/property/
dbpedia-ukhttp://uk.dbpedia.org/resource/
dbpedia-fahttp://fa.dbpedia.org/resource/
dbchttp://dbpedia.org/resource/Category:
dbthttp://dbpedia.org/resource/Template:
rdfshttp://www.w3.org/2000/01/rdf-schema#
n14http://eprints.soton.ac.uk/265003/1/
dcthttp://purl.org/dc/terms/
wikipedia-enhttp://en.wikipedia.org/wiki/
dbpedia-srhttp://sr.dbpedia.org/resource/
n49http://www.domagoj-babic.com/uploads/Pubs/TCOM06/
foafhttp://xmlns.com/foaf/0.1/
dbpedia-cshttp://cs.dbpedia.org/resource/
dbpedia-eohttp://eo.dbpedia.org/resource/
dbpedia-zhhttp://zh.dbpedia.org/resource/
n48http://www.eecs.umich.edu/
n42http://www.cc.pol.una.py/lcca/publicaciones/optimizacion/2007/
dbpedia-plhttp://pl.dbpedia.org/resource/
n41http://www.maxsat.udl.cat/
dbpedia-hehttp://he.dbpedia.org/resource/

Statements

Subject Item
dbr:BSAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Program_synthesis
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Quine–McCluskey_algorithm
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Satz_(SAT_solver)
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Science_and_technology_in_Ukraine
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Elimination_theory
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Entropy_compression
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Entscheidungsproblem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Enumeration_algorithm
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:List_of_computability_and_complexity_topics
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Millennium_Prize_Problems
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:NP_(complexity)
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Negation_normal_form
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:MAX-3SAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Membrane_computing
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Symmetric_Boolean_function
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Probabilistic_programming
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Bart_Selman
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Book_embedding
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Deterministic_finite_automaton
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Algorithm_selection
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Algorithmic_Lovász_local_lemma
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Algorithmic_efficiency
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Alloy_(specification_language)
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:List_of_important_publications_in_theoretical_computer_science
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Resolution_(logic)
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Richard_Lipton
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Richard_M._Karp
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:DIMACS
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:DPLL(T)
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:DPLL_algorithm
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbp:class
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Vertex_cover
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Vertex_cover_in_hypergraphs
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Decision_problem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Index_of_combinatorics_articles
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Interval_scheduling
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Quantum_computing
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:List_of_mathematical_proofs
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:PSPACE-complete
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:K-SAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:K-cnf-sat
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Not-all-equal_3-satisfiability
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Timeline_of_artificial_intelligence
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:♯P
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:♯P-completeness_of_01-permanent
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:1-in-3-SAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Cristopher_Moore
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:SL_(complexity)
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Oracle_machine
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Valiant–Vazirani_theorem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Schaefer's_dichotomy_theorem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:One-in-three_3SAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Clique_problem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Co-NP
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Gap_reduction
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:George_Boole
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:George_Logemann
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Glossary_of_artificial_intelligence
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Model_checking
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:NLTS_Conjecture
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Concolic_testing
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Conflict-driven_clause_learning
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Conjunctive_normal_form
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Constraint_programming
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Constraint_satisfaction
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Constraint_satisfaction_problem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Cook–Levin_theorem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Optical_computing
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Leonard_Adleman
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:MAXEkSAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Simulated_annealing
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Stephen_Cook
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Computational_complexity
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Computational_complexity_theory
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Computational_hardness_assumption
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:ZYpp
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Function_problem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Horn-satisfiability
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Horn_clause
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:PCP_theorem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:PLS_(complexity)
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Post_correspondence_problem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Propositional_directed_acyclic_graph
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Spectrum_of_a_sentence
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
n31:Ones_classification_theorems
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Maximum_satisfiability_problem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Time_complexity
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:TwixT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:GRASP_(SAT_solver)
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Galactic_algorithm
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Karloff–Zwick_algorithm
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Karp's_21_NP-complete_problems
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:List_of_Boolean_algebra_topics
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Local_search_(optimization)
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Logic_programming
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Minimum-weight_triangulation
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:P-complete
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:3-satisfiability
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:3cnf
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:3cnf-sat
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:3cnfsat
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Algorithms_for_solving_SAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:3-dimensional_matching
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Daniel_J._Hulme
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Alternating_Turing_machine
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:NuSMV
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:PP_(complexity)
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Pangram
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Parallel_SAT_solver
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Cavity_method
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Difference-map_algorithm
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Differential_cryptanalysis
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Formal_equivalence_checking
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Isolation_lemma
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:João_Marques_Silva
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Kazuo_Iwama_(computer_scientist)
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Knowledge-based_configuration
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:List_of_NP-complete_problems
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Reduction_(complexity)
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:2-satisfiability
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Harry_R._Lewis
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Heyting_algebra
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Hilary_Putnam
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Tautology_(logic)
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Boolean_SAT_solver
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Hyper-heuristic
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Unsatisfiable_core
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Social_golfer_problem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:APX
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Karp–Lipton_theorem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Binary_decision_diagram
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Symbolic_artificial_intelligence
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:SystemVerilog
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Co-NP-complete
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Heyawake
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Holographic_algorithm
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Taut
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Disjunctive_normal_form
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:3-SAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:3SAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Automated_reasoning
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Automatic_test_pattern_generation
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Boole's_expansion_theorem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Boolean
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageDisambiguates
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Boolean_algebra
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Boolean_satisfiability_algorithm_heuristics
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Boolean_satisfiability_problem
rdf:type
yago:WikicatFormalMethods yago:WikicatNP-hardProblems yago:WikicatNP-completeProblems yago:Attribute100024264 yago:WikicatSatisfiabilityProblems yago:Condition113920835 yago:PsychologicalFeature100023100 yago:Ability105616246 yago:Abstraction100002137 yago:Cognition100023271 yago:Know-how105616786 yago:State100024720 yago:Method105660268 yago:Problem114410605 dbo:Disease yago:Difficulty114408086
rdfs:label
布尔可满足性问题 Bulea plenumebloproblemo 충족 가능성 문제 Problema de satisfatibilidade booliana 充足可能性問題 Problema de satisfacibilitat booleana Задача здійсненності булевих формул مسألة قابلية الإرضاء المنطقية Problém splnitelnosti booleovské formule Soddisfacibilità booleana Problème SAT Задача выполнимости булевых формул Problema de satisfacibilidad booleana Boolean satisfiability problem Vervulbaarheidsprobleem Erfüllbarkeitsproblem der Aussagenlogik Problem spełnialności
rdfs:comment
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. 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 é 충족 가능성 문제(充足可能性問題, satisfiability problem, SAT)는 어떠한 변수들로 이루어진 논리식이 주어졌을 때, 그 논리식이 참이 되는 변수값이 존재하는지를 찾는 문제이다. 만족성 문제, 만족도 문제, 만족 문제, 불린 충족 가능성 문제(boolean satisfiability problem)라고도 부른다. 充足可能性問題(じゅうそくかのうせいもんだい、satisfiability problem, SAT)は、一つの命題論理式が与えられたとき、それに含まれる変数の値を偽 (False) あるいは真 (True) にうまく定めることによって全体の値を'真'にできるか、という問題をいう。SATisfiabilityの頭3文字を取ってしばしば「SAT」と呼ばれる。 Зада́ча здійсне́нності бу́левих фо́рмул (SAT, від англ. satisfiability) — важлива для теорії обчислювальної складності алгоритмічна задача. Об'єктом задачі SAT є , що складається тільки з назв змінних, дужок і операцій (І) (АБО) і (НІ).Задача полягає в наступному: чи можна призначити усім змінним, що трапляються у формулі, значення хибність і істина так, щоб формула стала істинною. مسألة قابلية الإرضاء المنطقية، في المنطق وعلوم الحاسوب، (تسمى أحيانًا مسألة قابلية الإرضاء الافتراضية وتختصر إلى قابلية الإرضاء أو إس إيه تي أو بي-إس إيه تي) هي مسألة تحديد وجود ترجمة تفسيرية ترضي صيغة منطقية معينة. بمعنى آخر، تستعلم ما إذا كان يمكن استبدال متغيرات صيغة منطقية معينة باستمرار بالقيم TRUE (صح) أو FALSE (خطأ) بطريقة تكون نتيجة الصيغة TRUE. إذا طبقت هذه الحالة، تسمى الصيغة مرضية. من ناحية أخرى، في حالة عدم وجود تعيين كهذا، تكون الوظيفة المعبر عنها بواسطة الصيغة FALSE لجميع تعيينات المتغيرات المحتملة وتكون الصيغة غير مرضية. مثلًا، تعد الصيغة «a AND NOT b (إيه و نفي بي) مرضية لأنه يمكن إيجاد قيمتين a = TRUE و b = FALSE، تحققان الصيغة (a AND NOT b = TRUE). في المقابل، تعد الصيغة «a AND NOT a» غير مُرضية. Зада́ча выполни́мости бу́левых фо́рмул (SAT, ВЫП) — важная для теории вычислительной сложности алгоритмическая задача. Экземпляром задачи является булева формула, состоящая только из имён переменных, скобок и операций (И), (ИЛИ) и (HE).Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной. 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 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. 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). 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ą. 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). 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. 可滿足性(英語:Satisfiability)是用來解決給定的真值方程式,是否存在一组变量赋值,使問題为可满足。布尔可滿足性問題(Boolean satisfiability problem;SAT )屬於決定性問題,也是第一个被证明屬於NP完全的问题。此問題在電腦科學上許多的領域皆相當重要,包括、演算法、人工智慧、等等。 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. 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. 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
foaf:depiction
n26:Sat_reduced_to_Clique_from_Sipser.svg n26:Schaefer's_3-SAT_to_1-in-3-SAT_reduction.gif n26:Boolean_satisfiability_vs_true_literal_counts.png
dct:subject
dbc:NP-complete_problems dbc:Boolean_algebra dbc:Logic_in_computer_science dbc:Satisfiability_problems dbc:Electronic_design_automation dbc:Formal_methods
dbo:wikiPageID
4715
dbo:wikiPageRevisionID
1117934167
dbo:wikiPageWikiLink
dbr:2-SAT dbr:Polynomial-time dbr:Tautology_(logic) dbr:Logic dbr:First-order_predicate_calculus dbr:Cryptography dbr:Entailment dbr:Valiant-Vazirani_theorem dbr:P_(complexity) dbr:NP_(complexity_class) dbr:PH_(complexity) dbr:Unit_propagation n10:Sat_reduced_to_Clique_from_Sipser.svg dbr:University_of_Toronto dbr:Automatic_test_pattern_generation dbr:Leonid_Levin n10:Schaefer's_3-SAT_to_1-in-3-SAT_reduction.gif dbr:Polynomial-time_approximation_scheme dbr:Graph_(discrete_mathematics) dbr:Polynomial_hierarchy dbr:Graph_coloring dbr:L_(complexity) dbr:Conjunctive_normal_form dbr:SL_(complexity) dbr:Logical_conjunction dbr:Quantified_Boolean_formula_problem dbr:Exclusive_or dbr:Logical_value dbr:Uninterpreted_function dbr:Model_checking dbr:Computational_complexity_theory dbr:Polynomial-time_reduction dbr:Substitution_(logic) dbr:Approximation_algorithm dbr:Maximum_satisfiability_problem dbr:Propositional_logic dbr:Formal_equivalence_checking dbr:Tseytin_transformation dbr:FP_(complexity) dbr:Schaefer's_dichotomy_theorem dbr:BPP_(complexity) dbr:Horn_clause dbr:P_system dbr:Gaussian_elimination dbr:P_versus_NP_problem dbr:Scheduling_algorithm dbc:NP-complete_problems dbr:Routing_(electronic_design_automation) dbr:P-complete dbc:Boolean_algebra dbr:Exponential_time_hypothesis dbr:Microprocessor dbr:Unsatisfiable_core dbr:Stephen_Cook dbr:Quantifier_(logic) dbr:David_S._Johnson dbr:Logically_equivalent dbr:Algorithmics dbr:∀ dbr:FPGA dbr:∃ dbr:Conflict-driven_clause_learning dbr:Formal_verification dbr:Sharp-SAT dbr:0-1_integer_programming n10:Boolean_satisfiability_vs_true_literal_counts.png dbr:Artificial_intelligence dbr:Negation dbr:Search_problem dbr:DPLL_algorithm dbr:WalkSAT dbr:Small_o_notation dbr:PP_(complexity) dbr:Variable_(mathematics) dbr:Circuit_satisfiability dbr:Boolean_algebra_(structure) dbr:Karloff–Zwick_algorithm dbr:Cook–Levin_theorem dbr:Boolean_function dbr:Circuit_design dbr:NL-complete dbc:Logic_in_computer_science dbr:Formula_(mathematical_logic) dbr:Local_search_(constraint_satisfaction) dbr:Interpretation_(logic) dbr:Sharp-P-complete dbr:PSPACE-complete dbr:NP-complete dbr:NP-hard dbr:Co-NP-complete dbr:US_(complexity) dbr:Complexity_class dbr:Electronic_design_automation dbr:P_(complexity_class) n52:poly dbr:Decision_problem dbr:Contradiction dbr:Equisatisfiable dbr:RP_(complexity) dbr:APX dbc:Satisfiability_problems dbr:Second-order_logic dbr:Automated_planning_and_scheduling dbr:Russian_Academy_of_Sciences dbr:Thomas_Jerome_Schaefer dbr:Karp's_21_NP-complete_problems dbr:P_=_NP_problem dbr:Boolean_logic dbr:Planar_SAT dbr:Planar_graph dbr:Karp–Lipton_theorem dbr:Computer_science dbr:Michael_R._Garey dbc:Electronic_design_automation dbr:NL_(complexity) dbr:Davis–Putnam–Logemann–Loveland_algorithm dbr:FNP_(complexity) dbr:Logical_disjunction dbr:Reduction_(complexity) dbr:Bounded-error_probabilistic_polynomial dbr:Promise_problem dbr:Finite_field dbr:Satisfiability dbr:Satisfiability_modulo_theories dbr:Turing_machine dbr:Stochastic dbr:Constraint_satisfaction_problem dbr:NP_(complexity) dbr:Theoretical_computer_science dbr:Boolean_rings dbc:Formal_methods dbr:Automatic_theorem_proving dbr:Disjunctive_normal_form dbr:Clique_problem
dbo:wikiPageExternalLink
n11:jpms-date99a.pdf n13:eNews_061201.html n14:jpms-date99a.pdf n19:satgame.php%3Flang=eng n33:www.satlive.org n36: n41: n42:Asynchronous%20Team%20Algorithms%20for%20Boolean%20Satisfiability.pdf%7C n44:index.html n33:www.sigda.org n48:~karem n49:tcom06.pdf%7C n54: n55: n58:jpms-date99a.pdf
owl:sameAs
dbpedia-ja:充足可能性問題 dbpedia-sr:САТ_проблем dbpedia-simple:Boolean_satisfiability_problem dbpedia-he:בעיית_הספיקות dbpedia-zh:布尔可满足性问题 dbpedia-cs:Problém_splnitelnosti_booleovské_formule yago-res:Boolean_satisfiability_problem dbpedia-fa:مسئله_صدق‌پذیری_بولی freebase:m.01hmj dbpedia-eo:Bulea_plenumebloproblemo dbpedia-fr:Problème_SAT n34:51oKL dbpedia-pl:Problem_spełnialności dbpedia-it:Soddisfacibilità_booleana wikidata:Q875276 dbpedia-de:Erfüllbarkeitsproblem_der_Aussagenlogik dbpedia-nl:Vervulbaarheidsprobleem dbpedia-es:Problema_de_satisfacibilidad_booleana dbpedia-th:ปัญหาความสอดคล้องแบบบูล dbpedia-pt:Problema_de_satisfatibilidade_booliana dbpedia-ar:مسألة_قابلية_الإرضاء_المنطقية dbpedia-hu:Logikai_kielégítési_probléma dbpedia-ca:Problema_de_satisfacibilitat_booleana dbpedia-sh:SAT_problem dbpedia-ru:Задача_выполнимости_булевых_формул dbpedia-ko:충족_가능성_문제 dbpedia-uk:Задача_здійсненності_булевих_формул
dbp:wikiPageUsesTemplate
dbt:Main dbt:Citation_needed dbt:Cite_book dbt:Cite_journal dbt:Additional_citations_needed dbt:Color dbt:Math dbt:Commons_category dbt:Tmath dbt:Short_description dbt:Fontcolor dbt:Redirect dbt:Reflist dbt:Logic dbt:Refn dbt:Refend dbt:Refbegin dbt:Mvar
dbo:thumbnail
n26:Sat_reduced_to_Clique_from_Sipser.svg?width=300
dbo:abstract
Зада́ча здійсне́нності бу́левих фо́рмул (SAT, від англ. satisfiability) — важлива для теорії обчислювальної складності алгоритмічна задача. Об'єктом задачі SAT є , що складається тільки з назв змінних, дужок і операцій (І) (АБО) і (НІ).Задача полягає в наступному: чи можна призначити усім змінним, що трапляються у формулі, значення хибність і істина так, щоб формула стала істинною. Згідно з теоремою Кука, доведеною Стівеном Куком в 1971-му році, задача SAT для булевих формул, записаних в кон'юнктивній нормальній формі, є NP-повною. Вимога про запис у кон'юнктивній формі є важливою, оскільки, наприклад, для формул, представлених в диз'юнктивній нормальній формі, задача SAT тривіально вирішується за лінійний час від розміру запису формули. 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. 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. 可滿足性(英語:Satisfiability)是用來解決給定的真值方程式,是否存在一组变量赋值,使問題为可满足。布尔可滿足性問題(Boolean satisfiability problem;SAT )屬於決定性問題,也是第一个被证明屬於NP完全的问题。此問題在電腦科學上許多的領域皆相當重要,包括、演算法、人工智慧、等等。 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. 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. 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. 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. 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. 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. 充足可能性問題(じゅうそくかのうせいもんだい、satisfiability problem, SAT)は、一つの命題論理式が与えられたとき、それに含まれる変数の値を偽 (False) あるいは真 (True) にうまく定めることによって全体の値を'真'にできるか、という問題をいう。SATisfiabilityの頭3文字を取ってしばしば「SAT」と呼ばれる。 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 . 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). Зада́ча выполни́мости бу́левых фо́рмул (SAT, ВЫП) — важная для теории вычислительной сложности алгоритмическая задача. Экземпляром задачи является булева формула, состоящая только из имён переменных, скобок и операций (И), (ИЛИ) и (HE).Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной. Согласно теореме Кука, доказанной Стивеном Куком в 1971 году, задача SAT для булевых формул, записанных в конъюнктивной нормальной форме, является NP-полной. Требование о записи в конъюнктивной форме существенно, так как, например, задача SAT для формул, представленных в дизъюнктивной нормальной форме, тривиально решается за линейное время в зависимости от размера записи формулы (для выполнимости формулы требуется только наличие хотя бы одной конъюнкции, не содержащей одновременно и отрицание для некоторой переменной ). 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). مسألة قابلية الإرضاء المنطقية، في المنطق وعلوم الحاسوب، (تسمى أحيانًا مسألة قابلية الإرضاء الافتراضية وتختصر إلى قابلية الإرضاء أو إس إيه تي أو بي-إس إيه تي) هي مسألة تحديد وجود ترجمة تفسيرية ترضي صيغة منطقية معينة. بمعنى آخر، تستعلم ما إذا كان يمكن استبدال متغيرات صيغة منطقية معينة باستمرار بالقيم TRUE (صح) أو FALSE (خطأ) بطريقة تكون نتيجة الصيغة TRUE. إذا طبقت هذه الحالة، تسمى الصيغة مرضية. من ناحية أخرى، في حالة عدم وجود تعيين كهذا، تكون الوظيفة المعبر عنها بواسطة الصيغة FALSE لجميع تعيينات المتغيرات المحتملة وتكون الصيغة غير مرضية. مثلًا، تعد الصيغة «a AND NOT b (إيه و نفي بي) مرضية لأنه يمكن إيجاد قيمتين a = TRUE و b = FALSE، تحققان الصيغة (a AND NOT b = TRUE). في المقابل، تعد الصيغة «a AND NOT a» غير مُرضية. تعد المسألة كثيرة الحدود غير القطعية الكاملة أول مسألة يثبت أنها مسألة قابلة للإرضاء منطقية؛ انظر مبرهنة كوك وليفين. يعني هذا أن جميع المسائل من فئة تعقيد المسألة كثيرة الحدود غير القطعية، والتي تتضمن مجموعة واسعة من مسائل القرار والتحسين الطبيعية، يصعب حلها كمسألة قابلية الإرضاء. لا توجد خوارزمية معروفة تعمل على حل جميع مسائل قابلية الإرضاء بكفاءة، ويُعتقد عمومًا أنه لا توجد خوارزمية كهذه؛ ولكن، لم يثبت هذا الاعتقاد رياضيًا، يكافئ حل سؤال ما إذا كانت مسألة قابلية الإرضاء تملك خوارزمية حدودية الزمن مسألة كثير حدود وكثير حدود غير قطعي، وهي مسألة مفتوحة شهيرة في نظرية الحوسبة. أصبحت خوارزميات مسألة قابلية الإرضاء المنطقية التجريبية منذ عام 2007 قادرة على حل حالات المسائل التي تتضمن عشرات الآلاف من المتغيرات والصيغ التي تتكون من ملايين الرموز، أي ما يكفي للعديد من مسائل قابلية الإرضاء العملية في الذكاء الاصطناعي وتصميم الدوائر الكهربائية وإثبات النظرية التلقائية مثلًا. 충족 가능성 문제(充足可能性問題, satisfiability problem, SAT)는 어떠한 변수들로 이루어진 논리식이 주어졌을 때, 그 논리식이 참이 되는 변수값이 존재하는지를 찾는 문제이다. 만족성 문제, 만족도 문제, 만족 문제, 불린 충족 가능성 문제(boolean satisfiability problem)라고도 부른다.
gold:hypernym
dbr:Problem
prov:wasDerivedFrom
wikipedia-en:Boolean_satisfiability_problem?oldid=1117934167&ns=0
dbo:wikiPageLength
52424
foaf:isPrimaryTopicOf
wikipedia-en:Boolean_satisfiability_problem
Subject Item
dbr:Planar_SAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Polynomial_hierarchy
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Circuit_Value_Problem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Circuit_satisfiability_problem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Methods_for_solving_SAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Ian_Gent
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Algorithms_for_solving_the_boolean_satisfiability_problem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Rainbow-independent_set
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Chaff_algorithm
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:CNF-SAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:CNFSAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Model-based_testing
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:SAT_(disambiguation)
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageDisambiguates
dbr:Boolean_satisfiability_problem
Subject Item
dbr:SAT_solver
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:SNP_(complexity)
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Satisfiability
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Satisfiability_modulo_theories
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:System_on_a_chip
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:USAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Vienna_Summer_of_Logic
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Vijay_Vazirani
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Nerode_Prize
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Nike_Sun
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Uwe_Schöning
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Satplan
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Sharp-SAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Expert_system
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Exponential_time_hypothesis
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:FKT_algorithm
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Implication_graph
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:List_of_volunteer_computing_projects
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Thomas_Jerome_Schaefer
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:NP-completeness
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:NP-hardness
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:NP-intermediate
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Natural_proof
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Planning_Domain_Definition_Language
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Tseytin_transformation
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Solver
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Second-order_propositional_logic
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:List_of_SAT_solvers
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:P_system
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:P_versus_NP_problem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:WalkSAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:True_quantified_Boolean_formula
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Structural_complexity_theory
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Tentai_Show
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Boolean_SAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Boolean_Satisfiability
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Boolean_satisfiability
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Linear_SAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Propositional_satisfiability
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Propositional_satisfiability_problem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Satisfiability_Problem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Satisfiability_of_boolean_expressions
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:XOR-SAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:XOR-satisfiability
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:SAT_problem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:SAT_solving
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Counted_Boolean_Satisfiability_Problem
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Unique-SAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
dbr:Unambiguous_SAT
dbo:wikiPageWikiLink
dbr:Boolean_satisfiability_problem
dbo:wikiPageRedirects
dbr:Boolean_satisfiability_problem
Subject Item
wikipedia-en:Boolean_satisfiability_problem
foaf:primaryTopic
dbr:Boolean_satisfiability_problem