3 resultados para Prove it works

em ArchiMeD - Elektronische Publikationen der Universität Mainz - Alemanha


Relevância:

90.00% 90.00%

Publicador:

Resumo:

The use of linear programming in various areas has increased with the significant improvement of specialized solvers. Linear programs are used as such to model practical problems, or as subroutines in algorithms such as formal proofs or branch-and-cut frameworks. In many situations a certified answer is needed, for example the guarantee that the linear program is feasible or infeasible, or a provably safe bound on its objective value. Most of the available solvers work with floating-point arithmetic and are thus subject to its shortcomings such as rounding errors or underflow, therefore they can deliver incorrect answers. While adequate for some applications, this is unacceptable for critical applications like flight controlling or nuclear plant management due to the potential catastrophic consequences. We propose a method that gives a certified answer whether a linear program is feasible or infeasible, or returns unknown'. The advantage of our method is that it is reasonably fast and rarely answers unknown'. It works by computing a safe solution that is in some way the best possible in the relative interior of the feasible set. To certify the relative interior, we employ exact arithmetic, whose use is nevertheless limited in general to critical places, allowing us to rnremain computationally efficient. Moreover, when certain conditions are fulfilled, our method is able to deliver a provable bound on the objective value of the linear program. We test our algorithm on typical benchmark sets and obtain higher rates of success compared to previous approaches for this problem, while keeping the running times acceptably small. The computed objective value bounds are in most of the cases very close to the known exact objective values. We prove the usability of the method we developed by additionally employing a variant of it in a different scenario, namely to improve the results of a Satisfiability Modulo Theories solver. Our method is used as a black box in the nodes of a branch-and-bound tree to implement conflict learning based on the certificate of infeasibility for linear programs consisting of subsets of linear constraints. The generated conflict clauses are in general small and give good rnprospects for reducing the search space. Compared to other methods we obtain significant improvements in the running time, especially on the large instances.

Relevância:

30.00% 30.00%

Publicador:

Resumo:

In this treatise we consider finite systems of branching particles where the particles move independently of each other according to d-dimensional diffusions. Particles are killed at a position dependent rate, leaving at their death position a random number of descendants according to a position dependent reproduction law. In addition particles immigrate at constant rate (one immigrant per immigration time). A process with above properties is called a branching diffusion withimmigration (BDI). In the first part we present the model in detail and discuss the properties of the BDI under our basic assumptions. In the second part we consider the problem of reconstruction of the trajectory of a BDI from discrete observations. We observe positions of the particles at discrete times; in particular we assume that we have no information about the pedigree of the particles. A natural question arises if we want to apply statistical procedures on the discrete observations: How can we find couples of particle positions which belong to the same particle? We give an easy to implement 'reconstruction scheme' which allows us to redraw or 'reconstruct' parts of the trajectory of the BDI with high accuracy. Moreover asymptotically the whole path can be reconstructed. Further we present simulations which show that our partial reconstruction rule is tractable in practice. In the third part we study how the partial reconstruction rule fits into statistical applications. As an extensive example we present a nonparametric estimator for the diffusion coefficient of a BDI where the particles move according to one-dimensional diffusions. This estimator is based on the Nadaraya-Watson estimator for the diffusion coefficient of one-dimensional diffusions and it uses the partial reconstruction rule developed in the second part above. We are able to prove a rate of convergence of this estimator and finally we present simulations which show that the estimator works well even if we leave our set of assumptions.

Relevância:

30.00% 30.00%

Publicador:

Resumo:

„Ich bin, weil du bist“ – so lautet eines der Schlüsselzitate in What I Loved, dem 2003 erschienenen dritten Roman der zeitgenössischen amerikanischen Autorin Siri Hustvedt. Die Bedeutung von Beziehung und Interaktion für die Identitätsbildung spielt eine zentrale Rolle nicht nur in diesem Roman, sondern auch in ihrem Gesamtwerk, das vier Romane, ein memoir, drei Essay-Sammlungen und einen Lyrikband umfasst. Hustvedt erforscht die Identität als ein vielschichtiges Produkt bewusster und unbewusster Verknüpfungen innerhalb der sozialen und biologischen Umwelt. Das Bewusstsein wird als eine dialogisch geprägte Entität gezeigt, dessen Identität erst durch die Beziehung auf ein Anderes geformt werden kann. Um dem Mysterium der menschlichen Identitätsfindung nachzuspüren, bedient sich Hustvedt sowohl philosophischer, psychoanalytischer, biologischer als auch kunsttheoretischer Diskurse. In ihren Romanen stellt sich die Frage nach der Erklärung von Identität als komplexe Problematik dar: Ist die Beziehung zu anderen Menschen vor allem durch unsere Entwicklung als Kind und die Nähe zu Bezugspersonen geprägt? In welchem Ausmaß ist das Empfinden von Subjektivität beeinflusst von körperlichen und unbewussten Mechanismen? Inwiefern ist die Wahrnehmung visueller Kunst eine Kooperation zwischen Betrachter und Künstler? rnDiesen und anderen Fragen geht diese Dissertation nach, indem sie Hustvedts Werk als Anlass für eine Analyse intersubjektiver Strukturen der Identität nimmt. Die Intersubjektivitätsphiloso¬phien von Hegel, Buber, Bakhtin, Husserl, und Merleau-Ponty dienen hierbei als Ausgangspunkt für die Interpretation von relationaler Identität in Hustvedts Werken. Die Dissertation konzentriert sich auf Hustvedts Darstellung der Beziehung zwischen Selbst und Anderem in der Photographie und in der Malerei, der Überschreitung von Körpergrenzen in Hysterie und Anorexie sowie der Auswirkung des Verlustes von Bezugspersonen auf die persönliche Identität. Entscheidend für den Hustvedtschen Kunstbegriff ist das Zusammenspiel von Kunstobjekt, Künstler und Betrachter. Die Grenzen zwischen Innerem und Äußeren werden aufgelöst: mal wird der Rezipient Teil des Kunstwerks, mal verschmilzt der Künstler förmlich mit seinem Objekt. Auch hier wird wiederum deutlich, dass Identität nur in Wechselbeziehung und als zwischenmenschliche Kooperation entsteht. Hustvedt betritt durch ihre einzigartige Auseinandersetzung mit den Wechselbeziehungen und fragilen Grenzen zwischen Ich und Umwelt Neuland auf dem Gebiet der literarischen Identitätsforschung, da sie ihr Prinzip des „mixing,“ des unausweichlichen Eindringens fremder Substanz in die eigene Identität, aus dem Blickwinkel dieser verschiedenen Erklärungsansätze beleuchtet. rn