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. 466485

Konferensbidrag (refereegranskat)abstract
 We consider the pebble game on DAGs with bounded fanin 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 PSPACEcomplete, 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 PSPACEhard 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 PSPACEhard 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.  02725428.  9798350318944 ; , s. 111

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ősRényi random graphs, are 3colourable.


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.  02725428.  9781728196220  9781728196213 ; 2020November, s. 4349

Konferensbidrag (refereegranskat)abstract
 One of the major open problems in complexity theory is proving superlogarithmic 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 querytocommunication lifting theorem. This allows us to handle several new and wellstudied functions such as the stconnectivity, clique, and generation functions. In order to carry this progress back to the nonmonotone setting, we introduce a new notion of semimonotone composition, which combines the nonmonotone 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.  02725428.  9781728196213  9781728196220 ; 2020November, s. 2430

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 greaterthan. 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 nonexplicit separation was known. •We give the strongest separation todate between monotone Boolean formulas and monotone Boolean circuits. Namely, we show that the classical GEN problem, which has polynomialsize 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).  00975397 . 10957111. ; 44:4, s. 11191153

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 timespace tradeoffs 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 wellunderstood 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. 11841211], 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 kCNF 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 3CNF 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 kCNF 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 3CNF in the canonical way, something that we believe can be useful when proving PCR space lower bounds for other wellstudied formula families in proof complexity.


6. 
 Gjerde, Kjetil, et al.
(författare)

On the suitability of carbon nanotube forests as nonstick surfaces for nanomanipulation
 2008

Ingår i: Soft Matter.  : Royal Society of Chemistry (RSC).  17446848 . 1744683X. ; 4:3, s. 392399

Tidskriftsartikel (refereegranskat)abstract
 A carbon nanotube forest provides a unique nonstick 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 plasmaenhanced chemical vapour deposition are compared to structures with a similar morphology, silicon nanograss, defined by anisotropic reactive ionetching. While manipulation experiments with latex microbeads on structured as well as smooth surfaces ( gold, silicon, silicon dioxide, Teflon, diamondlike 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. Contactangle measurements during gradual evaporation revealed that the silicon nanograss was superhydrophic with no contactline pinning, while carbon nanotube forests in contrast showed strong contactline 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 diamondlike 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 nonstick surface for nanomanipulation is indeed the strong contactline 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 GateLevel Multiplier Verification
 2022

Ingår i: Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022.  9783981926361 ; , s. 14311436

Konferensbidrag (refereegranskat)abstract
 Algebraic reasoning has proven to be one of the most effective approaches for verifying gatelevel integer multipliers, 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 Bitvector Multiplication Using Cutting Planes Reasoning
 2020

Ingår i: Proceedings of the 20th Conference on Formal Methods in ComputerAided Design, FMCAD 2020.  9783854480426 ; , s. 194204

Konferensbidrag (refereegranskat)abstract
 Systems mixing Boolean logic and arithmetic have been a longstanding challenge for verification tools such as SATbased bitvector 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 bitlevel reasoning. We propose that pseudoBoolean 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 optimallength cutting planes proofs for a large class of bitlevel 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 bitlevel consequences of wordlevel equations in exponentially fewer steps than methods based on Gröbner bases. Experimentally, we demonstrate that pseudoBoolean solvers can verify the wordlevel equivalence of adderbased multiplier architectures, as well as commutativity of bitvector multiplication, in times comparable to the best algebraic methods. We then go further than previous approaches and also verify these properties at the bitlevel. Finally, we find examples of simple nonlinear bitvector inequalities that are intractable for current bitvector and SAT solvers but easy for pseudoBoolean solvers.

