Jacobo Torán

MFCS Conference 2024 Conference Paper

Pebble Games and Algebraic Proof Systems

• Lisa-Marie Jaser
• Jacobo Torán

Analyzing refutations of the well known pebbling formulas Peb(G) we prove some new strong connections between pebble games and algebraic proof system, showing that there is a parallelism between the reversible, black and black-white pebbling games on one side, and the three algebraic proof systems Nullstellensatz, Monomial Calculus and Polynomial Calculus on the other side. In particular we prove that for any DAG G with a single sink, if there is a Monomial Calculus refutation for Peb(G) having simultaneously degree s and size t then there is a black pebbling strategy on G with space s and time t+s. Also if there is a black pebbling strategy for G with space s and time t it is possible to extract from it a MC refutation for Peb(G) having simultaneously degree s and size ts. These results are analogous to those proven in [Susanna F. de Rezende et al. , 2021] for the case of reversible pebbling and Nullstellensatz. Using them we prove degree separations between NS, MC and PC, as well as strong degree-size tradeoffs for MC. We also notice that for any directed acyclic graph G the space needed in a pebbling strategy on G, for the three versions of the game, reversible, black and black-white, exactly matches the variable space complexity of a refutation of the corresponding pebbling formula Peb(G) in each of the algebraic proof systems NS, MC and PC. Using known pebbling bounds on graphs, this connection implies separations between the corresponding variable space measures.

SAT Conference 2023 Conference Paper

Cutting Planes Width and the Complexity of Graph Isomorphism Refutations

• Jacobo Torán
• Florian Wörz

The width complexity measure plays a central role in Resolution and other propositional proof systems like Polynomial Calculus (under the name of degree). The study of width lower bounds is the most extended method for proving size lower bounds, and it is known that for these systems, proofs with small width also imply the existence of proofs with small size. Not much has been studied, however, about the width parameter in the Cutting Planes (CP) proof system, a measure that was introduced by Dantchev and Martin in 2011 under the name of CP cutwidth. In this paper, we study the width complexity of CP refutations of graph isomorphism formulas. For a pair of non-isomorphic graphs G and H, we show a direct connection between the Weisfeiler-Leman differentiation number WL(G, H) of the graphs and the width of a CP refutation for the corresponding isomorphism formula Iso(G, H). In particular, we show that if WL(G, H) ≤ k, then there is a CP refutation of Iso(G, H) with width k, and if WL(G, H) > k, then there are no CP refutations of Iso(G, H) with width k-2. Similar results are known for other proof systems, like Resolution, Sherali-Adams, or Polynomial Calculus. We also obtain polynomial-size CP refutations from our width bound for isomorphism formulas for graphs with constant WL-dimension.

TCS Journal 2023 Journal Article

Pure Nash equilibria in a generalization of congestion games allowing resource failures

• Julian Nickerl
• Jacobo Torán

We introduce a model for congestion games in which resources can fail with some probability distribution. These games are an extension of classical congestion games, and like these, have exact potential functions that guarantee the existence of pure Nash equilibria (PNE). We prove that the agent's cost functions for these games can be hard to compute by giving an example of a game for which the cost function is hard for Valiant's # P class, even in the case when all failure probabilities coincide. We characterize the complexity of computing PNE in congestion games with failures with an extension of the local search class PLS that allows queries to a # P function, and show examples of games for which the PNE search problem is complete for this class. Furthermore, we provide a variant of the game with the property that a PNE can be constructed in polynomial time if this also holds in the restricted game without failures.

CSL Conference 2022 Conference Paper

Number of Variables for Graph Differentiation and the Resolution of GI Formulas

• Jacobo Torán
• Florian Wörz

We show that the number of variables and the quantifier depth needed to distinguish a pair of graphs by first-order logic sentences exactly match the complexity measures of clause width and positive depth needed to refute the corresponding graph isomorphism formula in propositional narrow resolution. Using this connection, we obtain upper and lower bounds for refuting graph isomorphism formulas in (normal) resolution. In particular, we show that if k is the number of variables needed to distinguish two graphs with n vertices each, then there is an n^O(k) resolution refutation size upper bound for the corresponding isomorphism formula, as well as lower bounds of 2^(k-1) and k for the tree-like resolution size and resolution clause space for this formula. We also show a (normal) resolution size lower bound of exp(Ω(k²/n)) for the case of colored graphs with constant color class sizes. Applying these results, we prove the first exponential lower bound for graph isomorphism formulas in the proof system SRC-1, a system that extends resolution with a global symmetry rule, thereby answering an open question posed by Schweitzer and Seebach.

SAT Conference 2018 Conference Paper

Cops-Robber Games and the Resolution of Tseitin Formulas

• Nicola Galesi
• Navid Talebanfard
• Jacobo Torán

Abstract We characterize several complexity measures for the resolution of Tseitin formulas in terms of a two person cop-robber game. Our game is a slight variation of the one Seymour and Thomas used in order to characterize the tree-width parameter. For any undirected graph, by counting the number of cops needed in our game in order to catch a robber in it, we are able to exactly characterize the width, variable space and depth measures for the resolution of the Tseitin formula corresponding to that graph. We also give an exact game characterization of resolution variable space for any formula. We show that our game can be played in a monotone way. This implies that the corresponding resolution measures on Tseitin formulas correspond exactly to those under the restriction of regular resolution. Using our characterizations we improve the existing complexity bounds for Tseitin formulas showing that resolution width, depth and variable space coincide up to a logarithmic factor, and that variable space is bounded by the clause space times a logarithmic factor.

I&C Journal 2017 Journal Article

CNF and DNF succinct graph encodings

• Bireswar Das
• Patrick Scharpfenecker
• Jacobo Torán

It is well-known that succinct encodings of computational problems – using circuits or formulas to encode large instances – generally result in an exponential complexity blow-up compared to their original complexity. We introduce a new way to encode graph problems, based on CNF or DNF formulas. We show that – contrary to the other existing succinct models – there are examples of problems whose complexity does not increase when encoded in the new form, or increases to an intermediate complexity class less powerful than the exponential blow up. We also study the complexity of the succinct versions of the Graph Isomorphism problem. We show that all the versions are hard for PSPACE. Although the exact complexity of these problems is still unknown, we show that under most existing succinct models the different versions of the problem are equivalent. We also give an algorithm for the DNF encoded version of GI whose running time depends mainly on the number of terms in the succinct representation.

SAT Conference 2016 Conference Paper

Solution-Graphs of Boolean Formulas and Isomorphism

• Patrick Scharpfenecker
• Jacobo Torán

Abstract The solution graph of a Boolean formula on n variables is the subgraph of the hypercube \(H_n\) induced by the satisfying assignments of the formula. The structure of solution graphs has been the object of much research in recent years since it is important for the performance of SAT-solving procedures based on local search. Several authors have studied connectivity problems in such graphs focusing on how the structure of the original formula might affect the complexity of the connectivity problems in the solution graph. In this paper we study the complexity of the isomorphism problem of solution graphs of Boolean formulas and we investigate how this complexity depends on the formula type. We observe that for general formulas the solution graph isomorphism problem can be solved in exponential time while in the cases of 2CNF formulas, as well as for CPSS formulas, the problem is in the counting complexity class \(\text {C}_=\text {P} \), a subclass of PSPACE. We also prove a strong property on the structure of solution graphs of Horn formulas showing that they are just unions of partial cubes. In addition we give a \(\text {PSPACE} \) lower bound for the problem on general Boolean functions. We prove that for 2CNF, as well as for CPSS formulas the solution graph isomorphism problem is hard for \(\text {C}_=\text {P} \) under polynomial time many one reductions, thus matching the given upper bound.

SAT Conference 2013 Conference Paper

On the Resolution Complexity of Graph Non-isomorphism

• Jacobo Torán

Abstract For a pair of given graphs we encode the isomorphism principle in the natural way as a CNF formula of polynomial size in the number of vertices, which is satisfiable if and only if the graphs are isomorphic. Using the CFI graphs from [12], we can transform any undirected graph G into a pair of non-isomorphic graphs. We prove that the resolution width of any refutation of the formula stating that these graphs are isomorphic has a lower bound related to the expansion properties of G. Using this fact, we provide an explicit family of non-isomorphic graph pairs for which any resolution refutation requires an exponential number of clauses in the size of the initial formula. These graphs pairs are colored with color multiplicity bounded by 4. In contrast we show that when the color classes are restricted to have size 3 or less, the non-isomorphism formulas have tree-like resolution refutations of polynomial size.

I&C Journal 2012 Journal Article

Restricted space algorithms for isomorphism on bounded treewidth graphs

• Bireswar Das
• Jacobo Torán
• Fabian Wagner

The Graph Isomorphism problem restricted to graphs of bounded treewidth or bounded tree distance width are known to be solvable in polynomial time. We give restricted space algorithms for these problems proving the following results: • Isomorphism for bounded tree distance width graphs is in L and thus complete for the class. We also show that for this kind of graphs a canon can be computed within logspace. • For bounded treewidth graphs, when both input graphs are given together with a tree decomposition, the problem of whether there is an isomorphism which respects the decompositions (i. e. when only isomorphisms are considered, mapping bags in one decomposition blockwise onto bags in the other decomposition) is in L. • For bounded treewidth graphs, when one of the input graphs is given with a tree decomposition the isomorphism problem is in LogCFL. • As a corollary the isomorphism problem for bounded treewidth graphs is in LogCFL. This improves the known TC1 upper bound for the problem given by Grohe and Verbitsky.

I&C Journal 2003 Journal Article

Optimal proof systems imply complete sets for promise classes

• Johannes Köbler
• Jochen Messner
• Jacobo Torán

A polynomial time computable function h: Σ *→Σ * whose range is a set L is called a proof system for L. In this setting, an h-proof for x∈L is just a string w with h(w)=x. Cook and Reckhow defined this concept in [13], and in order to compare the relative strength of different proof systems for the set TAUT of tautologies in propositional logic, they considered the notion of p-simulation. Intuitively, a proof system h ′ p-simulates h if any h-proof w can be translated in polynomial time into an h ′-proof w ′ for h(w). We also consider the related notion of simulation between proof systems where it is only required that for any h-proof w there exists an h ′-proof w ′ whose size is polynomially bounded in the size of w. A proof system is called (p-)optimal for a set L if it (p-)simulates every other proof system for L. The question whether p-optimal or optimal proof systems for TAUT exist is an important one in the field. In this paper we show a close connection between the existence of (p-)optimal proof systems and the existence of complete problems for certain promise complexity classes like UP, NP∩Sparse, RP or BPP. For this we introduce the notion of a test set for a promise class C and prove that C has a many-one complete set if and only if C has a test set T with a p-optimal proof system. If in addition the machines defining a promise class have a certain ability to guess proofs, then the existence of a p-optimal proof system for T can be replaced by the presumably weaker assumption that T has an optimal proof system. Strengthening a result from Krajı́ c ̌ ek and Pudlák [20], we also give sufficient conditions for the existence of optimal and p-optimal proof systems.

TCS Journal 2001 Journal Article

A nonadaptive NC checker for permutation group intersection

• V. Arvind
• Jacobo Torán

We design a nonadaptive NC checker for permutation group intersection, sharpening a result of Blum and Kannan (J. ACM 43 (1995) 269–291). Additionally, we also get nonadaptive NC checkers for some related group-theoretic problems.

I&C Journal 2001 Journal Article

Space Bounds for Resolution

• Juan Luis Esteban
• Jacobo Torán

We introduce a new way to measure the space needed in resolution refutations of CNF formulas in propositional logic. With the former definition (1994, B. H. Kleine and T. Lettman, “Aussangenlogik: Deduktion und Algorithmen, Teubner, Stuttgart) the space required for the resolution of any unsatisfiable formula in CNF is linear in the number of clauses. The new definition allows a much finer analysis of the space in the refutation, ranging from constant to linear space. Moreover, the new definition allows us to relate the space needed in a resolution proof of a formula to other well-studied complexity measures. It coincides with the complexity of a pebble game in the resolution graphs of a formula and, as we show, has relationships to the size of the refutation. We also give upper and lower bounds on the space needed for the resolution of unsatisfiable formulas. We show that Tseitin formulas associated to a certain kind of expander graphs of n nodes need resolution space n−c for some constant c. Measured on the number of clauses, this result is the best possible. We also show that the formulas expressing the general pigeonhole principle with n holes and more than n pigeons need space n+1 independent of the number of pigeons. Since a matching space upper bound of n+1 for these formulas exists, the obtained bound is exact. We also point to a possible connection between resolution space and resolution width, another measure for the complexity of resolution refutations.

FOCS Conference 2000 Conference Paper

On the Hardness of Graph Isomorphism

• Jacobo Torán

We show that the graph isomorphism problem is hard under logarithmic space many-one reductions for the complexity classes NL, PL (probabilistic logarithmic space), for every logarithmic space modular class Mod/sub k/L and for the class DET of problems NC/sup 1/ reducible to the determinant. These are the strongest existing hardness results for the graph isomorphism problem, and imply a randomized logarithmic space reduction from the perfect matching problem to graph isomorphism.

CSL Conference 1999 Conference Paper

Lower Bounds for Space in Resolution

• Jacobo Torán

Abstract Resolution space measures the maximum number of clauses that need to be simultaneously active in a resolution refutation. This complexity measure was defined by Kleine Büning and Lettmann in [ 8 ] and slightly modified recently [ 6 ] to make it suitable for comparisons with other measures. Since its definition, only trivial lower bound for the resolution space, measured in terms of the number of initial clauses were known. In this paper we prove optimal lower bounds for the space needed in the resolution refutation of two important families of formulas. We show that Tseitin formulas associated to a certain kind of expander graphs of n nodes need resolution space n - c for some constant c. Measured on the number of clauses, this result is best possible since the mentioned formulas have O ( n ) clauses, and the number of clauses is an upper bound for the resolution space. We also show that the formulas expressing the general Pigeonhole Principle with n holes and more than n pigeons, need space n + 1 independently of the number of pigeons. Since a matching space upper bound of n + 1 for these formulas exist, the obtained bound is exact. These results point to a possible connection between resolution space and resolution width, another measure for the complexity of resolution refutations.

TCS Journal 1995 Journal Article

Computing functions with parallel queries to NP

• Birgit Jenner
• Jacobo Torán

The class Θ 2 p of languages polynomial-time truth-table reducible to sets in NP has a wide range of different characterizations. We consider several functional versions of Θ 2 p based on these characterizations. We show that in this way the three function classes FLlog NP, FPlog NP, and FP∥ NP are obtained. In contrast to the language case the function classes seem to all be different. We give evidence in support of this fact by showing that FLlog NP coincides with any of the other classes then L = P, and that the equality of the classes FPlog NP and FP∥ NP would imply that the number of nondeterministic bits needed for the computation of any problem in NP can be reduced by a polylogarithmic factor, and that the problem can be computed deterministically with a subexponential time bound of order 2 n O(1/log log n).

MFCS Conference 1990 Invited Paper

Counting the Number of Solutions

• Jacobo Torán