arXiv subjects

Haokun Li

Publications and source records attributed to Haokun Li.

23 records · Page 2Linked to original sources

arXiv2021

Choosing the Variable Ordering for Cylindrical Algebraic Decomposition via Exploiting Chordal Structure

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 while computing CAD has a great effect on the time and memory use of the computation as well as the number of sample points computed. In this paper, we indicate that typical CAD algorithms, if executed with respect to a special kind of variable orderings (called "the perfect elimination orderings"), naturally preserve chordality, which is an important property on sparsity of variables. Experimentation suggests that if the associated graph of the polynomial system in question is chordal (\emph{resp.}, is nearly chordal), then a perfect elimination ordering of the associated graph (\emph{resp.}, of a minimal chordal completion of the associated graph) can be a good variable ordering for the CAD computation. That is, by using the perfect elimination orderings, the CAD computation may produce a much smaller full set of projection polynomials than by using other naive variable orderings. More importantly, for the complexity analysis of the CAD computation via a perfect elimination ordering, a so-called $(m,d)$-property of the full set of projection polynomials obtained via such an ordering is given, through which the "size" of this set is characterized. This property indicates that when the corresponding perfect elimination tree has a lower height, the full set of projection polynomials also tends to have a smaller "size". This is well consistent with the experimental results, hence the perfect elimination orderings with lower elimination tree height are further recommended to be used in the CAD projection.

cs.SC↗

arXiv2020

Generative Low-bitwidth Data Free Quantization

Neural network quantization is an effective way to compress deep models and improve their execution latency and energy efficiency, so that they can be deployed on mobile or embedded devices. Existing quantization methods require original data for calibration or fine-tuning to get better performance. However, in many real-world scenarios, the data may not be available due to confidential or private issues, thereby making existing quantization methods not applicable. Moreover, due to the absence of original data, the recently developed generative adversarial networks (GANs) cannot be applied to generate data. Although the full-precision model may contain rich data information, such information alone is hard to exploit for recovering the original data or generating new meaningful data. In this paper, we investigate a simple-yet-effective method called Generative Low-bitwidth Data Free Quantization (GDFQ) to remove the data dependence burden. Specifically, we propose a knowledge matching generator to produce meaningful fake data by exploiting classification boundary knowledge and distribution information in the pre-trained model. With the help of generated data, we can quantize a model by learning knowledge from the pre-trained model. Extensive experiments on three data sets demonstrate the effectiveness of our method. More critically, our method achieves much higher accuracy on 4-bit quantization than the existing data free quantization method. Code is available at https://github.com/xushoukai/GDFQ.

cs.CV↗

arXiv2020

Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection

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 projection operator, custom-made for Conflict-Driven Clause Learning (CDCL)-style search. Although the new operator is also a CAD (Cylindrical Algebraic Decomposition)-like projection operator which computes the cell (not necessarily cylindrical) containing a given sample such that each polynomial from the problem is sign-invariant on the cell, it is of singly exponential time complexity. The sample-cell projection operator can efficiently guide CDCL-style search away from conflicting states. Experiments show the effectiveness of the new algorithm.

cs.LO↗

arXiv2019

A New Sparse SOS Decomposition Algorithm Based on Term Sparsity

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 thus is different from the well-known correlative sparsity pattern which focuses on the sparsity of variables though the sparse SOS decomposition algorithms based on these two sparsity patterns both take use of chordal extensions/chordal decompositions. Moreover, it is proved that the SOS decomposition obtained by the new sparsity pattern is always a refinement of the block-diagonalization obtained by the sign-symmetry method. %Because the new sparsity pattern covers more sparse polynomials than correlative sparsity pattern, Various experiments show that the new algorithm dramatically saves the computational cost compared to existing tools and can handle some really huge polynomials.

math.OC↗

arXiv2018

Block SOS Decomposition

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 theory. In practice, although many SDP solvers can work out some problems of big scale, the efficiency and reliability of such method decrease greatly while the input size increases. Recently, by exploiting the sparsity of the input SOS decomposition problem, some preprocessing algorithms were proposed [5,17], which first divide the input problem satisfying special definitions or properties into smaller SDP problems and then pass the smaller ones to SDP solvers to obtain reliable results efficiently. A natural question is that to what extent the above mentioned preprocessing algorithms work. That is, how many polynomials satisfying those definitions or properties are there in the SOS polynomials? In this paper, we define a concept of block SOS decomposable polynomials which is a generalization of those special classes in [5] and [17]. Roughly speaking, it is a class of polynomials whose SOS decomposition problem can be transformed into smaller ones (in other words, the corresponding SDP matrices can be block-diagnolized) by considering their supports only (coefficients are not considered). Then we prove that the set of block SOS decomposable polynomials has measure zero in the set of SOS polynomials. That means if we only consider supports (not with coefficients) of polynomials, such algorithms decreasing the size of SDPs for those SDP-based SOS solvers can only work on very few polynomials. As a result, this shows that the SOS decomposition problems that can be optimized by the above mentioned preprocessing algorithms are very few.

cs.SC↗