[Thesis]. Manchester, UK: The University of Manchester; 2011.
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.