Table of Contents
Fetching ...

Method for Verifying Solutions of Sparse Linear Systems with General Coefficients

Takeshi Terao, Katsuhisa Ozaki

TL;DR

This work tackles the problem of verifiable numerical solution for sparse linear systems with general coefficients by introducing a shifted $LDL^T$ decomposition framework to compute a lower bound on the smallest singular value and an upper bound on $\|A^{-1}\|$. It then combines this with an efficient iterative refinement strategy that uses the LDL$^T$ factors of a shifted matrix to produce highly accurate, certified solutions without relying on dense normal equations or dense approximate inverses. The proposed method emphasizes memory efficiency and stability, including equilibrating preconditioning and selective pivoting considerations, and is demonstrated through numerical experiments that compare favorably with existing SPD and LU-based verification approaches. The approach addresses a key open problem in verified numerics for sparse systems by delivering reliable bounds and refinement with practical computational cost, suitable for large-scale problems in scientific computing.

Abstract

This paper proposes a verification method for sparse linear systems $Ax=b$ with general and nonsingular coefficients. A verification method produces the error bound for a given approximate solution. Conventional methods use one of two approaches. One approach is to verify the computed solution of the normal equation $A^TAx=A^Tb$ by exploiting symmetric and positive definiteness; however, the condition number of $A^TA$ is the square of that for $A$. The other approach uses an approximate inverse matrix of the coefficient; however, the approximate inverse may be dense even if $A$ is sparse. Here, we propose a method for the verification of solutions of sparse linear systems based on $LDL^T$ decomposition. The proposed method can reduce the fill-in and is applicable to many problems. Moreover, an efficient iterative refinement method is proposed for obtaining accurate solutions.

Method for Verifying Solutions of Sparse Linear Systems with General Coefficients

TL;DR

This work tackles the problem of verifiable numerical solution for sparse linear systems with general coefficients by introducing a shifted decomposition framework to compute a lower bound on the smallest singular value and an upper bound on . It then combines this with an efficient iterative refinement strategy that uses the LDL factors of a shifted matrix to produce highly accurate, certified solutions without relying on dense normal equations or dense approximate inverses. The proposed method emphasizes memory efficiency and stability, including equilibrating preconditioning and selective pivoting considerations, and is demonstrated through numerical experiments that compare favorably with existing SPD and LU-based verification approaches. The approach addresses a key open problem in verified numerics for sparse systems by delivering reliable bounds and refinement with practical computational cost, suitable for large-scale problems in scientific computing.

Abstract

This paper proposes a verification method for sparse linear systems with general and nonsingular coefficients. A verification method produces the error bound for a given approximate solution. Conventional methods use one of two approaches. One approach is to verify the computed solution of the normal equation by exploiting symmetric and positive definiteness; however, the condition number of is the square of that for . The other approach uses an approximate inverse matrix of the coefficient; however, the approximate inverse may be dense even if is sparse. Here, we propose a method for the verification of solutions of sparse linear systems based on decomposition. The proposed method can reduce the fill-in and is applicable to many problems. Moreover, an efficient iterative refinement method is proposed for obtaining accurate solutions.
Paper Structure (11 sections, 1 theorem, 32 equations, 6 tables, 5 algorithms)

This paper contains 11 sections, 1 theorem, 32 equations, 6 tables, 5 algorithms.

Key Result

Lemma 1

Let $\bar{A}\in\mathbb{R}^{2n\times 2n}, \theta\in\mathbb{R}$, and $\widehat{L},\widehat{D}\in\mathbb{R}^{2n\times 2n}$ be given. If the number of positive (or negative) eigenvalues for $\widehat{D}$ is equal to $n$, it holds that where $\rho\geq \|\bar{A}+\theta I-\widehat{L}\widehat{D}\widehat{L}^T\|$. In particular, when $|\theta|>\rho$, matrix $A$ is nonsingular and is satisfied.

Theorems & Definitions (2)

  • Lemma 1
  • proof