In April 2016 Manchester eScholar was replaced by the University of Manchester’s new Research Information Management System, Pure. In the autumn the University’s research outputs will be available to search and browse via a new Research Portal. Until then the University’s full publication record can be accessed via a temporary portal and the old eScholar content is available to search and browse via this archive.

Conflict Resolution

Tsiskaridze, Nestan

[Thesis]. Manchester, UK: The University of Manchester; 2011.

Access to files

Abstract

This thesis proposes a new method for solving systems of linear constraints overthe rational and real numbers (or, equivalently, linear programming) – the conflict resolution method. The method is a new approach to a classic problem inmathematics and computer science, that has been known since the 19th century.The problem has a wide range of real-life applications of increasing importancein both academic and industrial areas. Although, the problem has been a subjectof intensive research for the past two centuries only a handful of methods hadbeen developed for solving it. Consequently, new results in this field may be of aparticular value, not mentioning the development of new approaches. The motivation of our research did not arise solely from the field of linearprogramming, but rather was instantiated from problems of Satisfiability ModuloTheories (or shortly SMT ). SMT is a new and rapidly developing branch of automated reasoning dedicated to reasoning in first-order logic with (combination)of various theories, such as, linear real and integer arithmetic, theory of arrays,equality and uninterpreted functions, and others. The role of linear arithmetic in solving SMT problems is very significant,since a considerable part of SMT problems arising from real-life applicationsinvolve theories of linear real and integer arithmetic. Reasoning on such instancesincorporates reasoning in linear arithmetic. Our research spanned the fields ofSMT and linear programming. We propose a method, that is not only used for solving linear programmingproblems, but also is well-suited to SMT framework. Namely, there are certain requirements imposed on theory reasoners when they are integrated in SMTsolving. Our conflict resolution method possesses all the attributes necessary forintegration into SMT. As the experimental evaluation of the method has shown,the method is very promising and competitive to the existing ones.

Bibliographic metadata

Type of resource:
Content type:
Form of thesis:
Type of submission:
Thesis title:
Degree type:
Doctor of Philosophy
Degree programme:
PhD Computer Science
Publication date:
Location:
Manchester, UK
Total pages:
164
Abstract:
This thesis proposes a new method for solving systems of linear constraints overthe rational and real numbers (or, equivalently, linear programming) – the conflict resolution method. The method is a new approach to a classic problem inmathematics and computer science, that has been known since the 19th century.The problem has a wide range of real-life applications of increasing importancein both academic and industrial areas. Although, the problem has been a subjectof intensive research for the past two centuries only a handful of methods hadbeen developed for solving it. Consequently, new results in this field may be of aparticular value, not mentioning the development of new approaches. The motivation of our research did not arise solely from the field of linearprogramming, but rather was instantiated from problems of Satisfiability ModuloTheories (or shortly SMT ). SMT is a new and rapidly developing branch of automated reasoning dedicated to reasoning in first-order logic with (combination)of various theories, such as, linear real and integer arithmetic, theory of arrays,equality and uninterpreted functions, and others. The role of linear arithmetic in solving SMT problems is very significant,since a considerable part of SMT problems arising from real-life applicationsinvolve theories of linear real and integer arithmetic. Reasoning on such instancesincorporates reasoning in linear arithmetic. Our research spanned the fields ofSMT and linear programming. We propose a method, that is not only used for solving linear programmingproblems, but also is well-suited to SMT framework. Namely, there are certain requirements imposed on theory reasoners when they are integrated in SMTsolving. Our conflict resolution method possesses all the attributes necessary forintegration into SMT. As the experimental evaluation of the method has shown,the method is very promising and competitive to the existing ones.
Thesis main supervisor(s):
Thesis advisor(s):
Language:
en

Institutional metadata

University researcher(s):

Record metadata

Manchester eScholar ID:
uk-ac-man-scw:122316
Created by:
Tsiskaridze, Nestan
Created:
27th April, 2011, 11:51:19
Last modified by:
Tsiskaridze, Nestan
Last modified:
11th April, 2012, 18:24:25

Can we help?

The library chat service will be available from 11am-3pm Monday to Friday (excluding Bank Holidays). You can also email your enquiry to us.