Spelling suggestions: "subject:"aussagenlogik"" "subject:"aussagenlogiken""
1 |
Partielle Wissenskompilation Wissensrepräsentation und ReasoningstrategieObermaier, Claudia January 2007 (has links)
Zugl.: Diplomarbeit
|
2 |
Lineare Algebra und Erfüllbarkeitsalgorithmen für zufällige FormelnNeupert, Sascha. January 2005 (has links)
Chemnitz, Techn. Univ., Diplomarb., 2005.
|
3 |
Zur Effizienz der Beweissuche in der Logikverarbeitung /Dunker, Ulf. January 1997 (has links)
Zugl.: Paderborn, Universiẗat, Diss., 1997.
|
4 |
Interactive learning environments for mathematical topicsArnold, Rudolf January 2007 (has links)
Zürich, Eidgenössische Techn. Hochsch., Diss., 2007. / Zsfassung in engl. und dt. Sprache.
|
5 |
Spektrale Algorithmen - Mit Eigenwerten schwierige Probleme lösenLanka, André 25 April 2008 (has links) (PDF)
Bei der Partitionierung von Graphen versucht man, Strukturen in Graphen zu finden (etwa 3-Färbungen oder kleine Bisektionen). Mithilfe von Eigenwerten und Eigenvektoren können solche Probleme oftmals effizient gelöst werden. Wir stellen einen Algorithmus vor, der auf einem sehr allgemeinen Modell für zufällige Graphen bewiesenermaßen sehr gute Dienste leistet.
Weiterhin untersuchen wir zufällige 3Sat-Formeln. Hier wollen wir mit Eigenwerten obere Schranken an die Anzahl der erfüllbaren Klauseln finden. Die gefundenen Schranken sind (in den meisten Fällen) nahezu optimal.
|
6 |
Lineare Algebra und Erfüllbarkeitsalgorithmen für zufällige FormelnNeupert, Sascha 13 August 2005 (has links) (PDF)
Es werden effiziente Algorithmen vorgestellt, die
auf algebraischen Methoden beruhen um die
Unerfüllbarkeit aussagenlogischer 4-SAT Formeln zu
zertifizieren. Die Algorithmen werden implementiert
und auf praktische Weise hinsichtlich der Laufzeit
mit Backtracking-Algorithmen verglichen.
|
7 |
SAT Compilation for Constraints over Structured Finite DomainsBau, Alexander 22 March 2017 (has links) (PDF)
A constraint is a formula in first-order logic expressing a relation between values of various domains. In order to solve a constraint, constructing a propositional encoding is a successfully applied technique that benefits from substantial progress made in the development of modern SAT solvers. However, propositional encodings are generally created by developing a problem-specific generator program or by crafting them manually, which often is a time-consuming and error-prone process especially for constraints over complex domains. Therefore, the present thesis introduces the constraint solver CO4 that automatically generates propositional encodings for constraints over structured finite domains written in a syntactical subset of the functional programming language Haskell. This subset of Haskell enables the specification of expressive and concise constraints by supporting user-defined algebraic data types, pattern matching, and polymorphic types, as well as higher-order and recursive functions. The constraint solver CO4 transforms a constraint written in this high-level language into a propositional formula. After an external SAT solver determined a satisfying assignment for the variables in the generated formula, a solution in the domain of discourse is derived. This approach is even applicable for finite restrictions of recursively defined algebraic data types. The present thesis describes all aspects of CO4 in detail: the language used for specifying constraints, the solving process and its correctness, as well as exemplary applications of CO4.
|
8 |
Spektrale Algorithmen - Mit Eigenwerten schwierige Probleme lösenLanka, André 25 April 2008 (has links)
Bei der Partitionierung von Graphen versucht man, Strukturen in Graphen zu finden (etwa 3-Färbungen oder kleine Bisektionen). Mithilfe von Eigenwerten und Eigenvektoren können solche Probleme oftmals effizient gelöst werden. Wir stellen einen Algorithmus vor, der auf einem sehr allgemeinen Modell für zufällige Graphen bewiesenermaßen sehr gute Dienste leistet.
Weiterhin untersuchen wir zufällige 3Sat-Formeln. Hier wollen wir mit Eigenwerten obere Schranken an die Anzahl der erfüllbaren Klauseln finden. Die gefundenen Schranken sind (in den meisten Fällen) nahezu optimal.
|
9 |
A new algorithm for the quantified satisfiability problem, based on zero-suppressed binary decision diagrams and memoizationGhasemzadeh, Mohammad January 2005 (has links)
Quantified Boolean formulas (QBFs) play an important role in theoretical computer science. QBF extends propositional logic in such a way that many advanced forms of reasoning can be easily formulated and evaluated.
In this dissertation we present our ZQSAT, which is an algorithm for evaluating quantified Boolean formulas. ZQSAT is based on ZBDD: Zero-Suppressed Binary Decision Diagram / which is a variant of BDD, and an adopted version of the DPLL algorithm. It has been implemented in C using the CUDD: Colorado University Decision Diagram package.
<br><br>
The capability of ZBDDs in storing sets of subsets efficiently enabled us to store the clauses of a QBF very compactly and let us to embed the notion of memoization to the DPLL algorithm. These points led us to implement the search algorithm in such a way that we could store and reuse the results of all previously solved subformulas with a little overheads. ZQSAT can solve some sets of standard QBF benchmark problems (known to be hard for DPLL based algorithms) faster than the best existing solvers. In addition to prenex-CNF, ZQSAT accepts prenex-NNF formulas. We show and prove how this capability can be exponentially beneficial.
<br><br> / In der Dissertation stellen wir einen neuen Algorithmus vor, welcher Formeln
der quantifizierten Aussagenlogik (engl. Quantified Boolean formula, kurz QBF)
löst. QBFs sind eine Erweiterung der klassischen Aussagenlogik um die Quantifizierung über aussagenlogische Variablen. Die quantifizierte Aussagenlogik ist dabei eine konservative Erweiterung der Aussagenlogik, d.h. es können nicht mehr Theoreme nachgewiesen werden als in der gewöhnlichen Aussagenlogik. Der Vorteil der Verwendung von QBFs ergibt sich durch die Möglichkeit, Sachverhalte kompakter zu repräsentieren.
<br><br>
SAT (die Frage nach der Erfüllbarkeit einer Formel der Aussagenlogik) und
QSAT (die Frage nach der Erfüllbarkeit einer QBF) sind zentrale Probleme
in der Informatik mit einer Fülle von Anwendungen, wie zum Beispiel in der
Graphentheorie, bei Planungsproblemen, nichtmonotonen Logiken oder bei der
Verifikation. Insbesondere die Verifikation von Hard- und Software ist ein sehr
aktuelles und wichtiges Forschungsgebiet in der Informatik.
<br><br>
Unser Algorithmus zur Lösung von QBFs basiert auf sogenannten ZBDDs
(engl. Zero-suppressed Binary decision Diagrams), welche eine Variante der
BDDs (engl. Binary decision Diagrams) sind. BDDs sind eine kompakte Repräsentation von Formeln der Aussagenlogik. Der Algorithmus kombiniert nun
bekannte Techniken zum Lösen von QBFs mit der ZBDD-Darstellung unter
Verwendung geeigneter Heuristiken und Memoization. Memoization ermöglicht
dabei das einfache Wiederverwenden bereits gelöster Teilprobleme.
<br><br>
Der Algorithmus wurde unter Verwendung des CUDD-Paketes (Colorado
University Decision Diagram) implementiert und unter dem Namen ZQSAT
veröffentlicht. In Tests konnten wir nachweisen, dass ZQSAT konkurrenzfähig
zu existierenden QBF-Beweisern ist, in einigen Fällen sogar bessere Resultate
liefern kann.
|
10 |
Towards Next Generation Sequential and Parallel SAT Solvers / Hin zur nächsten Generation Sequentieller und Paralleler SAT-SolverManthey, Norbert 08 January 2015 (has links) (PDF)
This thesis focuses on improving the SAT solving technology. The improvements focus on two major subjects: sequential SAT solving and parallel SAT solving.
To better understand sequential SAT algorithms, the abstract reduction system Generic CDCL is introduced. With Generic CDCL, the soundness of solving techniques can be modeled. Next, the conflict driven clause learning algorithm is extended with the three techniques local look-ahead, local probing and all UIP learning that allow more global reasoning during search. These techniques improve the performance of the sequential SAT solver Riss. Then, the formula simplification techniques bounded variable addition, covered literal elimination and an advanced cardinality constraint extraction are introduced. By using these techniques, the reasoning of the overall SAT solving tool chain becomes stronger than plain resolution. When using these three techniques in the formula simplification tool Coprocessor before using Riss to solve a formula, the performance can be improved further.
Due to the increasing number of cores in CPUs, the scalable parallel SAT solving approach iterative partitioning has been implemented in Pcasso for the multi-core architecture. Related work on parallel SAT solving has been studied to extract main ideas that can improve Pcasso. Besides parallel formula simplification with bounded variable elimination, the major extension is the extended clause sharing level based clause tagging, which builds the basis for conflict driven node killing. The latter allows to better identify unsatisfiable search space partitions. Another improvement is to combine scattering and look-ahead as a superior search space partitioning function. In combination with Coprocessor, the introduced extensions increase the performance of the parallel solver Pcasso. The implemented system turns out to be scalable for the multi-core architecture. Hence iterative partitioning is interesting for future parallel SAT solvers.
The implemented solvers participated in international SAT competitions. In 2013 and 2014 Pcasso showed a good performance. Riss in combination with Copro- cessor won several first, second and third prices, including two Kurt-Gödel-Medals. Hence, the introduced algorithms improved modern SAT solving technology.
|
Page generated in 0.2507 seconds