Satisfiability (original) (raw)
قابلية الإرضاء تعبير في الرياضيات وفي نظرية التعقيد الحسابي ذو أهمية كبيرة جدا.
| Property | Value |
|---|---|
| dbo:abstract | V logice představuje splnitelnost (často zkracovaná jako SAT z anglického satisfiability) problém odpovědi na otázku, zdali existuje zadanému výrazu (formuli) zapsaného ve výrokové ... Booleovské logice například pomocí operací AND, OR a NOT přiřazení, při kterém bude výraz ohodnocen jako pravdivý. Zároveň je důležité určit,[zdroj?!] jestli pro zadaný výraz žádné takové přiřazení neexistuje, taková skutečnost implikuje, že zadaná funkce vyjádřená pomocí stanovených[zdroj?!] formulí je kontradikce (tedy že při jakémkoli vstupu je na výstupu hodnota FALSE) - při takové situaci říkáme, že je funkce nesplnitelná (anglicky unsatisfiable), jinak je funkce splnitelná (satisfiable). Například výraz a AND b je splnitelný, protože existují hodnoty a = TRUE and b = TRUE, při kterých výraz (a AND b) = TRUE. Pro zdůraznění binární[zdroj?!] povahy této úlohy se zdůrazňuje pojem Booleovská resp. výroková splnitelnost. SAT představuje první[zdroj?!] známý NP-úplný problém. To ve zkratce znamená, že není znám žádný efektivní algoritmus řešící všechny instance SAT problému v polynomiálním čase. Obecně se předpokládá, že takový algoritmus neexistuje (není to však dokázáno, viz Problém P versus NP). Dále může být široká škála přirozeně se vyskytujících problémů při rozhodování a optimalizacích transformována jako SAT problém. Třída algoritmů[zdroj?!] nazývaná může efektivně vyřešit dostatečně velké podmnožiny instancí SAT a být tak užitečná při řadě praktických aplikací, jako například při návrhu elektrických obvodů[zdroj?!] nebo při automatizovaném dokazování teorií, kdy je možné dokazovanou teorii transformovat[zdroj?!] jako instanci SAT. Rozšiřování potenciálu SAT solverů představuje v současnosti značně pokrokovou oblast, avšak prozatím neexistuje žádná metoda pro efektivní řešení všech instancí SAT.[zdroj?!] (cs) قابلية الإرضاء تعبير في الرياضيات وفي نظرية التعقيد الحسابي ذو أهمية كبيرة جدا. (ar) Erfüllbarkeit ist in der Logik und Mathematik ein metasprachliches Prädikat für die Eigenschaft von logischen Aussagen und Aussageformen. Eine Aussage ist erfüllbar, wenn es eine Belegung (Interpretation, Bewertung) der Variablen gibt, für die der Wahrheitswert des gesamten Ausdrucks wahr ist. (de) En lógica proposicional, la satisfacibilidad se define como la propiedad de un conjunto de fórmulas de tener un modelo. Decimos que una fórmula es satisfacible cuando después de analizarla bajo una interpretación dada afirmamos que tiene valor 1; o lo que es lo mismo, es verdadera. * Datos: Q1350299 (es) In mathematical logic, a formula is satisfiable if it is true under some assignment of values to its variables. For example, the formula is satisfiable because it is true when and , while the formula is not satisfiable over the integers. The dual concept to satisfiability is validity; a formula is valid if every assignment of values to its variables makes the formula true. For example, is valid over the integers, but is not. Formally, satisfiability is studied with respect to a fixed logic defining the syntax of allowed symbols, such as first-order logic, second-order logic or propositional logic. Rather than being syntactic, however, satisfiability is a semantic property because it relates to the meaning of the symbols, for example, the meaning of in a formula such as . Formally, we define an interpretation (or model) to be an assignment of values to the variables and an assignment of meaning to all other non-logical symbols, and a formula is said to be satisfiable if there is some interpretation which makes it true. While this allows non-standard interpretations of symbols such as , one can restrict their meaning by providing additional axioms. The satisfiability modulo theories problem considers satisfiability of a formula with respect to a formal theory, which is a (finite or infinite) set of axioms. Satisfiability and validity are defined for a single formula, but can be generalized to an arbitrary theory or set of formulas: a theory is satisfiable if at least one interpretation makes every formula in the theory true, and valid if every formula is true in every interpretation. For example, theories of arithmetic such as Peano arithmetic are satisfiable because they are true in the natural numbers. This concept is closely related to the consistency of a theory, and in fact is equivalent to consistency for first-order logic, a result known as Gödel's completeness theorem. The negation of satisfiability is unsatisfiability, and the negation of validity is invalidity. These four concepts are related to each other in a manner exactly analogous to Aristotle's square of opposition. The problem of determining whether a formula in propositional logic is satisfiable is decidable, and is known as the Boolean satisfiability problem, or SAT. In general, the problem of determining whether a sentence of first-order logic is satisfiable is not decidable. In universal algebra, equational theory, and automated theorem proving, the methods of term rewriting, congruence closure and unification are used to attempt to decide satisfiability. Whether a particular theory is decidable or not depends whether the theory is variable-free and on other conditions. (en) En logique mathématique, la satisfaisabilité ou satisfiabilité et la validité sont des concepts élémentaires de sémantique. Une formule est satisfaisable s'il est possible de trouver une interprétation (modèle), une façon d'interpréter tous les éléments constitutifs de la formule, qui rend la formule vraie. Une formule est universellement valide, ou en raccourci valide si, pour toutes les interprétations, la formule est vraie. Les concepts opposés sont la non satisfaisabilité ou insatisfaisabilité et la non-validité : une formule est insatisfaisable si aucune de ses interprétations ne rend la formule vraie et non valide s'il existe une interprétation qui rend la formule fausse. Les quatre concepts peuvent être appliqués aux théories. Ainsi une théorie est satisfaisable s'il existe une interprétation qui rend chacun des axiomes de la théorie vrai, non satisfaisable si toute interprétation rend l'un des axiomes faux. (fr) In de klassieke propositielogica is een propositie vervulbaar als er een toekenning van waarheidswaardes aan de atomaire formules van die propositie bestaat zodat de propositie waar is. Als zo'n toekenning niet bestaat is de propositie onvervulbaar. Een onvervulbare propositie wordt wel een contradictie genoemd. De vervulbaarheid van een formule kan met een waarheidstabel worden gecontroleerd. (nl) Na lógica matemática, satisfatibilidade e validade são conceitos elementares da semântica. Uma fórmula é satisfazível se é possível achar uma interpretação ( modelo) que torne a fórmula verdadeira. Uma fórmula é válida se todas as interpretações tornam a fórmula verdadeira. Os opostos deste conceito são insatisfatibilidade e invalidade, isto é, uma fórmula é insatisfazível se nenhuma das interpretações tornam a fórmula verdadeira, e inválida se alguma dessas interpretações tornam a fórmula falsa. Estes quatro conceitos estão relacionados uns aos outros de maneira exatamente análoga ao quadrado das oposições de Aristóteles. Os quatro conceitos podem ser usados para aplicar todas as teorias: uma teoria é satisfazível (válida) se uma (todas) as interpretações torna(m) cada um dos axiomas da teoria verdade, e a teoria é insatisfazível (inválida) se todas (uma) as interpretações tornam(a) cada um dos axiomas da teoria falso. Também é possível considerar apenas as interpretações que tornam todos os axiomas de uma segunda teoria verdadeiros. Esta generalização é comumente chamada satisfatibilidade módulo teorias. A questão de saber se uma sentença em uma proposição lógica é satisfatíval é um problema de decisão. Em geral, a questão de saber se sentenças em lógica de primeira ordem são satisfeitas não é decidível. Na álgebra universal e teoria das equações, os métodos de reescrita de termos, fecho de congruência e unificação são usados para tentar decidir satisfatibilidade. Uma teoria particular é decidida ou não depende se a teoria é livre de variável ou está em outras condições. (pt) |
| dbo:wikiPageID | 23401166 (xsd:integer) |
| dbo:wikiPageLength | 12282 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1123975948 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Propositional_calculus dbr:Entscheidungsproblem dbr:Model_theory dbr:David_Hilbert dbr:List_of_logic_systems dbr:Peano_axioms dbr:Cylindrical_algebraic_decomposition dbr:Unification_(computer_science) dbr:Validity_(logic) dbr:Decidability_(logic) dbr:Decision_problem dbr:Integer_programming dbr:Interpretation_(logic) dbr:Universal_algebra dbr:Computably_enumerable dbr:Consistency dbr:Mathematical_logic dbr:Mathematical_optimization dbr:Square_of_opposition dbr:Trakhtenbrot's_theorem dbr:NP-complete dbr:Congruence_closure dbr:Constraint_satisfaction dbr:Logical_conjunction dbr:Computational_complexity_theory dbr:Propositional_logic dbr:Syntax_(logic) dbr:Automated_theorem_proving dbr:Gödel's_completeness_theorem dbr:Karp's_21_NP-complete_problems dbr:Linear_inequality dbr:Linear_programming dbr:First-order_logic dbc:Logical_truth dbr:Hilbert's_tenth_problem dbr:Logical_constant dbr:Well-formed_formula dbr:RE_(complexity) dbr:2-satisfiability dbr:Atomic_formula dbr:Atomic_sentence dbr:Term_rewriting dbr:Aristotle dbc:Philosophy_of_logic dbc:Concepts_in_logic dbc:Model_theory dbr:Co-NP-complete dbr:Theory_(mathematical_logic) dbr:Axiom dbr:Boolean_satisfiability_problem dbr:Classical_logic dbr:Ofer_Strichman dbr:Second-order_logic dbr:Semidecidable dbr:Satisfiability_modulo_theories dbr:Semantics dbr:Undecidable_problem dbr:Variable_(mathematics) dbr:Finite_model_property dbr:Finite_model_theory dbr:System_of_linear_equations dbr:Equational_theory dbr:Variable-free dbr:PTIME dbr:Circuit_satisfiability dbr:Classical_propositional_logic dbr:Decidable_problem dbr:Structure_(logic) dbr:Theory_(logic) |
| dbp:wikiPageUsesTemplate | dbt:Cite_book dbt:Further dbt:Main dbt:Reflist dbt:Rp dbt:Sfn dbt:Short_description dbt:Clarify_span dbt:Mathematical_logic dbt:Metalogic |
| dct:subject | dbc:Logical_truth dbc:Philosophy_of_logic dbc:Concepts_in_logic dbc:Model_theory |
| gold:hypernym | dbr:Concepts |
| rdf:type | yago:WikicatConceptsInLogic yago:Abstraction100002137 yago:Cognition100023271 yago:Concept105835747 yago:Content105809192 yago:Idea105833840 yago:PsychologicalFeature100023100 dbo:Automobile |
| rdfs:comment | قابلية الإرضاء تعبير في الرياضيات وفي نظرية التعقيد الحسابي ذو أهمية كبيرة جدا. (ar) Erfüllbarkeit ist in der Logik und Mathematik ein metasprachliches Prädikat für die Eigenschaft von logischen Aussagen und Aussageformen. Eine Aussage ist erfüllbar, wenn es eine Belegung (Interpretation, Bewertung) der Variablen gibt, für die der Wahrheitswert des gesamten Ausdrucks wahr ist. (de) En lógica proposicional, la satisfacibilidad se define como la propiedad de un conjunto de fórmulas de tener un modelo. Decimos que una fórmula es satisfacible cuando después de analizarla bajo una interpretación dada afirmamos que tiene valor 1; o lo que es lo mismo, es verdadera. * Datos: Q1350299 (es) In de klassieke propositielogica is een propositie vervulbaar als er een toekenning van waarheidswaardes aan de atomaire formules van die propositie bestaat zodat de propositie waar is. Als zo'n toekenning niet bestaat is de propositie onvervulbaar. Een onvervulbare propositie wordt wel een contradictie genoemd. De vervulbaarheid van een formule kan met een waarheidstabel worden gecontroleerd. (nl) V logice představuje splnitelnost (často zkracovaná jako SAT z anglického satisfiability) problém odpovědi na otázku, zdali existuje zadanému výrazu (formuli) zapsaného ve výrokové ... Booleovské logice například pomocí operací AND, OR a NOT přiřazení, při kterém bude výraz ohodnocen jako pravdivý. Zároveň je důležité určit,[zdroj?!] jestli pro zadaný výraz žádné takové přiřazení neexistuje, taková skutečnost implikuje, že zadaná funkce vyjádřená pomocí stanovených[zdroj?!] formulí je kontradikce (tedy že při jakémkoli vstupu je na výstupu hodnota FALSE) - při takové situaci říkáme, že je funkce nesplnitelná (anglicky unsatisfiable), jinak je funkce splnitelná (satisfiable). Například výraz a AND b je splnitelný, protože existují hodnoty a = TRUE and b = TRUE, při kterých výraz (a AND b) = (cs) In mathematical logic, a formula is satisfiable if it is true under some assignment of values to its variables. For example, the formula is satisfiable because it is true when and , while the formula is not satisfiable over the integers. The dual concept to satisfiability is validity; a formula is valid if every assignment of values to its variables makes the formula true. For example, is valid over the integers, but is not. (en) En logique mathématique, la satisfaisabilité ou satisfiabilité et la validité sont des concepts élémentaires de sémantique. Une formule est satisfaisable s'il est possible de trouver une interprétation (modèle), une façon d'interpréter tous les éléments constitutifs de la formule, qui rend la formule vraie. Une formule est universellement valide, ou en raccourci valide si, pour toutes les interprétations, la formule est vraie. Les concepts opposés sont la non satisfaisabilité ou insatisfaisabilité et la non-validité : une formule est insatisfaisable si aucune de ses interprétations ne rend la formule vraie et non valide s'il existe une interprétation qui rend la formule fausse. (fr) Na lógica matemática, satisfatibilidade e validade são conceitos elementares da semântica. Uma fórmula é satisfazível se é possível achar uma interpretação ( modelo) que torne a fórmula verdadeira. Uma fórmula é válida se todas as interpretações tornam a fórmula verdadeira. Os opostos deste conceito são insatisfatibilidade e invalidade, isto é, uma fórmula é insatisfazível se nenhuma das interpretações tornam a fórmula verdadeira, e inválida se alguma dessas interpretações tornam a fórmula falsa. Estes quatro conceitos estão relacionados uns aos outros de maneira exatamente análoga ao quadrado das oposições de Aristóteles. (pt) |
| rdfs:label | قابلية الإرضاء (ar) Splnitelnost (cs) Erfüllbarkeit (de) Satisfacibilidad (es) Satisfaisabilité (fr) Vervulbaarheid (nl) Satisfiability (en) Satisfatibilidade (pt) |
| owl:sameAs | freebase:Satisfiability yago-res:Satisfiability wikidata:Satisfiability dbpedia-ar:Satisfiability dbpedia-cs:Satisfiability dbpedia-de:Satisfiability dbpedia-es:Satisfiability dbpedia-et:Satisfiability dbpedia-fi:Satisfiability dbpedia-fr:Satisfiability dbpedia-hu:Satisfiability dbpedia-nl:Satisfiability dbpedia-pt:Satisfiability https://global.dbpedia.org/id/N2cX |
| prov:wasDerivedFrom | wikipedia-en:Satisfiability?oldid=1123975948&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Satisfiability |
| is dbo:wikiPageDisambiguates of | dbr:Satisfy |
| is dbo:wikiPageRedirects of | dbr:Satisfiable dbr:Unsatisfiable dbr:Satisfiability_(logics) dbr:Satisfiability_and_validity dbr:Satisfiability_problem dbr:Finite_satisfiability_(logics) |
| is dbo:wikiPageWikiLink of | dbr:Belief_propagation dbr:Satisfiable dbr:Satisficing dbr:Universal_quantification dbr:Index_of_logic_articles dbr:Levi's_lemma dbr:Skolem_normal_form dbr:Trakhtenbrot's_theorem dbr:Glossary_of_artificial_intelligence dbr:NLTS_Conjecture dbr:Constraint_satisfaction dbr:Bernays–Schönfinkel_class dbr:Link_grammar dbr:Logic_of_graphs dbr:Compactness_theorem dbr:ZYpp dbr:Action_language dbr:Laws_of_Form dbr:Linear_temporal_logic dbr:Logic_programming dbr:Logical_truth dbr:Duality_(mathematics) dbr:FO(.) dbr:Fastest dbr:Barwise_compactness_theorem dbr:Diophantine_set dbr:Fragment_(logic) dbr:RE_(complexity) dbr:Bioinformatics,_and_Empirical_&_Theoretical_Algorithmics_Lab dbr:Herbrandization dbr:Theory_(mathematical_logic) dbr:Uninterpreted_function dbr:Double_turnstile dbr:Axiom dbr:Boolean_algebras_canonically_defined dbr:Boolean_satisfiability_problem dbr:Planar_SAT dbr:Something_(concept) dbr:Method_of_analytic_tableaux dbr:Modal_μ-calculus dbr:Markov_logic_network dbr:SAT_solver dbr:Satisfaction dbr:Satisfiability_modulo_theories dbr:Satisfy dbr:Sentence_(mathematical_logic) dbr:Skolem_arithmetic dbr:Sharp-SAT dbr:Expert_system dbr:The_Art_of_Computer_Programming dbr:Vacuous_truth dbr:Outline_of_logic dbr:Parameterized_complexity dbr:Second-order_predicate dbr:Skolem's_paradox dbr:State_space_enumeration dbr:Unsatisfiable dbr:Satisfiability_(logics) dbr:Satisfiability_and_validity dbr:Satisfiability_problem dbr:Finite_satisfiability_(logics) |
| is rdfs:seeAlso of | dbr:First-order_logic |
| is foaf:primaryTopic of | wikipedia-en:Satisfiability |