This paper presents a hybrid symbolic-numeric algorithm to compute ranking functions for establishing the termination of loop programs with polynomial guards and polynomial assignments.The authors first transform the ...This paper presents a hybrid symbolic-numeric algorithm to compute ranking functions for establishing the termination of loop programs with polynomial guards and polynomial assignments.The authors first transform the problem into a parameterized polynomial optimization problem,and obtain a numerical ranking function using polynomial sum-of-squares relaxation via semidefinite programming(SDP).A rational vector recovery algorithm is deployed to recover a rational polynomial from the numerical ranking function,and some symbolic computation techniques are used to certify that this polynomial is an exact ranking function of the loop programs.At last,the authors demonstrate on some polynomial loop programs from the literature that our algorithm successfully yields nonlinear ranking functions with rational coefficients.展开更多
It is well known that resultant elimination is an effective method of solving multivariate polynomial equations. In this paper, instead of computing the target resultants via variable by variable elimination, the auth...It is well known that resultant elimination is an effective method of solving multivariate polynomial equations. In this paper, instead of computing the target resultants via variable by variable elimination, the authors combine multivariate implicit equation interpolation and multivariate resultant elimination to compute the reduced resultants, in which the technique of multivariate implicit equation interpolation is achieved by some high probability algorithms on multivariate polynomial interpolation and univariate rational function interpolation. As an application of resultant elimination, the authors illustrate the proposed algorithm on three well-known unsolved combinatorial geometric optimization problems. The experiments show that the proposed approach of resultant elimination is more efficient than some existing resultant elimination methods on these difficult problems.展开更多
The well-known Generalized Champagne Problem on simultaneous stabilization of linear systems is solved by using complex analysis and Blonders technique. We give a complete answer to the open problem proposed by Patel ...The well-known Generalized Champagne Problem on simultaneous stabilization of linear systems is solved by using complex analysis and Blonders technique. We give a complete answer to the open problem proposed by Patel et al., which automatically includes the solution to the original Champagne Problem. Based on the recent development in automated inequality-type theorem proving, a new stabilizing controller design method is established. Our numerical examples significantly improve the relevant results in the literature.展开更多
Transcriptome reconstruction is an important application of RNA-Seq,providing critical information for further analysis of transcriptome.Although RNA-Seq offers the potential to identify the whole picture of transcrip...Transcriptome reconstruction is an important application of RNA-Seq,providing critical information for further analysis of transcriptome.Although RNA-Seq offers the potential to identify the whole picture of transcriptome,it still presents special challenges.To handle these difficulties and reconstruct transcriptome as completely as possible,current computational approaches mainly employ two strategies:de novo assembly and genome-guided assembly.In order to find the similarities and differences between them,we firstly chose five representative assemblers belonging to the two classes respectively,and then investigated and compared their algorithm features in theory and real performances in practice.We found that all the methods can be reduced to graph reduction problems,yet they have different conceptual and practical implementations,thus each assembly method has its specific advantages and disadvantages,performing worse than others in certain aspects while outperforming others in anther aspects at the same time.Finally we merged assemblies of the five assemblers and obtained a much better assembly.Additionally we evaluated an assembler using genome-guided de novo assembly approach,and achieved good performance.Based on these results,we suggest that to obtain a comprehensive set of recovered transcripts,it is better to use a combination of de novo assembly and genome-guided assembly.展开更多
In this work the authors consider the problem of optimally distributing 8 points inside a unit square so that the smallest area of the(38)triangles formed by them is maximal.Symbolic computations are employed to reduc...In this work the authors consider the problem of optimally distributing 8 points inside a unit square so that the smallest area of the(38)triangles formed by them is maximal.Symbolic computations are employed to reduce the problem into a nonlinear programming problem and find its optimal solution.All computations are done using Maple.展开更多
The problem of computing the greatest common divisor（GCD） of multivariate polynomials, as one of the most important tasks of computer algebra and symbolic computation in more general scope, has been studied extensiv...The problem of computing the greatest common divisor（GCD） of multivariate polynomials, as one of the most important tasks of computer algebra and symbolic computation in more general scope, has been studied extensively since the beginning of the interdisciplinary of mathematics with computer science. For many real applications such as digital image restoration and enhancement,robust control theory of nonlinear systems, L1-norm convex optimization in compressed sensing techniques, as well as algebraic decoding of Reed-Solomon and BCH codes, the concept of sparse GCD plays a core role where only the greatest common divisors with much fewer terms than the original polynomials are of interest due to the nature of problems or data structures. This paper presents two methods via multivariate polynomial interpolation which are based on the variation of Zippel＇s method and Ben-Or/Tiwari algorithm, respectively. To reduce computational complexity, probabilistic techniques and randomization are employed to deal with univariate GCD computation and univariate polynomial interpolation. The authors demonstrate the practical performance of our algorithms on a significant body of examples. The implemented experiment illustrates that our algorithms are efficient for a quite wide range of input.展开更多
基金supported in part by the National Natural Science Foundation of China under Grant Nos.10901055,61021004,91118007by NKBRPC 2011CB302802,2011CB70690by the Fundamental Research Funds for the Central Universities under Grant No.78210043
文摘This paper presents a hybrid symbolic-numeric algorithm to compute ranking functions for establishing the termination of loop programs with polynomial guards and polynomial assignments.The authors first transform the problem into a parameterized polynomial optimization problem,and obtain a numerical ranking function using polynomial sum-of-squares relaxation via semidefinite programming(SDP).A rational vector recovery algorithm is deployed to recover a rational polynomial from the numerical ranking function,and some symbolic computation techniques are used to certify that this polynomial is an exact ranking function of the loop programs.At last,the authors demonstrate on some polynomial loop programs from the literature that our algorithm successfully yields nonlinear ranking functions with rational coefficients.
基金supported in part by the National Natural Science Foundation of China under Grant Nos.11471209,61321064 and 61361136002the Innovation Program of Shanghai Municipal Education Commission under Grant No.14ZZ046
文摘It is well known that resultant elimination is an effective method of solving multivariate polynomial equations. In this paper, instead of computing the target resultants via variable by variable elimination, the authors combine multivariate implicit equation interpolation and multivariate resultant elimination to compute the reduced resultants, in which the technique of multivariate implicit equation interpolation is achieved by some high probability algorithms on multivariate polynomial interpolation and univariate rational function interpolation. As an application of resultant elimination, the authors illustrate the proposed algorithm on three well-known unsolved combinatorial geometric optimization problems. The experiments show that the proposed approach of resultant elimination is more efficient than some existing resultant elimination methods on these difficult problems.
基金Supported by the National Natural Science Foundation of China (Grant Nos. 60572056, 60528007, 60334020, 60204006, 10471044, and 10372002)the National Key Basic Research and Development Program (Grant Nos. 2005CB321902, 2004CB318003, 2002CB312200)+1 种基金the Overseas Outstanding Young Researcher Foundation of Chinese Academy of Sciencesthe Program of National Key Laboratory of Intelligent Technology and Systems of Tsinghua University
文摘The well-known Generalized Champagne Problem on simultaneous stabilization of linear systems is solved by using complex analysis and Blonders technique. We give a complete answer to the open problem proposed by Patel et al., which automatically includes the solution to the original Champagne Problem. Based on the recent development in automated inequality-type theorem proving, a new stabilizing controller design method is established. Our numerical examples significantly improve the relevant results in the literature.
基金supported by the National Basic Research Program of China (2010CB945401)the National Natural Science Foundation of China (31240038, 31171264, 31071162, 31000590)the Science and Technology Commission of Shanghai Municipality (11DZ2260300)
文摘Transcriptome reconstruction is an important application of RNA-Seq,providing critical information for further analysis of transcriptome.Although RNA-Seq offers the potential to identify the whole picture of transcriptome,it still presents special challenges.To handle these difficulties and reconstruct transcriptome as completely as possible,current computational approaches mainly employ two strategies:de novo assembly and genome-guided assembly.In order to find the similarities and differences between them,we firstly chose five representative assemblers belonging to the two classes respectively,and then investigated and compared their algorithm features in theory and real performances in practice.We found that all the methods can be reduced to graph reduction problems,yet they have different conceptual and practical implementations,thus each assembly method has its specific advantages and disadvantages,performing worse than others in certain aspects while outperforming others in anther aspects at the same time.Finally we merged assemblies of the five assemblers and obtained a much better assembly.Additionally we evaluated an assembler using genome-guided de novo assembly approach,and achieved good performance.Based on these results,we suggest that to obtain a comprehensive set of recovered transcripts,it is better to use a combination of de novo assembly and genome-guided assembly.
基金the National Natural Science Foundation of China under Grant Nos.12171159 and 12071282“Digital Silk Road”Shanghai International Joint Lab of Trustworthy Intelligent Software under Grant No.22510750100。
文摘In this work the authors consider the problem of optimally distributing 8 points inside a unit square so that the smallest area of the(38)triangles formed by them is maximal.Symbolic computations are employed to reduce the problem into a nonlinear programming problem and find its optimal solution.All computations are done using Maple.
基金supported by the National Natural Science Foundation of China under Grant Nos.11471209,11561015,and 11301066Guangxi Key Laboratory of Cryptography and Information Security under Grant No.GCIS201615
文摘The problem of computing the greatest common divisor（GCD） of multivariate polynomials, as one of the most important tasks of computer algebra and symbolic computation in more general scope, has been studied extensively since the beginning of the interdisciplinary of mathematics with computer science. For many real applications such as digital image restoration and enhancement,robust control theory of nonlinear systems, L1-norm convex optimization in compressed sensing techniques, as well as algebraic decoding of Reed-Solomon and BCH codes, the concept of sparse GCD plays a core role where only the greatest common divisors with much fewer terms than the original polynomials are of interest due to the nature of problems or data structures. This paper presents two methods via multivariate polynomial interpolation which are based on the variation of Zippel＇s method and Ben-Or/Tiwari algorithm, respectively. To reduce computational complexity, probabilistic techniques and randomization are employed to deal with univariate GCD computation and univariate polynomial interpolation. The authors demonstrate the practical performance of our algorithms on a significant body of examples. The implemented experiment illustrates that our algorithms are efficient for a quite wide range of input.
