-
On the algebraic proof complexity of Tensor Isomorphism
Authors:
Nicola Galesi,
Joshua A. Grochow,
Toniann Pitassi,
Adrian She
Abstract:
The Tensor Isomorphism problem (TI) has recently emerged as having connections to multiple areas of research within complexity and beyond, but the current best upper bound is essentially the brute force algorithm. Being an algebraic problem, TI (or rather, proving that two tensors are non-isomorphic) lends itself very naturally to algebraic and semi-algebraic proof systems, such as the Polynomial…
▽ More
The Tensor Isomorphism problem (TI) has recently emerged as having connections to multiple areas of research within complexity and beyond, but the current best upper bound is essentially the brute force algorithm. Being an algebraic problem, TI (or rather, proving that two tensors are non-isomorphic) lends itself very naturally to algebraic and semi-algebraic proof systems, such as the Polynomial Calculus (PC) and Sum of Squares (SoS). For its combinatorial cousin Graph Isomorphism, essentially optimal lower bounds are known for approaches based on PC and SoS (Berkholz & Grohe, SODA '17). Our main results are an $Ω(n)$ lower bound on PC degree or SoS degree for Tensor Isomorphism, and a nontrivial upper bound for testing isomorphism of tensors of bounded rank.
We also show that PC cannot perform basic linear algebra in sub-linear degree, such as comparing the rank of two matrices, or deriving $BA=I$ from $AB=I$. As linear algebra is a key tool for understanding tensors, we introduce a strictly stronger proof system, PC+Inv, which allows as derivation rules all substitution instances of the implication $AB=I \rightarrow BA=I$. We conjecture that even PC+Inv cannot solve TI in polynomial time either, but leave open getting lower bounds on PC+Inv for any system of equations, let alone those for TI. We also highlight many other open questions about proof complexity approaches to TI.
△ Less
Submitted 30 May, 2023;
originally announced May 2023.
-
Depth lower bounds in Stabbing Planes for combinatorial principles
Authors:
Stefan Dantchev,
Nicola Galesi,
Abdul Ghani,
Barnaby Martin
Abstract:
Stabbing Planes (also known as Branch and Cut) is a proof system introduced very recently which, informally speaking, extends the DPLL method by branching on integer linear inequalities instead of single variables. The techniques known so far to prove size and depth lower bounds for Stabbing Planes are generalizations of those used for the Cutting Planes proof system. For size lower bounds these a…
▽ More
Stabbing Planes (also known as Branch and Cut) is a proof system introduced very recently which, informally speaking, extends the DPLL method by branching on integer linear inequalities instead of single variables. The techniques known so far to prove size and depth lower bounds for Stabbing Planes are generalizations of those used for the Cutting Planes proof system. For size lower bounds these are established by monotone circuit arguments, while for depth these are found via communication complexity and protection. As such these bounds apply for lifted versions of combinatorial statements. Rank lower bounds for Cutting Planes are also obtained by geometric arguments called protection lemmas.
In this work we introduce two new geometric approaches to prove size/depth lower bounds in Stabbing Planes working for any formula: (1) the antichain method, relying on Sperner's Theorem and (2) the covering method which uses results on essential coverings of the boolean cube by linear polynomials, which in turn relies on Alon's combinatorial Nullenstellensatz.
We demonstrate their use on classes of combinatorial principles such as the Pigeonhole principle, the Tseitin contradictions and the Linear Ordering Principle. By the first method we prove almost linear size lower bounds and optimal logarithmic depth lower bounds for the Pigeonhole principle and analogous lower bounds for the Tseitin contradictions over the complete graph and for the Linear Ordering Principle. By the covering method we obtain a superlinear size lower bound and a logarithmic depth lower bound for Stabbing Planes proof of Tseitin contradictions over a grid graph.
△ Less
Submitted 10 January, 2024; v1 submitted 15 February, 2021;
originally announced February 2021.
-
Counting and localizing defective nodes by Boolean network tomography
Authors:
Nicola Galesi,
Fariba Ranjbar
Abstract:
Identifying defective items in larger sets is a main problem with many applications in real life situations. We consider the problem of localizing defective nodes in networks through an approach based on boolean network tomography (BNT), which is grounded on inferring informations from the boolean outcomes of end-to-end measurements paths. {\em Identifiability} conditions on the set of paths which…
▽ More
Identifying defective items in larger sets is a main problem with many applications in real life situations. We consider the problem of localizing defective nodes in networks through an approach based on boolean network tomography (BNT), which is grounded on inferring informations from the boolean outcomes of end-to-end measurements paths. {\em Identifiability} conditions on the set of paths which guarantee discovering or counting unambiguously the defective nodes are of course very relevant. We investigate old and introduce new identifiability conditions contributing this problem both from a theoretical and applied perspective. (1) What is the precise tradeoff between number of nodes and number of paths such that at most $k$ nodes can be identified unambiguously ? The answer is known only for $k=1$ and we answer the question for any $k$, setting a problem implicitly left open in previous works. (2) We study upper and lower bounds on the number of unambiguously identifiable nodes, introducing new identifiability conditions which strictly imply and are strictly implied by unambiguous identifiability; (3) We use these new conditions on one side to design algorithmic heuristics to count defective nodes in a fine-grained way, on the other side to prove the first complexity hardness results on the problem of identifying defective nodes in networks via BNT. (4) We introduce a random model where we study lower bounds on the number of unambiguously identifiable defective nodes and we use this model to estimate that number on real networks by a maximum likelihood estimate approach
△ Less
Submitted 12 January, 2021;
originally announced January 2021.
-
Proof complexity and the binary encoding of combinatorial principles
Authors:
Stefan Dantchev,
Nicola Galesi,
Abdul Ghani,
Barnaby Martin
Abstract:
We consider Proof Complexity in light of the unusual binary encoding of certain combinatorial principles. We contrast this Proof Complexity with the normal unary encoding in several refutation systems, based on Resolution and Integer Linear Programming. Please consult the article for the full abstract.
We consider Proof Complexity in light of the unusual binary encoding of certain combinatorial principles. We contrast this Proof Complexity with the normal unary encoding in several refutation systems, based on Resolution and Integer Linear Programming. Please consult the article for the full abstract.
△ Less
Submitted 5 April, 2022; v1 submitted 4 August, 2020;
originally announced August 2020.
-
Vertex-Connectivity Measures for Node Failure Identification in Boolean Network Tomography
Authors:
Nicola Galesi,
Fariba Ranjbar,
Michele Zito
Abstract:
In this paper we study the node failure identification problem in undirected graphs by means of Boolean Network Tomography. We argue that vertex connectivity plays a central role. We show tight bounds on the maximal identifiability in a particular class of graphs, the Line of Sight networks. We prove slightly weaker bounds on arbitrary networks. Finally we initiate the study of maximal identifiabi…
▽ More
In this paper we study the node failure identification problem in undirected graphs by means of Boolean Network Tomography. We argue that vertex connectivity plays a central role. We show tight bounds on the maximal identifiability in a particular class of graphs, the Line of Sight networks. We prove slightly weaker bounds on arbitrary networks. Finally we initiate the study of maximal identifiability in random networks. We focus on two models: the classical Erdős-Rényi model, and that of Random Regular graphs. The framework proposed in the paper allows a probabilistic analysis of the identifiability in random networks giving a tradeoff between the number of monitors to place and the maximal identifiability.
△ Less
Submitted 3 July, 2019; v1 submitted 4 December, 2018;
originally announced December 2018.
-
Resolution and the binary encoding of combinatorial principles
Authors:
Stefan Dantchev,
Nicola Galesi,
Barnaby Martin
Abstract:
We investigate the size complexity of proofs in $Res(s)$ -- an extension of Resolution working on $s$-DNFs instead of clauses -- for families of contradictions given in the {\em unusual binary} encoding. A motivation of our work is size lower bounds of refutations in Resolution for families of contradictions in the usual unary encoding. Our main interest is the $k$-Clique Principle, whose Resoluti…
▽ More
We investigate the size complexity of proofs in $Res(s)$ -- an extension of Resolution working on $s$-DNFs instead of clauses -- for families of contradictions given in the {\em unusual binary} encoding. A motivation of our work is size lower bounds of refutations in Resolution for families of contradictions in the usual unary encoding. Our main interest is the $k$-Clique Principle, whose Resolution complexity is still unknown.
Our main result is a $n^{Ω(k)}$ lower bound for the size of refutations of the binary $k$-Clique Principle in $Res(\lfloor \frac{1}{2}\log \log n\rfloor)$. This improves the result of Lauria, Pudlák et al. [24] who proved the lower bound for Resolution, that is $Res(1)$.
Our second lower bound proves that in $RES(s)$ for $s\leq \log^{\frac{1}{2-ε}}(n)$, the shortest proofs of the $BinPHP^m_n$, requires size $2^{n^{1-δ}}$, for any $δ>0$. Furthermore we prove that $BinPHP^m_n$ can be refuted in size $2^{Θ(n)}$ in treelike $Res(1)$, contrasting with the unary case, where $PHP^m_n$ requires treelike $RES(1)$ \ refutations of size $2^{Ω(n \log n)}$ [9,16].
Furthermore we study under what conditions the complexity of refutations in Resolution will not increase significantly (more than a polynomial factor) when shifting between the unary encoding and the binary encoding. We show that this is true, from unary to binary, for propositional encodings of principles expressible as a $Π_2$-formula and involving {\em total variable comparisons}. We then show that this is true, from binary to unary, when one considers the \emph{functional unary encoding}. Finally we prove that the binary encoding of the general Ordering principle $OP$ -- with no total ordering constraints -- is polynomially provable in Resolution.
△ Less
Submitted 19 September, 2018; v1 submitted 8 September, 2018;
originally announced September 2018.
-
Tight Bounds for Maximal Identifiability of Failure Nodes in Boolean Network Tomography
Authors:
Nicola Galesi,
Fariba Ranjbar
Abstract:
We study maximal identifiability, a measure recently introduced in Boolean Network Tomography to characterize networks' capability to localize failure nodes in end-to-end path measurements. We prove tight upper and lower bounds on the maximal identifiability of failure nodes for specific classes of network topologies, such as trees and $d$-dimensional grids, in both directed and undirected cases.…
▽ More
We study maximal identifiability, a measure recently introduced in Boolean Network Tomography to characterize networks' capability to localize failure nodes in end-to-end path measurements. We prove tight upper and lower bounds on the maximal identifiability of failure nodes for specific classes of network topologies, such as trees and $d$-dimensional grids, in both directed and undirected cases. We prove that directed $d$-dimensional grids with support $n$ have maximal identifiability $d$ using $2d(n-1)+2$ monitors; and in the undirected case we show that $2d$ monitors suffice to get identifiability of $d-1$. We then study identifiability under embeddings: we establish relations between maximal identifiability, embeddability and graph dimension when network topologies are model as DAGs. Our results suggest the design of networks over $N$ nodes with maximal identifiability $Ω(\log N)$ using $O(\log N)$ monitors and a heuristic to boost maximal identifiability on a given network by simulating $d$-dimensional grids. We provide positive evidence of this heuristic through data extracted by exact computation of maximal identifiability on examples of small real networks.
△ Less
Submitted 24 October, 2019; v1 submitted 28 December, 2017;
originally announced December 2017.
-
Space proof complexity for random 3-CNFs
Authors:
Patrick Bennett,
Ilario Bonacina,
Nicola Galesi,
Tony Huynh,
Mike Molloy,
Paul Wollan
Abstract:
We investigate the space complexity of refuting $3$-CNFs in Resolution and algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random $3$-CNF $φ$ in $n$ variables requires, with high probability, $Ω(n)$ distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation $φ$ requires, with high probability…
▽ More
We investigate the space complexity of refuting $3$-CNFs in Resolution and algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random $3$-CNF $φ$ in $n$ variables requires, with high probability, $Ω(n)$ distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation $φ$ requires, with high probability, $Ω(n)$ clauses each of width $Ω(n)$ to be kept at the same time in memory. This gives a $Ω(n^2)$ lower bound for the total space needed in Resolution to refute $φ$. These results are best possible (up to a constant factor).
The main technical innovation is a variant of Hall's Lemma. We show that in bipartite graphs $G$ with bipartition $(L,R)$ and left-degree at most 3, $L$ can be covered by certain families of disjoint paths, called VW-matchings, provided that $L$ expands in $R$ by a factor of $(2-ε)$, for $ε< 1/23$.
△ Less
Submitted 2 April, 2015; v1 submitted 5 March, 2015;
originally announced March 2015.
-
Space proof complexity for random $3$-CNFs via a $(2-ε)$-Hall's Theorem
Authors:
Ilario Bonacina,
Nicola Galesi,
Tony Huynh,
Paul Wollan
Abstract:
We investigate the space complexity of refuting $3$-CNFs in Resolution and algebraic systems. No lower bound for refuting any family of $3$-CNFs was previously known for the total space in resolution or for the monomial space in algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random $3$-CNF $φ$ in $n$ variables requires, with high probability,…
▽ More
We investigate the space complexity of refuting $3$-CNFs in Resolution and algebraic systems. No lower bound for refuting any family of $3$-CNFs was previously known for the total space in resolution or for the monomial space in algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random $3$-CNF $φ$ in $n$ variables requires, with high probability, $Ω(n/\log n)$ distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation $φ$ requires, with high probability, $Ω(n/\log n)$ clauses each of width $Ω(n/\log n)$ to be kept at the same time in memory. This gives a $Ω(n^2/\log^2 n)$ lower bound for the total space needed in Resolution to refute $φ$.
The main technical innovation is a variant of Hall's theorem. We show that in bipartite graphs $G$ with bipartition $(L,R)$ and left-degree at most 3, $L$ can be covered by certain families of disjoint paths, called $(2,4)$-matchings, provided that $L$ expands in $R$ by a factor of $(2-ε)$, for $ε< \frac{1}{23}$.
△ Less
Submitted 6 November, 2014;
originally announced November 2014.
