| 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- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. - 9783959770699 ; , s. 1-24
-
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 dag-like cutting planes. This is proved by showing that the Clique-Coloring 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 Clique-Coloring 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 dag-like and tree-like 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 dag-like proof systems, some of our separations are quasipolynomial and some are exponential; for tree-like systems, all of our separations are exponential.
|
|
| 2. |
- De Rezende, Susanna F., et al.
(författare)
-
Automating algebraic proof systems is NP-hard
- 2021
-
Ingår i: STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing. - New York, NY, USA : ACM. - 0737-8017. - 9781450380539 ; , s. 209-222
-
Konferensbidrag (refereegranskat)abstract
- We show that algebraic proofs are hard to find: Given an unsatisfiable CNF formula F, it is NP-hard to find a refutation of F in the Nullstellensatz, Polynomial Calculus, or Sherali-Adams 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–Leibniz-Zentrum für Informatik. - 1868-8969. - 9783959771566 ; 169, s. 28-1
-
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 constant-degree expanders as in [Ben-Sasson and Wigderson'01] and highly unbalanced, dense graphs as in [Raz'04] and [Razborov'03,'04]. We obtain our results by revisiting Razborov's pseudo-width method for PHP formulas over dense graphs and extending it to sparse graphs. This further demonstrates the power of the pseudo-width 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. - 1868-8969. - 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, Sherali-Adams, and sums-of-squares 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, Sherali-Adams, and sums-of-squares 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. 902-911
-
Konferensbidrag (refereegranskat)abstract
- For any unsatisfiable CNF formula F that is hard to refute in the Resolution proof system, we show that a gadget-composed version of F is hard to refute in any proof system whose lines are computed by efficient communication protocols-or, 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. - 1557-2862. ; 16
-
Tidskriftsartikel (refereegranskat)abstract
- For any unsatisfiable CNF formula F that is hard to refute in the Resolution proof system, we show that a gadget-composed version of F is hard to refute in any proof system whose lines are computed by efficient communication protocols-or, 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- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. - 9783959770958
-
Konferensbidrag (refereegranskat)abstract
- Separations: We introduce a monotone variant of Xor-Sat and show it has exponential monotone circuit complexity. Since Xor-Sat is in NC2, this improves qualitatively on the monotone vs. non-monotone 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 c-axis uniaxial stress
- 2022
-
Ingår i: Nature Communications. - : Springer Nature. - 2041-1723. ; 13:1
-
Tidskriftsartikel (refereegranskat)abstract
- Applying in-plane uniaxial pressure to strongly correlated low-dimensional 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 T-c and H-c2. Out-of-plane (c axis) uniaxial pressure is expected to tune the quasi-two-dimensional 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. H-c2 increases, as expected for increasing density of states, but unexpectedly T-c falls. As a first attempt to explain this result, we present three-dimensional calculations in the weak interaction limit. We find that within the weak-coupling framework there is no single order parameter that can account for the contrasting effects of in-plane versus c-axis uniaxial stress, which makes this new result a strong constraint on theories of the superconductivity of Sr2RuO4. In the superconductor Sr2RuO4, in-plane strain is known to enhance both the superconducting transition temperature Tc and upper critical field Hc2, but the effect of out-of-plane strain has not been studied. Here, the authors find that Hc2 is enhanced under out-of-plane strain, but Tc unexpectedly decreases.
|
|
| 9. |
- Lagarde, G., et al.
(författare)
-
Trade-offs between size and degree in polynomial calculus
- 2020
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - : Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. ; 151
-
Konferensbidrag (refereegranskat)abstract
- Building on [Clegg et al.’96], [Impagliazzo et al.’99] established that if an unsatisfiable k-CNF 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 small-size refutation into a small-degree 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 blow-up is inherent. Using and extending ideas from [Thapen’16], who studied the analogous question for the resolution proof system, we prove that a strong size-degree trade-off is necessary.
|
|
| 10. |
- Marković, Igor, et al.
(författare)
-
Electronically driven spin-reorientation 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. - 0027-8424. ; 117:27, s. 15524-15529
-
Tidskriftsartikel (refereegranskat)abstract
- The interplay between spin-orbit 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 spin-orbit coupling, in turn rendering electronic correlations weak. In contrast, here we investigate the temperature-dependent electronic structure of Ca3Ru2O7, a 4d oxide metal for which both correlations and spin-orbit coupling are pronounced and in which octahedral tilts and rotations combine to mediate both global and local inversion symmetry-breaking polar distortions. Our angle-resolved photoemission measurements reveal the destruction of a large hole-like 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 Rashba-type spin- orbit coupling. This is enabled by the bulk structural distortions and unlocked when the spin reorients perpendicular to the local symmetry-breaking 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 spin-orbit coupling and strong electronic correlations and revealing a route to control magnetic ordering in solids.
|
|
