| 1. |
- Chan, S. M., et al.
(författare)
-
Hardness of Approximation in PSPACE and Separation Results for Pebble Games
- 2015
-
Ingår i: Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS. - : Institute of Electrical and Electronics Engineers (IEEE). - 9781467381918 ; , s. 466-485
-
Konferensbidrag (refereegranskat)abstract
- We consider the pebble game on DAGs with bounded fan-in introduced in [Paterson and Hewitt '70] and the reversible version of this game in [Bennett '89], and study the question of how hard it is to decide exactly or approximately the number of pebbles needed for a given DAG in these games. We prove that the problem of deciding whether s pebbles suffice to reversibly pebble a DAG G is PSPACE-complete, as was previously shown for the standard pebble game in [Gilbert, Lengauer and Tarjan '80]. Via two different graph product constructions we then strengthen these results to establish that both standard and reversible pebbling space are PSPACE-hard to approximate to within any additive constant. To the best of our knowledge, these are the first hardness of approximation results for pebble games in an unrestricted setting (even for polynomial time). Also, since [Chan '13] proved that reversible pebbling is equivalent to the games in [Dymond and Tompa '85] and [Raz and McKenzie '99], our results apply to the Dymond - Tompa and Raz - McKenzie games as well, and from the same paper it follows that resolution depth is PSPACE-hard to determine up to any additive constant. We also obtain a multiplicative logarithmic separation between reversible and standard pebbling space. This improves on the additive logarithmic separation previously known and could plausibly be tight, although we are not able to prove this. We leave as an interesting open problem whether our additive hardness of approximation result could be strengthened to a multiplicative bound if the computational resources are decreased from polynomial space to the more common setting of polynomial time.
|
|
| 2. |
- Conneryd, Jonas, et al.
(författare)
-
Graph Colouring Is Hard on Average for Polynomial Calculus and Nullstellensatz
- 2023
-
Ingår i: Proceedings - 2023 IEEE 64th Annual Symposium on Foundations of Computer Science, FOCS 2023. - 0272-5428. - 9798350318944 ; , s. 1-11
-
Konferensbidrag (refereegranskat)abstract
- We prove that polynomial calculus (and hence also Nullstellensatz) over any field requires linear degree to refute that sparse random regular graphs, as well as sparse Erdős-Rényi random graphs, are 3-colourable.
|
|
| 3. |
- De Rezende, Susanna F., et al.
(författare)
-
KRW composition theorems via lifting
- 2020
-
Ingår i: Proceedings - 2020 IEEE 61st Annual Symposium on Foundations of Computer Science, FOCS 2020. - 0272-5428. - 9781728196213 - 9781728196220 ; 2020-November, s. 43-49
-
Konferensbidrag (refereegranskat)abstract
- One of the major open problems in complexity theory is proving super-logarithmic lower bounds on the depth of circuits (i.e., mathrm{P} nsubseteq text{NC}{1}). Karchmer, Raz, and Wigderson [13] suggested to approach this problem by proving that depth complexity behaves'as expected' with respect to the composition of functions f diamond g. They showed that the validity of this conjecture would imply that mathrm{P} nsubseteq text{NC}{1}. Several works have made progress toward resolving this conjecture by proving special cases. In particular, these works proved the KRW conjecture for every outer function, but only for few inner functions. Thus, it is an important challenge to prove the KRW conjecture for a wider range of inner functions. In this work, we extend significantly the range of inner functions that can be handled. First, we consider the monotone version of the KRW conjecture. We prove it for every monotone inner function whose depth complexity can be lower bounded via a query-to-communication lifting theorem. This allows us to handle several new and well-studied functions such as the s-t-connectivity, clique, and generation functions. In order to carry this progress back to the non-monotone setting, we introduce a new notion of semi-monotone composition, which combines the non-monotone complexity of the outer function with the monotone complexity of the inner function. In this setting, we prove the KRW conjecture for a similar selection of inner functions, but only for a specific choice of the outer function f.
|
|
| 4. |
- De Rezende, Susanna, et al.
(författare)
-
Lifting with simple gadgets and applications to circuit and proof complexity
- 2020
-
Ingår i: Proceedings - 2020 IEEE 61st Annual Symposium on Foundations of Computer Science, FOCS 2020. - 0272-5428. - 9781728196213 - 9781728196220 ; 2020-November, s. 24-30
-
Konferensbidrag (refereegranskat)abstract
- We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve three open problems: •We present the first result that demonstrates a separation in proof power for cutting planes with unbounded versus polynomially bounded coefficients. Specifically, we exhibit CNF formulas that can be refuted in quadratic length and constant line space in cutting planes with unbounded coefficients, but for which there are no refutations in subexponential length and subpolynomial line space if coefficients are restricted to be of polynomial magnitude. •We give the first explicit separation between monotone Boolean formulas and monotone real formulas. Specifically, we give an explicit family of functions that can be computed with monotone real formulas of nearly linear size but require monotone Boolean formulas of exponential size. Previously only a non-explicit separation was known. •We give the strongest separation to-date between monotone Boolean formulas and monotone Boolean circuits. Namely, we show that the classical GEN problem, which has polynomial-size monotone Boolean circuits, requires monotone Boolean formulas of size 2{Omega(n text{polylog}(n))}. An important technical ingredient, which may be of independent interest, is that we show that the Nullstellensatz degree of refuting the pebbling formula over a DAG G over any field coincides exactly with the reversible pebbling price of G. In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal. This is an extended abstract. The full version of the paper is available at https://arxiv.org/abs/2001.02144.
|
|
| 5. |
- Filmus, Yuval, et al.
(författare)
-
Space complexity in polynomial calculus
- 2015
-
Ingår i: SIAM journal on computing (Print). - : Society for Industrial & Applied Mathematics (SIAM). - 0097-5397 .- 1095-7111. ; 44:4, s. 1119-1153
-
Tidskriftsartikel (refereegranskat)abstract
- During the last 10 to 15 years, an active line of research in proof complexity has been to study space complexity and time-space trade-offs for proofs. Besides being a natural complexity measure of intrinsic interest, space is also an important concern in SAT solving, and so research has mostly focused on weak systems that are used by SAT solvers. There has been a relatively long sequence of papers on space in resolution, which is now reasonably well-understood from this point of view. For other proof systems of interest, however, such as polynomial calculus or cutting planes, progress has been more limited. Essentially nothing has been known about space complexity in cutting planes, and for polynomial calculus the only lower bound has been for conjunctive normal form (CNF) formulas of unbounded width in [Alekhnovich et al., SIAM J. Comput., 31 (2002), pp. 1184-1211], where the space lower bound is smaller than the initial width of the clauses in the formulas. Thus, in particular, it has been consistent with current knowledge that polynomial calculus could be able to refute any k-CNF formula in constant space. In this paper, we prove several new results on space in polynomial calculus (PC) and in the extended proof system polynomial calculus resolution (PCR) studied by Alekhnovich et al.: (1) We prove an omega(n) space lower bound in PC for the canonical 3-CNF version of the pigeonhole principle formulas PHPmn with m pigeons and n holes, and show that this is tight. (2) For PCR, we prove an omega(n) space lower bound for a bitwise encoding of the functional pigeonhole principle. These formulas have width O(log n), and hence this is an exponential improvement over Alekhnovich et al. measured in the width of the formulas. (3) We then present another encoding of the pigeonhole principle that has constant width, and prove an omega(n) space lower bound in PCR for these formulas as well. (4) Finally, we prove that any k-CNF formula can be refuted in PC in simultaneous exponential size and linear space (which holds for resolution and thus for PCR, but was not obviously the case for PC). We also characterize a natural class of CNF formulas for which the space complexity in resolution and PCR does not change when the formula is transformed into 3-CNF in the canonical way, something that we believe can be useful when proving PCR space lower bounds for other well-studied formula families in proof complexity.
|
|
| 6. |
- Gjerde, Kjetil, et al.
(författare)
-
On the suitability of carbon nanotube forests as non-stick surfaces for nanomanipulation
- 2008
-
Ingår i: Soft Matter. - : Royal Society of Chemistry (RSC). - 1744-6848 .- 1744-683X. ; 4:3, s. 392-399
-
Tidskriftsartikel (refereegranskat)abstract
- A carbon nanotube forest provides a unique non-stick surface for nanomanipulation, as the nanostructuring of the surface allows micro- and nanoscale objects to be easily removed after first being deposited via a liquid dispersion. A common problem for smooth surfaces is the strong initial stiction caused by adhesion forces after deposition onto the surface. In this work, carbon nanotube forests fabricated by plasma-enhanced chemical vapour deposition are compared to structures with a similar morphology, silicon nanograss, defined by anisotropic reactive ion-etching. While manipulation experiments with latex microbeads on structured as well as smooth surfaces ( gold, silicon, silicon dioxide, Teflon, diamond-like carbon) showed a very low initial stiction for both carbon nanotube forests and silicon nanograss, a homogeneous distribution of particles was significantly easier to achieve on the carbon nanotube forests. Contact-angle measurements during gradual evaporation revealed that the silicon nanograss was superhydrophic with no contact-line pinning, while carbon nanotube forests in contrast showed strong contact-line pinning, as confirmed by environmental scanning electron microscopy of microdroplets. As a consequence, latex microbeads dispersed on the surface from an aqueous solution distributed evenly on carbon nanotube forests, but formed large agglomerates after evaporation on silicon nanograss. Lateral manipulation of latex microbeads with a microcantilever was found to be easier on carbon nanotube forests and silicon nanograss compared to smooth diamond-like carbon, due to a substantially lower initial stiction force on surfaces with nanoscale roughness. Nanomanipulation of bismuth nanowires, carbon nanotubes and organic nanofibres was demonstrated on carbon nanotube forests using a sharp tungsten tip. We find that the reason for the remarkable suitability of carbon nanotube forests as a non-stick surface for nanomanipulation is indeed the strong contact-line pinning in combination with the nanostructured surface, which allows homogeneous dispersion and easy manipulation of individual particles.
|
|
| 7. |
- Kaufmann, Daniela, et al.
(författare)
-
Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification
- 2022
-
Ingår i: Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022. - 9783981926361 ; , s. 1431-1436
-
Konferensbidrag (refereegranskat)abstract
- Algebraic reasoning has proven to be one of the most effective approaches for verifying gate-level integer mul-tipliers, but it struggles with certain components, necessitating the complementary use of SAT solvers. For this reason validation certificates require proofs in two different formats. Approaches to unify the certificates are not scalable, meaning that the validation results can only be trusted up to the correctness of compositional reasoning. We show in this paper that using dual variables in the algebraic encoding, together with a novel tail substitution and carry rewriting method, removes the need for SAT solvers in the verification flow and yields a single, uniform proof certificate.
|
|
| 8. |
- Liew, Vincent, et al.
(författare)
-
Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning
- 2020
-
Ingår i: Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020. - 9783854480426 ; , s. 194-204
-
Konferensbidrag (refereegranskat)abstract
- Systems mixing Boolean logic and arithmetic have been a long-standing challenge for verification tools such as SAT-based bit-vector solvers. Though SAT solvers can be highly efficient for Boolean reasoning, they scale poorly once multiplication is involved. Algebraic methods using Gröbner basis reduction have recently been used to efficiently verify multiplier circuits in isolation, but generally do not perform well on problems involving bit-level reasoning. We propose that pseudo-Boolean solvers equipped with cutting planes reasoning have the potential to combine the complementary strengths of the existing SAT and algebraic approaches while avoiding their weaknesses. Theoretically, we show that there are optimal-length cutting planes proofs for a large class of bit-level properties of some well known multiplier circuits. This scaling is significantly better than the smallest proofs known for SAT and, in some instances, for algebraic methods. We also show that cutting planes reasoning can extract bit-level consequences of word-level equations in exponentially fewer steps than methods based on Gröbner bases. Experimentally, we demonstrate that pseudo-Boolean solvers can verify the word-level equivalence of adder-based multiplier architectures, as well as commutativity of bit-vector multiplication, in times comparable to the best algebraic methods. We then go further than previous approaches and also verify these properties at the bit-level. Finally, we find examples of simple nonlinear bit-vector inequalities that are intractable for current bit-vector and SAT solvers but easy for pseudo-Boolean solvers.
|
|
