| 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)
|
| 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)
|
