Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Barrett, C., Cesare Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)
Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2008), http://www.SMT-LIB.org
Chandru, V.: Variable elimination in linear constraints. Comput. J. 36(5), 463–472 (1993)
Chernikov, S.N.: Linejnye Neravenstva. Nauka, Moscow (1968) (in Russian)
Duffin, R.J.: On Fourier’s analyse of linear inequality systems. Mathematical Programming Study 1, 71–95 (1974)
Imbert, J., Van Hentenryck, P.: A note on redundant linear constraints. Technical Report CS-92-11, CS Department, Brown University (1992)
Jaffar, J., Maher, M.J., Roland, P.S., Yap, R.H.C.: Projecting CLP(\(\mathcal{R}\)) constraints. New Generation Computing 11 (1993)
Kohler, D.A.: Projection of Convex Polyhedral Sets. PhD thesis, University of California, Barkaley (1967)
Korovin, K., Voronkov, A.: Hard Reality Tool (submitted, 2009), http://www.cs.man.ac.uk/~korovink/hr
Nieuwenhuis, R., Oliveras, A.: Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools (Invited Paper). In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 23–46. Springer, Heidelberg (2005)
Schrijver, A.: Theory of Linear and Integer Programming. John Wiley and Sons, Chichester (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Korovin, K., Tsiskaridze, N., Voronkov, A. (2009). Conflict Resolution. In: Gent, I.P. (eds) Principles and Practice of Constraint Programming - CP 2009. CP 2009. Lecture Notes in Computer Science, vol 5732. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04244-7_41
Download citation
DOI: https://doi.org/10.1007/978-3-642-04244-7_41
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04243-0
Online ISBN: 978-3-642-04244-7
eBook Packages: Computer ScienceComputer Science (R0)