No Arabic abstract
We study the (hereditary) discrepancy of definable set systems, which is a natural measure for their inherent complexity and approximability. We establish a strong connection between the hereditary discrepancy and quantifier elimination over signatures with only unary relation and function symbols. We prove that set systems definable in theories (over such signatures) with quantifier elimination have constant hereditary discrepancy. We derive that set systems definable in bounded expansion classes, which are very general classes of uniformly sparse graphs, have bounded hereditary discrepancy. We also derive that nowhere dense classes, which are more general than bounded expansion classes, in general do not admit quantifier elimination over a signature extended by an arbitrary number of unary function symbols. We show that the set systems on a ground set $U$ definable on a monotone nowhere dense class of graphs $mathscr C$ have hereditary discrepancy at most $|U|^{c}$ (for some~$c<1/2$) and that, on the contrary, for every monotone somewhere dense class $mathscr C$ and for every positive integer $d$ there is a set system of $d$-tuples definable in $mathscr C$ with discrepancy $Omega(|U|^{1/2})$. We further prove that if $mathscr C$ is a class of graphs with bounded expansion and $phi(bar x;bar y)$ is a first-order formula, then we can compute in polynomial time, for an input graph $Ginmathscr C$, a mapping $chi:V(G)^{|bar x|}rightarrow{-1,1}$ witnessing the boundedness of the discrepancy of the set-system defined by~$phi$, an $varepsilon$-net of size $mathcal{O}(1/varepsilon)$, and an $varepsilon$-approximation of size $mathcal{O}(1/varepsilon)$.
The satisfiability problem in real closed fields is decidable. In the context of satisfiability modulo theories, the problem restricted to conjunctive sets of literals, that is, sets of polynomial constraints, is of particular importance. One of the central problems is the computation of good explanations of the unsatisfiability of such sets, i.e. obtaining a small subset of the input constraints whose conjunction is already unsatisfiable. We adapt two commonly used real quantifier elimination methods, cylindrical algebraic decomposition and virtual substitution, to provide such conflict sets and demonstrate the performance of our method in practice.
The only C*-algebras that admit elimination of quantifiers in continuous logic are $mathbb{C}, mathbb{C}^2$, $C($Cantor space$)$ and $M_2(mathbb{C})$. We also prove that the theory of C*-algebras does not have model companion and show that the theory of $M_n(mathcal {O_{n+1}})$ is not $forallexists$-axiomatizable for any $ngeq 2$.
We show that it is possible to use Bondy-Chvatal closure to design an FPT algorithm that decides whether or not it is possible to cover vertices of an input graph by at most k vertex disjoint paths in the complement of the input graph. More precisely, we show that if a graph has tree-width at most w and its complement is closed under Bondy-Chvatal closure, then it is possible to bound neighborhood diversity of the complement by a function of w only. A simpler proof where tree-depth is used instead of tree-width is also presented.
What is the maximum number of copies of a fixed forest $T$ in an $n$-vertex graph in a graph class $mathcal{G}$ as $nto infty$? We answer this question for a variety of sparse graph classes $mathcal{G}$. In particular, we show that the answer is $Theta(n^{alpha_d(T)})$ where $alpha_d(T)$ is the size of the largest stable set in the subforest of $T$ induced by the vertices of degree at most $d$, for some integer $d$ that depends on $mathcal{G}$. For example, when $mathcal{G}$ is the class of $k$-degenerate graphs then $d=k$; when $mathcal{G}$ is the class of graphs containing no $K_{s,t}$-minor ($tgeq s$) then $d=s-1$; and when $mathcal{G}$ is the class of $k$-planar graphs then $d=2$. All these results are in fact consequences of a single lemma in terms of a finite set of excluded subgraphs.
Quantifier elimination over the reals is a central problem in computational real algebraic geometry, polynomial system solving and symbolic computation. Given a semi-algebraic formula (whose atoms are polynomial constraints) with quantifiers on some variables, it consists in computing a logically equivalent formula involving only unquantified variables. When there is no alternation of quantifiers, one has a one block quantifier elimination problem. This paper studies a variant of the one block quantifier elimination in which we compute an almost equivalent formula of the input. We design a new probabilistic efficient algorithm for solving this variant when the input is a system of polynomial equations satisfying some regularity assumptions. When the input is generic, involves $s$ polynomials of degree bounded by $D$ with $n$ quantified variables and $t$ unquantified ones, we prove that this algorithm outputs semi-algebraic formulas of degree bounded by $mathcal{D}$ using $O {widetilde{~}}left ((n-s+1) 8^{t} mathcal{D}^{3t+2} binom{t+mathcal{D}}{t} right )$ arithmetic operations in the ground field where $mathcal{D} = 2(n+s) D^s(D-1)^{n-s+1} binom{n}{s}$. In practice, it allows us to solve quantifier elimination problems which are out of reach of the state-of-the-art (up to $8$ variables).