Full Text:   <1500>

CLC number: TP31

On-line Access: 2009-10-21

Received: 2008-11-12

Revision Accepted: 2009-05-04

Crosschecked: 2009-08-14

Cited: 1

Clicked: 3200

Citations:  Bibtex RefMan EndNote GB/T7714

-   Go to

Article info.
1. Reference List
Open peer comments

Journal of Zhejiang University SCIENCE A 2009 Vol.10 No.12 P.1784~1789


Equality detection for linear arithmetic constraints

Author(s):  Li LI, Kai-duo HE, Ming GU, Xiao-yu SONG

Affiliation(s):  Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China; more

Corresponding email(s):   l-li-05@mails.tsinghua.edu.cn

Key Words:  Model checking, Satisfiability modulo theories (SMT), Linear arithmetic

Li LI, Kai-duo HE, Ming GU, Xiao-yu SONG. Equality detection for linear arithmetic constraints[J]. Journal of Zhejiang University Science A, 2009, 10(12): 1784~1789.

@article{title="Equality detection for linear arithmetic constraints",
author="Li LI, Kai-duo HE, Ming GU, Xiao-yu SONG",
journal="Journal of Zhejiang University Science A",
publisher="Zhejiang University Press & Springer",

%0 Journal Article
%T Equality detection for linear arithmetic constraints
%A Li LI
%A Kai-duo HE
%A Ming GU
%A Xiao-yu SONG
%J Journal of Zhejiang University SCIENCE A
%V 10
%N 12
%P 1784~1789
%@ 1673-565X
%D 2009
%I Zhejiang University Press & Springer
%DOI 10.1631/jzus.A0820812

T1 - Equality detection for linear arithmetic constraints
A1 - Li LI
A1 - Kai-duo HE
A1 - Ming GU
A1 - Xiao-yu SONG
J0 - Journal of Zhejiang University Science A
VL - 10
IS - 12
SP - 1784
EP - 1789
%@ 1673-565X
Y1 - 2009
PB - Zhejiang University Press & Springer
ER -
DOI - 10.1631/jzus.A0820812

satisfiability modulo theories (SMT) play a key role in verification applications. A crucial SMT problem is to combine separate theory solvers for the union of theories. In previous work, the simplex method is used to determine the solvability of constraint systems and the equalities implied by constraint systems are detected by a multitude of applications of the dual simplex method. We present an effective simplex tableau-based method to identify all implicit equalities such that the simplex method is harnessed to an irreducible minimum. Experimental results show that the method is feasible and effective.

Darkslateblue:Affiliate; Royal Blue:Author; Turquoise:Article


[1] Barrett, C., Berezin, S., 2004. CVC Lite: a new implementation of the cooperating validity checker. LNCS, 3114:515-518.

[2] Barrett, C., Dill, D., Levitt, J., 1996. Validity checking for combinations of theories with equality. LNCS, 1166:187-201.

[3] Barrett, C., de Moura, L., Stump, A., 2005. SMT-COMP: satisfiability modulo theories competition. LNCS, 3576:20-23.

[4] Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Rossum, P.V., Schulz, S., Sebastiani, R., 2005. The MathSAT 3 System. LNCS, 3632:315-321.

[5] Chvatal, V., 1983. Linear Programming. Springer-Verlag New York, LLC, p.34-45.

[6] Dantzig, G.B., 1973. Fourier-Motzkin elimination and its dual. J. Comb. Theory Ser. A, 14(3):288-297.

[7] Detlefs, D., Nelson, G., Saxe, J.B., 2005. Simplify: a theorem prover for program checking. J. ACM, 52(3):365-473.

[8] Dutertre, B., de Moura, L., 2006. A fast linear-arithmetic solver for DPLL(T). LNCS, 4144:81-94.

[9] Filliatre, J.C., Owre, S., Rueb, H., Shankar, N., 2001. ICS: Integrated Canonization and Solving. Int. Conf. on Computer Aided Verification, p.246-249.

[10] Kroening, D., Strichman, O., 2008. Decision Procedures: An Algorithmic Point of View. Springer-Verlag New York Inc., p.113-122.

[11] Lassez, J.L., McAloon, K., 1992. A canonical form for generalized linear constraints. J. Symb. Comput., 13(1):1-24.

[12] McMillan, K.L., 2004. An Interpolating Theorem Prover. TACAS 2004: Tools and Algorithms for Construction and Analysis of Systems, p.102-121.

[13] Nelson, G., 1981. Techniques for Program Verification. Technical Report, CSL-81-10, Xerox Palo Alto Research Center, Palo Alto, CA.

[14] Nieuwenhuis, R., Oliveras, A., 2005. DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. Int. Conf. on Computer Aided Verification, p.321-324.

[15] Refalo, P., 1998. Approaches to the Incremental Detection of Implicit Equalities with the Revised Simplex Method. Proc. 10th Int. Symp. on Principles of Declarative Programming, p.481-496.

[16] Rueß, H., Shankar, N., 2004. Solving Linear Arithmetic Constraints. Technical Report, CSL-SRI-04-01, SRI International, Menlo Park, CA, USA.

[17] Sheini, H.M., Sakallah, K.A., 2005. A scalable method for solving satisfiability of integer linear arithmetic logic. LNCS, 3569:241-256.

[18] Stuckey, P.J., 1991. Incremental linear constraint solving and detection of implicit equalities. ORSA J. Comput., 3(4):269-271.

[19] Stump, A., Barrett, C.W., Dill, D.L., 2002. CVC: a cooperating validity checker. LNCS, 2404:500-504.

[20] Vanderbei, R.J., 2001. Linear Programming: Foundations and Extensions (2nd Ed.). Springer-Verlag New York, LLC, p.16-22.

[21] Wang, C., Ivancic, F., Ganai, M., Gupta, A., 2005. Deciding separation logic formulae by SAT and incremental negative cycle elimination. LNCS, 3835:322-336.

Open peer comments: Debate/Discuss/Question/Opinion


Please provide your name, email address and a comment

Journal of Zhejiang University-SCIENCE, 38 Zheda Road, Hangzhou 310027, China
Tel: +86-571-87952783; E-mail: cjzhang@zju.edu.cn
Copyright © 2000 - Journal of Zhejiang University-SCIENCE