Equality detection for linear arithmetic constraints  

作　　者：Li LI Kai-duo HE Ming GU Xiao-yu SONG 

机构地区：[1]Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China [2]School of Software, Tsinghua University, Beijing 100084, China [3]MOE Key Laboratory for Information System Security, Beijing 100084, China [4]Department of Electrical and Computer Engineering, Portland State University, Oregon 97207, USA

出　　处：《Journal of Zhejiang University-Science A(Applied Physics & Engineering)》2009年第12期1784-1789,共6页浙江大学学报（英文版）A辑（应用物理与工程）

基　　金：Project supported by the National Natural Science Foundation of China (Nos 60635020 and 90718039);the National Basic Research Program (973) of China (No 2004CB719406)

摘　　要：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.Satisfiability modulo theories （SMT） play a key role in verification applications. A crucial SMT problem is to com- bine 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.

关 键 词：Model checking Satisfiability modulo theories （SMT） Linear arithmetic 

分 类 号：O221.1[理学—运筹学与控制论] TP391.41[理学—数学]