1 citations · 1 across the 8 of their papers we have counts for
8 papers
A Hybrid SMT-NRA Solver: Integrating 2D Cell-Jump-Based Local Search, MCSAT and OpenCAD
Tianyi Ding, Haokun Li, Xinpeng Ni +2
In this paper, we propose a hybrid framework for Satisfiability Modulo the Theory of Nonlinear Real Arithmetic (SMT-NRA for short). First, we introduce a two-dimensional cell-jump…
Local Search for Solving Satisfiability of Polynomial Formulas
Haokun Li, Bican Xia, Tianqi Zhao
Satisfiability Modulo the Theory of Nonlinear Real Arithmetic, SMT(NRA) for short, concerns the satisfiability of polynomial formulas, which are quantifier-free Boolean combination…
Isolating Bounded and Unbounded Real Roots of a Mixed Trigonometric-Polynomial
Rizeng Chen, Haokun Li, Bican Xia +2
Mixed trigonometric-polynomials (MTPs) are functions of the form with . In this paper, an algorithm ``isolating" all the real r…
Square-free Strong Triangular Decomposition of Zero-dimensional Polynomial Systems
Haokun Li, Bican Xia, Tianqi Zhao
Triangular decomposition with different properties has been used for various types of problem solving, e.g. geometry theorem proving, real solution isolation of zero-dimensional po…
Choosing the Variable Ordering for Cylindrical Algebraic Decomposition via Exploiting Chordal Structure
Haokun Li, Bican Xia, Huiying Zhang +1
Cylindrical algebraic decomposition (CAD) plays an important role in the field of real algebraic geometry and many other areas. As is well-known, the choice of variable ordering wh…
Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection
Haokun Li, Bican Xia
A new algorithm for deciding the satisfiability of polynomial formulas over the reals is proposed. The key point of the algorithm is a new projection operator, called sample-cell p…
A New Sparse SOS Decomposition Algorithm Based on Term Sparsity
Jie Wang, Haokun Li, Bican Xia
A new sparse SOS decomposition algorithm is proposed based on a new sparsity pattern, called cross sparsity patterns. The new sparsity pattern focuses on the sparsity of terms and…
Block SOS Decomposition
Haokun Li, Bican Xia
A widely used method for solving SOS (Sum Of Squares) decomposition problem is to reduce it to the problem of semi-definite programs (SDPs) which can be efficiently solved in theor…