The talk describes a new method for solving systems of linear inequalities over the rational and real numbers (or, equivalently, linear programming) - the conflict resolution method. The method is a new approach to a classic problem in mathematics and computer science, that has been known since the 19th century. The problem has a wide range of real-life applications of increasing importance in both academic and industrial areas. The problem has been a subject of intensive research for the past two centuries and only a handful of methods had been developed for solving it.

Conflict resolution is a solution driven method. Given a system of linear inequalities and an assignment on variables, the method iteratively modifies the assignment aiming at obtaining a solution. During this process a conflict can arise when the current assignment cannot be directly modified to satisfy the system of inequalities. In this case there exists at least one pair of conflicting inequalities which impedes the refinement. Such a conflict is resolved by deriving a new inequality form the conflicting pair and adding it to the current system of inequalities. The process continues until either the assignment is refined into a solution, or trivially unsatisfiable inequality is derived, showing unsatisfiability of the initial system of inequalities. Generation of new constraints ensures that new constraints are non-redundant in some natural sense.

Conflict resolution is not only used for solving linear programming problems, but also is well-suited to Satisfiability Modulo Theories (SMT) framework. SMT is a new and rapidly developing branch of automated reasoning dedicated to reasoning in first-order logic with (combination) of various theories. A considerable part of SMT problems arise from real-life applications that involve theories of linear real and integer arithmetic. Reasoning on such instances incorporates reasoning in linear arithmetic. There are certain requirements imposed on theory reasoners when they are integrated in SMT solving. Our conflict resolution method possesses all the attributes necessary for integration into SMT. As the experimental evaluation of the method has shown, the method is very promising and competitive to the existing ones.