955 research outputs found
IPASIR-UP: User Propagators for CDCL
No full textModern SAT solvers are frequently embedded as sub-reasoning engines into more complex tools for addressing problems beyond the Boolean satisfiability problem. Examples include solvers for Satisfiability Modulo Theories (SMT), combinatorial optimization, model enumeration and counting. In such use cases, the SAT solver is often able to provide relevant information beyond the satisfiability answer. Further, domain knowledge of the embedding system (e.g., symmetry properties or theory axioms) can be beneficial for the CDCL search, but cannot be efficiently represented in clausal form. In this paper, we propose a general interface to inspect and influence the internal behaviour of CDCL SAT solvers. Our goal is to capture the most essential functionalities that are sufficient to simplify and improve use cases that require a more fine-grained interaction with the SAT solver than provided via the standard IPASIR interface. For our experiments, we extend CaDiCaL with our interface and evaluate it on two representative use cases: enumerating graphs within the SAT modulo Symmetries framework (SMS), and as the main CDCL(T) SAT engine of the SMT solver cvc5
Lambdas, arrays and quantifiers
No full textSatisfiability Modulo Theories (SMT) refers to the problem of deciding the satisfiability of a first-order formula with respect to one or more first-order theories. In many applications of hardware and software verification, SMT solvers are employed as back-end engine to solve complex verification tasks that usually combine multiple theories, such as the theory of fixed-size bit-vectors and the theory of arrays. This thesis presents several advances in the design and implementation of theory solvers for the theory of arrays, uninterpreted functions and quantified bit-vectors.
We introduce a decision procedure for non-recursive non-extensional first-order lambda terms, which is implemented in our SMT solver Boolector to handle the theory of arrays and uninterpreted functions. We discuss various implementation aspects and algorithms as well as the advantage of using lambda terms for array reasoning. We provide an extension of the lemmas on demand for lambdas approach to handle extensional arrays and discuss an optimization that improves the overall performance of Boolector.
We further investigate common array patterns in existing SMT benchmarks that can be represented by means of more compact and succinct lambda terms. We show that exploiting lambda terms for certain array patterns is beneficial for lemma generation since it allows us to produce stronger and more succinct lemmas, which improve the overall performance, particularly on instances from symbolic execution. Our results suggest that a more expressive theory of arrays might be desirable for users of SMT solvers in order to allow more succinct encodings of common array operations.
We further propose a new approach for solving quantified SMT problems, with a particular focus on the theory of fixed-size bit-vectors. Our approach combines counterexample-guided quantifier instantiation with a syntax-guided synthesis approach to synthesize interpretations for Skolem functions and terms for quantifier instantiations. We discuss a simple yet effective approach that does not rely on heuristic quantifier instantiation techniques, which are commonly employed by current state-of-the-art SMT procedures for handling quantified formulas. We show that our techniques are competitive compared to the state-of-the-art in solving quantified bit-vectors and discuss extensions and optimizations that improve the overall performance of our approach.Das "Satisfiability Modulo Theories (SMT)" Problem beschäftigt sich mit der Erfüllbarkeit von Formeln in Prädikatenlogik erster Stufe unter Berücksichtigung einer oder mehrerer Theorien. In vielen Anwendungen im Bereich der Hardware und Software Verifikation werden SMT Prozeduren (auch SMT Solver genannt) als Backend verwendet um komplexe Verifikationsprobleme zu lösen, die üblicherweise mehrere Theorien kombinieren, wie z.B. die Theorie der Bitvektoren mit der Theorie der Arrays. Diese Dissertation beschäftigt sich mit Entscheidungsprozeduren für die Theorie der Arrays kombiniert mit nicht-interpretierten Funktionen und für Bitvektoren in Kombination mit Quantoren.
Wir stellen eine Entscheidungsprozedur für nicht-rekursive, nicht-extensionale Lambdaterme erster Stufe vor, welche in unserem SMT Solver Boolector für die Theorie der Arrays kombiniert mit nicht-interpretierten Funktionen zum Einsatz kommt. Wir beschreiben unterschiedliche Implementierungsaspekte und Algorithmen und diskutieren die Vorteile von Lambdatermen in Bezug auf die Darstellung von Arrays. Zusätzlich stellen wir eine Erweiterung für unsere Entscheidungsprozedur vor, die uns ermöglicht mit Gleichheit von Arrays, die als Lambdaterme dargestellt werden, umzugehen und beschreiben eine Optimierung, die im Allgemeinen die Laufzeit von Boolector verbessert.
Weiters beschäftigen wir uns mit unterschiedlichen Array Strukturen, die in existierenden SMT Benchmarks zum Einsatz kommen und die mit Lambdatermen kompakter dargestellt werden können. Wir zeigen, dass die alternative Darstellungsform mit Lambdatermen die Erzeugung von besseren und stärkeren Lemmas in unserer Entscheidungsprozedur ermöglicht. Dies hat zur Folge, dass die Performanz besonders auf Benchmarks, die durch symbolische Programmausführung erzeugt wurden, wesentlich gesteigert werden kann.
Im letzten Teil dieser Dissertation beschäftigten wir uns mit einem neuen Ansatz zum Lösen von quantifizierten SMT Problemen mit Fokus auf quantifizierten Bitvektoren. Unser Ansatz kombiniert eine Technik namens "counterexample-guided quantifier instantiation" mit einer Technik aus dem Bereich der Synthese um Interpretationen für Skolemfunktionen und Terme für die Instantiierung von Quantoren zu synthetisieren. Unsere Ergebnisse zeigen, dass unser Ansatz zum Lösen von quantifizierten Bitvektoren im Vergleich zum aktuellen Stand der Technik kompetitiv ist. Weiters beschreiben wir eine Erweiterung und einige Optimierung für unseren neuen Ansatz, der im Allgemeinen die Performanz wesentlich verbessert.eingereicht von Dipl.-Ing. Mathias Preiner, BscDissertation Universität Linz 201
Mauersegler weiter Wege. Mathias Enard: Kompass
No full textAnalysis of the peculiar scientific narrative in the novel of the Prix-Goncourt winning author Mathias Enard
Les commissions électorales en Afrique de l'Ouest
No full text[author: Mathias Hounkpe ; Ismaila Madior Fall]Electronic ed.: Abuja ; Bonn : FES, 201
Paul Bourget, écrivain engagé
No full textPaul Bourget, A committed writer, Yehoshua Mathias.
In the France of the early twentieth century, Paul Bourget's figure is that of a successful novelist who became gradually a «committed author». A monarchist, deeply conservative, passionate defender of religion and the family as the vital bases of the social order, he thus became the bard of the bourgeois ethic faced with the destabilization of modernity.Mathias Yehoshua. Paul Bourget, écrivain engagé. In: Vingtième Siècle, revue d'histoire, n°45, janvier-mars 1995. pp. 14-29
„Nature must be felt“ – Alexander von Humboldt, pioneer of an ecological worldview and protagonist of „transversal reason“
No full textDer Text erinnert zum 250sten Geburtsjahr an Alexander von Humboldt, ein Vordenker für eine ökologische Sicht der Welt und ein früher Protagonist „transversaler Vernunft“. Er ist als Ideengeber für die „neuen Naturtherapien“, für die Integrative Therapie und für eine ökologische Sicht in der Psychotherapie eine unverzichtbare Quelle. Einige aus dieser Perspektive wichtige Aspekte seines Denkens und Werkes werden aufgezeigt. Er ist ein Referenzautor für transversales und integratives Konzeptualisieren in unserer Zeit.The text commemorates the 250th year of birth of Alexander von Humboldt, a thought leader for an ecological view of the world and an early protagonist of „transversal reason“. He is an indispensable source of ideas for the „new nature therapies“, for integrative therapy and for an ecological viewpoint in psychotherapy. Some important aspects of his thinking and work are shown from this perspective. He is a reference author for transversal and integrative conceptualization in our time.https://www.fpi-publikation.de/gruene-texte/17-2019-petzold-h-g-mathias-wiedemann-u-natur-muss-gefuehlt-werden-alexander-v-humboldt/peerReviewedpublishedVersio
„Natur muss gefühlt werden“ – Alexander von Humboldt, Vordenker einer ökologischen Weltsicht und Protagonist „transversaler Vernunft“
No full textDer Text erinnert zum 250sten Geburtsjahr an Alexander von Humboldt, ein Vordenker für eine ökologische Sicht der Welt und ein früher Protagonist „transversaler Vernunft“. Er ist als Ideengeber für die „neuen Naturtherapien“, für die Integrative Therapie und für eine ökologische Sicht in der Psychotherapie eine unverzichtbare Quelle. Einige aus dieser Perspektive wichtige Aspekte seines Denkens und Werkes werden aufgezeigt. Er ist ein Referenzautor für transversales und integratives Konzeptualisieren in unserer Zeit.The text commemorates the 250th year of birth of Alexander von Humboldt, a thought leader for an ecological view of the world and an early protagonist of „transversal reason“. He is an indispensable source of ideas for the „new nature therapies“, for integrative therapy and for an ecological viewpoint in psychotherapy. Some important aspects of his thinking and work are shown from this perspective. He is a reference author for transversal and integrative conceptualization in our time.https://www.fpi-publikation.de/polyloge/25-2019-petzold-h-g-mathias-wiedemann-u-natur-muss-gefuehlt-werden-alexander-v-humboldt/peerReviewedpublishedVersio
The reality of fiction: the ECO by Mathias Goeritz
No full textAbstract
This article covers the full biography of a building, the Experimental Museum El Eco, designed by Germanborn and Mexican émigré artist and architect Mathias Goeritz. It provides an approach intersecting the biography of the author, the history of the building, and prominent individuals of the two cultural traditions, German and Mexican, who participated in the creation of a very special and unique building: El Eco. On the one hand, the ethics of Expressionism, the interest in non-European art, the cult of primitivism and the aesthetic system of the pair of concepts abstraction-empathy, all stemming from German culture. On the other, the pantheistic religiosity of landscape, zoomorphism and anthropomorphism, the interest in masks, and the aesthetics of monumental scale, stemming from pre-Cortesian Mexican culture. Taking the stance of intertwining Mathias Goeritz parcours with those of individuals and issues from his German past and his Mexican future – highlighting the figures of Wilhelm Worringer, Paul Westheim, Luis Barragán, Edmundo O'Gorman, and Ida Rodríguez Prampolini – this article proposes a return trip from fiction to reality, following in the footsteps of the author and comparing them with the pathway of the very building El Eco
Oswald Mathias Ungers and Sol LeWitt: Variations
No full textOne of the fundamentals of Oswald Mathias Ungers work is the definition of a new unity between art and architecture. What this investigation is focused on is the identification of the intersection point between art and architecture, considering the project for the Entrance to the Kaiserthermen in Trier (20032007) as case study, revealing the system of theoretical, methodological and compositional correspondences. Plastic art is Ungers' main interlocutor: one of the author's most important references is Sol LeWitt (1928-2007), an artist he admired and collected. Setting the work of Oswald Mathias Unger and Sol LeWitt side by side, offers the opportunity to underline the shared interpretation that the two authors have of the world of forms postulated by Henri Focillon (1881-1943) in Life of Forms, according to which form, autonomous with respect to time and place, has its own universe, governed by its own laws, space and matter. According to these premises, we propose to read Trier's building through the instruments of art, following the hypothesis that in this project art embodies a creative and positive component in the definition of architecture, a cultural stimulus that guides the author in the design process
Correction to: Editorial: symmetries and asymmetries in physics
No full textThe article Editorial: symmetries and asymmetries in physics, written by Radin Dardashti, Mathias Frisch, Giovanni Valente, was originally published electronically on the publisher’s internet portal on 3 July 2020 without open access. With the author(s)’ decision to opt for Open Choice the copyright of the article changed on 16 June 2021 to © The Author(s) 2021 and the article is forthwith distributed under a Creative Commons Attribution
- …
