1. 
 Buss, S., et al.
(författare)

Reordering rule makes OBDD proof systems stronger
 2018

Ingår i: Leibniz International Proceedings in Informatics, LIPIcs.  : Schloss Dagstuhl LeibnizZentrum fur Informatik GmbH, Dagstuhl Publishing.  9783959770699 ; , s. 124

Konferensbidrag (refereegranskat)abstract
 Atserias, Kolaitis, and Vardi showed that the proof system of Ordered Binary Decision Diagrams with conjunction and weakening, OBDD(∧, weakening), simulates CP∗ (Cutting Planes with unary coefficients). We show that OBDD(∧, weakening) can give exponentially shorter proofs than daglike cutting planes. This is proved by showing that the CliqueColoring tautologies have polynomial size proofs in the OBDD(∧, weakening) system. The reordering rule allows changing the variable order for OBDDs. We show that OBDD (∧, weakening, reordering) is strictly stronger than OBDD(∧, weakening). This is proved using the CliqueColoring tautologies, and by transforming tautologies using coded permutations and orification. We also give CNF formulas which have polynomial size OBDD(∧) proofs but require superpolynomial (actually, quasipolynomial size) resolution proofs, and thus we partially resolve an open question proposed by Groote and Zantema. Applying daglike and treelike lifting techniques to the mentioned results, we completely analyze which of the systems among CP∗, OBDD(∧), OBDD(∧, reordering), OBDD(∧, weakening) and OBDD (∧, weakening, reordering) polynomially simulate each other. For daglike proof systems, some of our separations are quasipolynomial and some are exponential; for treelike systems, all of our separations are exponential.


2. 
 De Rezende, Susanna F., et al.
(författare)

Automating algebraic proof systems is NPhard
 2021

Ingår i: STOC 2021  Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing.  New York, NY, USA : ACM.  07378017.  9781450380539 ; , s. 209222

Konferensbidrag (refereegranskat)abstract
 We show that algebraic proofs are hard to find: Given an unsatisfiable CNF formula F, it is NPhard to find a refutation of F in the Nullstellensatz, Polynomial Calculus, or SheraliAdams proof systems in time polynomial in the size of the shortest such refutation. Our work extends, and gives a simplified proof of, the recent breakthrough of Atserias and Müller (JACM 2020) that established an analogous result for Resolution.


3. 
 de Rezende, Susanna F., et al.
(författare)

Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs
 2020

Ingår i: CCC '20: Proceedings of the 35th Computational Complexity Conference 2020.  : Schloss Dagstuhl–LeibnizZentrum für Informatik.  18688969.  9783959771566 ; 169, s. 281

Konferensbidrag (refereegranskat)abstract
 We show exponential lower bounds on resolution proof length for pigeonhole principle (PHP) formulas and perfect matching formulas over highly unbalanced, sparse expander graphs, thus answering the challenge to establish strong lower bounds in the regime between balanced constantdegree expanders as in [BenSasson and Wigderson'01] and highly unbalanced, dense graphs as in [Raz'04] and [Razborov'03,'04]. We obtain our results by revisiting Razborov's pseudowidth method for PHP formulas over dense graphs and extending it to sparse graphs. This further demonstrates the power of the pseudowidth method, and we believe it could potentially be useful for attacking also other longstanding open problems for resolution and other proof systems.


4. 
 de Rezende, Susanna F., et al.
(författare)

The power of negative reasoning
 2021

Ingår i: 36th Computational Complexity Conference, CCC 2021.  18688969.  9783959771931 ; 200

Konferensbidrag (refereegranskat)abstract
 Semialgebraic proof systems have been studied extensively in proof complexity since the late 1990s to understand the power of Gröbner basis computations, linear and semidefinite programming hierarchies, and other methods. Such proof systems are defined alternately with only the original variables of the problem and with special formal variables for positive and negative literals, but there seems to have been no study how these different definitions affect the power of the proof systems. We show for Nullstellensatz, polynomial calculus, SheraliAdams, and sumsofsquares that adding formal variables for negative literals makes the proof systems exponentially stronger, with respect to the number of terms in the proofs. These separations are witnessed by CNF formulas that are easy for resolution, which establishes that polynomial calculus, SheraliAdams, and sumsofsquares cannot efficiently simulate resolution without having access to variables for negative literals.


5. 
 Garg, Ankit, et al.
(författare)

Monotone Circuit Lower Bounds from Resolution
 2018

Ingår i: STOC'18.  New York, NY, USA : ASSOC COMPUTING MACHINERY. ; , s. 902911

Konferensbidrag (refereegranskat)abstract
 For any unsatisfiable CNF formula F that is hard to refute in the Resolution proof system, we show that a gadgetcomposed version of F is hard to refute in any proof system whose lines are computed by efficient communication protocolsor, equivalently, that a monotone function associated with F has large monotone circuit complexity. Our result extends to monotone real circuits, which yields new lower bounds for the Cutting Planes proof system.


6. 
 Garg, Ankit, et al.
(författare)

Monotone Circuit Lower Bounds from Resolution
 2020

Ingår i: Theory of Computing.  : Theory of Computing Exchange.  15572862. ; 16

Tidskriftsartikel (refereegranskat)abstract
 For any unsatisfiable CNF formula F that is hard to refute in the Resolution proof system, we show that a gadgetcomposed version of F is hard to refute in any proof system whose lines are computed by efficient communication protocolsor, equivalently, that a monotone function associated with F has large monotone circuit complexity. Our result extends to monotone real circuits, which yields new lower bounds for the Cutting Planes proof system.


7. 
 Göös, M., et al.
(författare)

Adventures in monotone complexity and TFNP
 2019

Ingår i: Leibniz International Proceedings in Informatics, LIPIcs.  : Schloss Dagstuhl LeibnizZentrum fur Informatik GmbH, Dagstuhl Publishing.  9783959770958

Konferensbidrag (refereegranskat)abstract
 Separations: We introduce a monotone variant of XorSat and show it has exponential monotone circuit complexity. Since XorSat is in NC2, this improves qualitatively on the monotone vs. nonmonotone separation of Tardos (1988). We also show that monotone span programs over R can be exponentially more powerful than over finite fields. These results can be interpreted as separating subclasses of TFNP in communication complexity. Characterizations: We show that the communication (resp. query) analogue of PPA (subclass of TFNP) captures span programs over F2 (resp. Nullstellensatz degree over F2). Previously, it was known that communication FP captures formulas (Karchmer–Wigderson, 1988) and that communication PLS captures circuits (Razborov, 1995).


8. 
 Jerzembeck, Fabian, et al.
(författare)

The superconductivity of Sr2RuO4 under caxis uniaxial stress
 2022

Ingår i: Nature Communications.  : Springer Nature.  20411723. ; 13:1

Tidskriftsartikel (refereegranskat)abstract
 Applying inplane uniaxial pressure to strongly correlated lowdimensional systems has been shown to tune the electronic structure dramatically. For example, the unconventional superconductor Sr2RuO4 can be tuned through a single Van Hove point, resulting in strong enhancement of both Tc and Hc2. Outofplane (c axis) uniaxial pressure is expected to tune the quasitwodimensional structure even more strongly, by pushing it towards two Van Hove points simultaneously. Here, we achieve a record uniaxial stress of 3.2 GPa along the c axis of Sr2RuO4. Hc2 increases, as expected for increasing density of states, but unexpectedly Tc falls. As a first attempt to explain this result, we present threedimensional calculations in the weak interaction limit. We find that within the weakcoupling framework there is no single order parameter that can account for the contrasting effects of inplane versus caxis uniaxial stress, which makes this new result a strong constraint on theories of the superconductivity of Sr2RuO4. In the superconductor Sr2RuO4, inplane strain is known to enhance both the superconducting transition temperature Tc and upper critical field Hc2, but the effect of outofplane strain has not been studied. Here, the authors find that Hc2 is enhanced under outofplane strain, but Tc unexpectedly decreases.


9. 
 Lagarde, G., et al.
(författare)

Tradeoffs between size and degree in polynomial calculus
 2020

Ingår i: Leibniz International Proceedings in Informatics, LIPIcs.  : Schloss Dagstuhl LeibnizZentrum fur Informatik GmbH, Dagstuhl Publishing. ; 151

Konferensbidrag (refereegranskat)abstract
 Building on [Clegg et al.’96], [Impagliazzo et al.’99] established that if an unsatisfiable kCNF formula over n variables has a refutation of size S in the polynomial calculus resolution proof system, then this formula also has a refutation of degree k + O(n log S). The proof of this works by converting a smallsize refutation into a smalldegree one, but at the expense of increasing the proof size exponentially. This raises the question of whether it is possible to achieve both small size and small degree in the same refutation, or whether the exponential blowup is inherent. Using and extending ideas from [Thapen’16], who studied the analogous question for the resolution proof system, we prove that a strong sizedegree tradeoff is necessary.


10. 
 Marković, Igor, et al.
(författare)

Electronically driven spinreorientation transition of the correlated polar metal Ca3Ru2O7
 2020

Ingår i: Proceedings of the National Academy of Sciences of the United States of America.  : Proceedings of the National Academy of Sciences.  00278424. ; 117:27, s. 1552415529

Tidskriftsartikel (refereegranskat)abstract
 The interplay between spinorbit coupling and structural inversion symmetry breaking in solids has generated much interest due to the nontrivial spin and magnetic textures which can result. Such studies are typically focused on systems where large atomic number elements lead to strong spinorbit coupling, in turn rendering electronic correlations weak. In contrast, here we investigate the temperaturedependent electronic structure of Ca3Ru2O7, a 4d oxide metal for which both correlations and spinorbit coupling are pronounced and in which octahedral tilts and rotations combine to mediate both global and local inversion symmetrybreaking polar distortions. Our angleresolved photoemission measurements reveal the destruction of a large holelike Fermi surface upon cooling through a coupled structural and spinreorientation transition at 48 K, accompanied by a sudden onset of quasiparticle coherence. We demonstrate how these result from band hybridization mediated by a hidden Rashbatype spin orbit coupling. This is enabled by the bulk structural distortions and unlocked when the spin reorients perpendicular to the local symmetrybreaking potential at the Ru sites. We argue that the electronic energy gain associated with the band hybridization is actually the key driver for the phase transition, reflecting a delicate interplay between spinorbit coupling and strong electronic correlations and revealing a route to control magnetic ordering in solids.

