In this paper,we studied the dual form of the basic line algorthm for linear programs.It can be easily implemented in tableau that similar to the primal/dual simplex method.Different from primal simplex method or dual...In this paper,we studied the dual form of the basic line algorthm for linear programs.It can be easily implemented in tableau that similar to the primal/dual simplex method.Different from primal simplex method or dual simplex method,the dual basic line algorithm can keep primal feasibility and dual feasibility at the same time in a tableau,which makes it more efficient than the former ones.Principles and convergence of dual basic line algorthm were discussed.Some examplex and computational experience were given to illustrate the efficiency of our method.展开更多
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...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.展开更多
文摘In this paper,we studied the dual form of the basic line algorthm for linear programs.It can be easily implemented in tableau that similar to the primal/dual simplex method.Different from primal simplex method or dual simplex method,the dual basic line algorithm can keep primal feasibility and dual feasibility at the same time in a tableau,which makes it more efficient than the former ones.Principles and convergence of dual basic line algorthm were discussed.Some examplex and computational experience were given to illustrate the efficiency of our method.
基金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.
