arXiv subjects

Harshit J Motwani

Publications and source records attributed to Harshit J Motwani.

5 recordsLinked to original sources

arXiv2024

Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization

The problem of checking satisfiability of linear real arithmetic (LRA) and non-linear real arithmetic (NRA) formulas has broad applications, in particular, they are at the heart of logic-related applications such as logic for artificial intelligence, program analysis, etc. While there has been much work on checking satisfiability of unquantified LRA and NRA formulas, the problem of checking satisfiability of quantified LRA and NRA formulas remains a significant challenge. The main bottleneck in the existing methods is a computationally expensive quantifier elimination step. In this work, we propose a novel method for efficient quantifier elimination in quantified LRA and NRA formulas. We propose a template-based Skolemization approach, where we automatically synthesize linear/polynomial Skolem functions in order to eliminate quantifiers in the formula. The key technical ingredients in our approach are Positivstellensätze theorems from algebraic geometry, which allow for an efficient manipulation of polynomial inequalities. Our method offers a range of appealing theoretical properties combined with a strong practical performance. On the theory side, our method is sound, semi-complete, and runs in subexponential time and polynomial space, as opposed to existing sound and complete quantifier elimination methods that run in doubly-exponential time and at least exponential space. On the practical side, our experiments show superior performance compared to state-of-the-art SMT solvers in terms of the number of solved instances and runtime, both on LRA and on NRA benchmarks.

cs.LO↗

arXiv2023

Global Rigidity of Line Constrained Frameworks

We consider the global rigidity problem for bar-joint frameworks where each vertex is constrained to lie on a particular line in $\mathbb R^d$. In our setting we allow multiple vertices to be constrained to the same line. Under a mild assumption on the given set of lines we give a complete combinatorial characterisation of graphs that are generically globally rigid in this setting. This gives a $d$-dimensional extension of the well-known combinatorial characterisation of 1-dimensional global rigidity.

math.CO↗

arXiv2022

The Linear Span of Uniform Matrix Product States

The variety of uniform matrix product states arises both in algebraic geometry as a natural generalization of the Veronese variety, and in quantum many-body physics as a model for a translation-invariant system of sites placed on a ring. Using methods from linear algebra, representation theory, and invariant theory of matrices, we study the linear span of this variety.

math.AG↗

arXiv2022

Matroid stratifications of hypergraph varieties, their realization spaces, and discrete conditional independence models

We study varieties associated to hypergraphs from the point of view of projective geometry and matroid theory. We describe their decompositions into matroid varieties, which may be reducible and can have arbitrary singularities by the Mnëv--Sturmfels universality theorem. We focus on various families of hypergraph varieties for which we explicitly compute an irredundant irreducible decomposition. Our main findings in this direction are threefold: (1) we describe minimal matroids of such hypergraphs; (2) we prove that the varieties of these matroids are irreducible and their union is the hypergraph variety; and (3) we show that every such matroid is realizable over real numbers. As corollaries, we give conceptual decompositions of various, previously-studied, varieties associated with graphs, hypergraphs, and adjacent minors of generic matrices. In particular, our decomposition strategy gives immediate matroid interpretations of the irreducible components of multiple families of varieties associated to conditional independence (CI) models in statistical theory and unravels their symmetric structures which hugely simplifies the computations.

math.CO↗

arXiv2022

Template-based Program Synthesis using Stellensätze

Template-based synthesis, also known as sketching, is a localized approach to program synthesis in which the programmer provides not only a specification, but also a high-level ``sketch'' of the program. The sketch is basically a partial program that models the general intuition of the programmer, while leaving the low-level details as unimplemented ``holes''. The role of the synthesis engine is then to fill in these holes such that the completed program satisfies the desired specification. In this work, we focus on template-based synthesis of polynomial imperative programs with real variables, i.e.~imperative programs in which all expressions appearing in assignments, conditions and guards are polynomials over program variables. While this problem can be solved in a sound and complete manner by a reduction to the first-order theory of the reals, the resulting formulas will contain a quantifier alternation and are extremely hard for modern SMT solvers, even when considering toy programs with a handful of lines. Moreover, the classical algorithms for quantifier elimination are notoriously unscalable and not at all applicable to this use-case. In contrast, our main contribution is an algorithm, based on several well-known theorems in polyhedral and real algebraic geometry, namely Putinar's Positivstellensatz, the Real Nullstellensatz, Handelman's Theorem and Farkas' Lemma, which sidesteps the quantifier elimination difficulty and reduces the problem directly to Quadratic Programming (QP). Alternatively, one can view our algorithm as an efficient way of eliminating quantifiers in the particular formulas that appear in the synthesis problem. The resulting QP instances can then be handled quite easily by SMT solvers. Notably, our reduction to QP is sound and semi-complete, i.e.~it is complete if polynomials of a sufficiently high degree are used in the templates...

cs.PL↗