Related papers: A Note on Semi-Algebraic Proofs and Gaussian Elimi…
We demonstrate a family of propositional formulas in conjunctive normal form so that a formula of size $N$ requires size $2^{\Omega(\sqrt[7]{N/logN})}$ to refute using the tree-like OBDD refutation system of Atserias, Kolaitis and Vardi…
We develop a new tool, namely polynomial and linear algebraic methods, for studying systems of word equations. We illustrate its usefulness by giving essentially simpler proofs of several hard problems. At the same time we prove extensions…
In order to verify programs or hybrid systems, one often needs to prove that certain formulas are unsatisfiable. In this paper, we consider conjunctions of polynomial inequalities over the reals. Classical algorithms for deciding these not…
In this paper we consider the problem of how to computationally test whether a matrix inequality is positive semidefinite on a semialgebraic set. We propose a family of sufficient conditions using the theory of matrix Positivstellensatz…
We provide a necessary and sufficient condition for existence of Gaussian cubature formulas. It consists of checking whether some overdetermined linear system has a solution and so complements Mysovskikh's theorem which requires computing…
Semi-algebraic proof systems such as sum-of-squares (SoS) have attracted a lot of attention recently due to their relation to approximation algorithms: constant degree semi-algebraic proofs lead to conjecturally optimal polynomial-time…
Checking whether a system of linear equations is consistent is a basic computational problem with ubiquitous applications. When dealing with inconsistent systems, one may seek an assignment that minimizes the number of unsatisfied…
We analyse how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional, algebraic, and semi-algebraic proof systems, the classical constructions of…
Proofs of the fundamental theorem of algebra can be divided up into three groups according to the techniques involved: proofs that rely on real or complex analysis, algebraic proofs, and topological proofs. Algebraic proofs make use of the…
Proving super-polynomial lower bounds on the size of proofs of unsatisfiability of Boolean formulas using resolution over parities is an outstanding problem that has received a lot of attention after its introduction by Raz and Tzamaret…
Consider a semi-algebraic set A in R^d constructed from the sets which are determined by inequalities p_i(x)>0, p_i(x)\ge 0, or p_i(x)=0 for a given list of polynomials p_1,...,p_m. We prove several statements that fit into the following…
We introduce new semi-algebraic proof systems for Quantified Boolean Formulas (QBF) analogous to the propositional systems Nullstellensatz, Sherali-Adams and Sum-of-Squares. We transfer to this setting techniques both from the QBF…
We show that if a system of degree-$k$ polynomial constraints on~$n$ Boolean variables has a Sums-of-Squares (SOS) proof of unsatisfiability with at most~$s$ many monomials, then it also has one whose degree is of the order of the square…
We study -- within the framework of propositional proof complexity -- the problem of certifying unsatisfiability of CNF formulas under the promise that any satisfiable formula has many satisfying assignments, where ``many'' stands for an…
We present an algorithm to solve a system of diagonal polynomial equations over finite fields when the number of variables is greater than some fixed polynomial of the number of equations whose degree depends only on the degree of the…
We consider general Gaussian latent tree models in which the observed variables are not restricted to be leaves of the tree. Extending related recent work, we give a full semi-algebraic description of the set of covariance matrices of any…
We address combinatorial problems that can be formulated as minimization of a partially separable function of discrete variables (energy minimization in graphical models, weighted constraint satisfaction, pseudo-Boolean optimization, 0-1…
For a finite set $\cal F$ of polynomials over fixed finite prime field of size $p$ containing all polynomials $x^2 - x$ a Nullstellensatz proof of the unsolvability of the system $$ f = 0\ ,\ \mbox{ all } f \in {\cal F} $$ in the field is a…
In this paper, we present and analyze methods for solving a system of linear equations over idempotent semifields. The first method is based on the pseudo-inverse of the system matrix. We then present a specific version of Cramer's rule…
The purpose of this note is to survey a methodology to solve systems of polynomial equations and inequalities. The techniques we discuss use the algebra of multivariate polynomials with coefficients over a field to create large-scale linear…