We introduce a new method for solving systems of linear inequalities over the rationals-the conflict resolution method. The method successively refines an initial assignment with the help of newly derived constraints until either the assignment becomes a solution of the system or a trivially unsatisfiable constraint is derived. We show that this method is correct and terminating. Our experimental results show that conflict resolution outperforms the Fourier-Motzkin method and the Chernikov algorithm, in some cases by orders of magnitude. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Korovin, K., Tsiskaridze, N., & Voronkov, A. (2009). Conflict resolution. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5732 LNCS, pp. 509–523). https://doi.org/10.1007/978-3-642-04244-7_41
Mendeley helps you to discover research relevant for your work.