Runge-Kutta interpolants based on values from two successive integration steps

New interpolants of the explicit Runge-Kutta method for the initial value problem are proposed. These interpolants are based on values of the solution and its derivative from two successive integration steps. In this paper, three interpolants withO(h ⁶) local error (l.e.), for the fifth order solution, of the methods Fehlberg 4(5) (RKF 4(5)), Dormand and Prince 5(4) (RKDP 5(4)) and Verner 5(6) (RKV 5(6)) without extra cost are derived. An interpolant withO(h ⁷) (l.e.) for the sixth order solution of the Verner's method with only one extra function evaluation per integration step is also constructed. The above advantages are obtained without any cost in the magnitude of the error.     

Interpolant Learning and Reuse in SAT-Based Model Checking

Bounded Model Checking (BMC) is one of the most paradigmatic practical applications of Boolean Satisfiability (SAT). The utilization of SAT in model checking has allowed significant performance gains and, as a consequence, a large number of commercial verification tools now include SAT-based model checkers. Recent work has provided SAT-based BMC with completeness conditions, and this is generally referred to as unbounded model checking (UMC). Among the existing approaches for SAT-based UMC, the utilization of interpolants is among the most effective. Despite their success, interpolants have only been used for identifying a fixed point of the set of reachable states. This paper extends the utilization of interpolants in SAT-based model checking. This is achieved by observing that, under reasonable assumptions, interpolants can be reused, i.e. computed interpolants can be reused at later stages of the model checking process. The paper develops conditions for validity of interpolant reuse. In addition, the paper outlines a new fixed point condition, alternative to the existing interpolant-based fixed point condition. Preliminary practical experience on interpolant learning and reuse is reported.     

G2 Surface Interpolation Over General Topology Curve Networks

The basic idea of curve network‐based design is to construct smoothly connected surface patches, that interpolate boundaries and cross‐derivatives extracted from the curve network. While the majority of applications demands only tangent plane (G¹) continuity between the adjacent patches, curvature continuous connections (G²) may also be required. Examples include special curve network configurations with supplemented internal edges, “master‐slave” curvature constraints, and general topology surface approximations over meshes. The first step is to assign optimal surface curvatures to the nodes of the curve network; we discuss different optimization procedures for various types of nodes. Then interpolant surfaces called parabolic ribbons are created along the patch boundaries, which carry first and second derivative constraints. Our construction guarantees that the neighboring ribbons, and thus the respective transfinite patches, will be G² continuous. We extend Gregory's multi‐sided surface scheme in order to handle parabolic ribbons, involving the blending functions, and a new sweepline parameterization. A few simple examples conclude the paper.     

Smooth interpolation over hypercubes

Multivariate interpolation problems, which occur often in scientific research, can sometimes be approached using Coons' patches. Coons' patches are smooth, local interpolants to lower dimensional data sets. (For example, they interpolate curves of data when considering 3-dimensional problems.) However, they do not interpolate as desired unless all the mixed partial derivatives, the ‘twists’, are equal. The twists are not equal in many cases of practical importance, such as for wire frame data. Gregory (1983) has developed a compatibly corrected Coons' patch for 3-dimensional surfaces. We generalize this interpolant, ‘Gregory's square’, to the case of functions of n variables. The interpolant we propose is built up inductively from one to n-dimensions, requiring, at each step, only one additional term to be defined. This is the key to the whole process and involves the definition of a general ‘twist operator’.     

Craig Interpolation with Clausal First-Order Tableaux

We develop foundations for computing Craig-Lyndon interpolants of two given formulas with first-order theorem provers that construct clausal tableaux. Provers that can be understood in this way include efficient machine-oriented systems based on calculi of two families: goal-oriented such as model elimination and the connection method, and bottom-up such as the hypertableau calculus. We present the first interpolation method for first-order proofs represented by closed tableaux that proceeds in two stages, similar to known interpolation methods for resolution proofs. The first stage is an induction on the tableau structure, which is sufficient to compute propositional interpolants. We show that this can linearly simulate different prominent propositional interpolation methods that operate by an induction on a resolution deduction tree. In the second stage, interpolant lifting, quantified variables that replace certain terms (constants and compound terms) by variables are introduced. We justify the correctness of interpolant lifting (for the case without built-in equality) abstractly on the basis of Herbrand’s theorem and for a different characterization of the formulas to be lifted than in the literature. In addition, we discuss various subtle aspects that are relevant for the investigation and practical realization of first-order interpolation based on clausal tableaux.

     

Identification of spatial PH quintic Hermite interpolants with near-optimal shape measures

The problem of specifying the two free parameters that arise in spatial Pythagorean-hodograph (PH) quintic interpolants to given first-order Hermite data is addressed. Conditions on the data that identify when the “ordinary” cubic interpolant becomes a PH curve are formulated, since it is desired that the selection procedure should reproduce such curves whenever possible. Moreover, it is shown that the arc length of the interpolants depends on only one of the parameters, and that four (general) helical PH quintic interpolants always exist, corresponding to extrema of the arc length. Motivated by the desire to improve the fairness of interpolants to general data at reasonable computational cost, three selection criteria are proposed. The first criterion is based on minimizing a bivariate function that measures how “close” the PH quintic interpolants are to a PH cubic. For the second criterion, one of the parameters is fixed by first selecting interpolants of extremal arc length, and the other parameter is then determined by minimizing the distance measure of the first method, considered as a univariate function. The third method employs a heuristic but efficient procedure to select one parameter, suggested by the circumstances in which the “ordinary” cubic interpolant is a PH curve, and the other parameter is then determined as in the second method. After presenting the theory underlying these three methods, a comparison of empirical results from their implementation is described, and recommendations for their use in practical design applications are made.     

Parallel Computation of the Topology of Level Sets

This paper introduces two efficient algorithms that compute the Contour Tree of a three-dimensional scalar field F and its augmented version with the Betti numbers of each isosurface. The Contour Tree is a fundamental data structure in scientific visualization that is used to pre-process the domain mesh to allow optimal computation of isosurfaces with minimal overhead storage. The Contour Tree can also be used to build user interfaces reporting the complete topological characterization of a scalar field, as shown in Figure~\ref{fig:top}. Data exploration time is reduced since the user understands the evolution of level set components with changing isovalue. The Augmented Contour Tree provides even more accurate information segmenting the range space of the scalar field into regions of invariant topology. The exploration time for a single isosurface is also improved since its genus is known in advance. Our first new algorithm augments any given Contour Tree with the Betti numbers of all possible corresponding isocontours in linear time with the size of the tree. Moreover, we show how to extend the scheme introduced in [3] with the Betti number computation without increasing its complexity. Thus, we improve on the time complexity in our previous approach from O(m log m) to O(n log n + m), where m is the number of cells and n is the number of vertices in the domain of F. Our second contribution is a new divide-and-conquer algorithm that computes the Augmented Contour Tree with improved efficiency. The approach computes the output Contour Tree by merging two intermediate Contour Trees and is independent of the interpolant. In this way we confine any knowledge regarding a specific interpolant to an independent function that computes the tree for a single cell. We have implemented this function for the trilinear interpolant and plan to replace it with higher-order interpolants when needed. The time complexity is O(n + t log n), where t is the number of critical points of F. For the first time we can compute the Contour Tree in linear time in many practical cases where t = O(n^1–). We report the running times for a parallel implementation, showing good scalability with the number of processors.     

Curve Interpolation with Arbitrary End Derivatives

An algorithm for interpolating data points with end derivative constraints is presented. The interpolating curve passes through the given points and at the same time assumes the derivatives specified. For degree p interpolation, up to p−1 derivatives may be specified, resulting in C ^p−1 continuous curve interpolants. The method is useful to piece individual curve segments together or to create closed curves with various degrees of smoothness.     

Recent advances in the construction of polygonal finite element interpolants

Summary This paper is an overview of recent developments in the construction of finite element interpolants, which areC ⁰-conforming on polygonal domains. In 1975, Wachspress proposed a general method for constructing finite element shape functions on convex polygons. Only recently has renewed interest in such interpolants surfaced in various disciplines including: geometric modeling, computer graphics, and finite element computations. This survey focuses specifically on polygonal shape functions that satisfy the properties of barycentric coordinates: (a) form a partition of unity, and are non-negative; (b) interpolate nodal data (Kronecker-delta property), (c) are linearly complete or satisfy linear precision, and (d) are smooth within the domain. We compare and contrast the construction and properties of various polygonal interpolants—Wachspress basis functions, mean value coordinates, metric coordinate method, natural neighbor-based coordinates, and maximum entropy shape functions. Numerical integration of the Galerkin weak form on polygonal domains is discussed, and the performance of these polygonal interpolants on the patch test is studied.     

On the interpolation of concentric curvature elements

A convex G² Hermite interpolation problem of concentric curvature elements is considered in this paper. It is first proved that there is no spiral arc solution with turning angle less than or equal to π and then, that any convex solution admits at least two vertices. The curvature and the evolute profiles of such an interpolant are analyzed. In particular, conditions for the existence of a G² convex interpolant with prescribed extremal curvatures are given.     

On the approximation order of a space data-dependent PH quintic Hermite interpolation scheme

Dealing with Pythagorean Hodograph quintic Hermite interpolation in the space, we deepen the analysis of the so-called CC criterion proposed in Farouki et al. (2008) for fixing the two free angular parameters characterizing the set of possible solutions, which remarkably influence the shape of the chosen interpolant. Such criterion is easy to implement, guarantees the reproduction of the standard cubic Hermite interpolant when it is a PH curve and usually allows the selection of interpolants with good shape. Here we first rigorously prove that the PH interpolant it selects doesn?t depend on the unit pure vector chosen for representing its hodograph in quaternion form. Then we evaluate the corresponding interpolation scheme from a theoretical point of view, proving with the help of symbolic computation that it has fourth approximation order. A selection of experiments related to the spline implementation of the method confirms our analysis.     

Uniform convergence of interpolation by cubic splines

For a sequence of meshes on [0, 1] sufficient conditions are given to obtain uniform convergence of cubic spline interpolants for continous functions respectively for the third derivatives of cubic spline interpolants for functions fromC ³ [0, 1].     

Using linear algebra in decomposition of Farkas interpolants

The use of propositional logic and systems of linear inequalities over reals is a common means to model software for formal verification. Craig interpolants constitute a central building block in this setting for over-approximating reachable states, e.g. as candidates for inductive loop invariants. Interpolants for a linear system can be efficiently computed from a Simplex refutation by applying the Farkas’ lemma. However, these interpolants do not always suit the verification task—in the worst case, they can even prevent the verification algorithm from converging. This work introduces the decomposed interpolants, a fundamental extension of the Farkas interpolants, obtained by identifying and separating independent components from the interpolant structure, using methods from linear algebra. We also present an efficient polynomial algorithm to compute decomposed interpolants and analyse its properties. We experimentally show that the use of decomposed interpolants in model checking results in immediate convergence on instances where state-of-the-art approaches diverge. Moreover, since being based on the efficient Simplex method, the approach is very competitive in general.

     

Two-grid quasilinearization approach to ODEs with applications to model problems in physics and mechanics

In this paper we propose a two-grid quasilinearization method for solving high order nonlinear differential equations. In the first step, the nonlinear boundary value problem is discretized on a coarse grid of size H. In the second step, the nonlinear problem is linearized around an interpolant of the computed solution (which serves as an initial guess of the quasilinearization process) at the first step. Thus, the linear problem is solved on a fine mesh of size h, h?H. On this base we develop two-grid iteration algorithms, that achieve optimal accuracy as long as the mesh size satisfies h=O(Hr²), r=1,2,… , where r is the rth Newton's iteration for the linearized differential problem. Numerical experiments show that a large class of NODEs, including the Fisher-Kolmogorov, Blasius and Emden-Fowler equations solving with two-grid algorithm will not be much more difficult than solving the corresponding linearized equations and at the same time with significant economy of the computations.     

How conservative is frozen-time interpolation?

It is shown in this note that for SISO systems under l² disturbances, when data commute approximately with the shift, the optimal interpolation (over all linear time-varying interpolants) can be approximated by the supremum of the frozen-time Hankel norms. This confirms the intuition that the frozen-time constructed optimal or suboptimal interpolants are in fact nearly optimal when data vary slowly.     

Generating Symbolic Interpolants for Scattered Data with Normal Vectors

Algorithms to generate a triangular or a quadrilateral interpolant with G1-continuity are given in this paper for arbitrary scattered data with associated normal vectors over a prescribed triangular or quadrilateral decomposition. The interpolants are constructed with a general method to generate surfaces from moving Bezier curves under geometric constraints. With the algorithm, we may obtain interpolants in complete symbolic parametric forms, leading to a fast computation of the interpolant. A dynamic interpolation solid modelling software package DISM is implemented based on the algorithm which can be used to generate and manipulate solid objects in an interactive way.     

平面三次PH曲线偶C1Hermite插值解的构造和形状分析

一般情况下,三次PH曲线偶的C^1 Hemite插值问题有四个不同的解。在这四个解中,只有一条曲线能很好地满足几何设计的要求。已有的插值算法都是依赖于构造出所有四个解,利用绝对旋转指标或弹性弯曲能量来找出这条“好”的插值曲线。本文提出一种新的方法以区分这些解,即用由三次PH曲线偶和惟一经典三次插值曲线的速端曲线形成的闭环的弯曲数来区分。对于“合理”的Hemite数据,本文还给出了不需计算和比较所有的四个解便可直接构造“好”的三次PH曲线偶的方法。     

Near conserving energy numerical schemes for two-dimensional coupled seismic wave equations

Two-dimensional coupled seismic waves, satisfying the equations of linear isotropic elasticity, on a rectangular domain with initial conditions and periodic boundary conditions, are considered. A quantity conserved by the solution of the continuous problem is used to check the numerical solution of the problem. Second order spatial derivatives, in the $x$ direction, in the $y$ direction and mixed derivative, are approximated by finite differences on a uniform grid. The ordinary second order in time system obtained is transformed into a first order in time system in the displacement and velocity vectors. For the time integration of this system, second order and fourth order exponential splitting methods, which are geometric integrators, are proposed. These explicit splitting methods are not unconditionally stable and the stability condition for time step and space step ratio is deduced. Numerical experiments displaying the good behavior in the long time integration and the efficiency of the numerical solution are provided.     

Accuracy improvement of a multistep splitting method for nonlinear viscous wave equations

This paper focuses on a multistep splitting method for a class of nonlinear viscous equations in two spaces, which uses second-order backward differentiation formula (BDF2) combined with approximation factorization for time integration, and second-order centred difference approximation to second derivatives for spatial discretization. By the discrete energy method, it is shown that this splitting method can attain second-order accuracy in both time and space with respect to the discrete L²- and H¹-norms. Moreover, for improving computational efficiency, we introduce a Richardson extrapolation method and obtain extrapolation solution of order four in both time and space. Numerical experiments illustrate the accuracy and performance of our algorithms.     

Shape preserving surface reconstruction using locally anisotropic radial basis function interpolants

In this paper we deal with the problem of reconstructing surfaces from unorganized sets of points, while capturing the significant geometry details of the modelled surface, such as edges, flat regions, and corners. This is obtained by exploiting the good approximation capabilities of the radial basis functions (RBF), the local nature of the method proposed in [1], and introducing information on shape features and data anisotropies detected from the given surface points.The result is a shape-preserving reconstruction, given by a weighted combination of locally aniso tropic interpolants. For each local interpolant the anisotropy is obtained by replacing the Euclidean norm with a suitable metric which takes into account the local distribution of the points. Thus hyperellipsoid basis functions, named anisotropic RBFs, are defined. Results from the application of the method to the reconstruction of object surfaces in ℝ³ are presented, confirming the effectiveness of the approach.