Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space

We show a new connection between the clause space measure in tree-like resolution and the reversible pebble game on graphs. Using this connection, we provide several formula classes for which there is a logarithmic factor separation between the clause space complexity measure in tree-like and general resolution. We also provide upper bounds for tree-like resolution clause space in terms of general resolution clause and variable space. In particular, we show that for any formula F, its tree-like resolution clause space is upper bounded by space$$(\pi)$$ ( π ) $$(\log({\rm time}(\pi))$$ ( log ( time ( π ) ) , where $$\pi$$ π is any general resolution refutation of F. This holds considering as space$$(\pi)$$ ( π ) the clause space of the refutation as well as considering its variable space. For the concrete case of Tseitin formulas, we are able to improve this bound to the optimal bound space$$(\pi)\log n$$ ( π ) log n , where n is the number of vertices of the corresponding graph

Rigidity, normal modes and flexible motion of a SARS-CoV-2 (COVID-19) protease structure

The rigidity and flexibility of two recently reported crystal structures (PDB entries 6Y2E and 6LU7) of a protease from the SARS-CoV-2 virus, the infectious agent of the COVID-19 respiratory disease, has been investigated using pebble-game rigidity analysis, elastic network model normal mode analysis, and all-atom geometric simulations. This computational investigation of the viral protease follows protocols that have been effective in studying other homodimeric enzymes. The protease is predicted to display flexible motions in vivo which directly affect the geometry of a known inhibitor binding site and which open new potential binding sites elsewhere in the structure. A database of generated PDB files representing natural flexible variations on the crystal structures has been produced and made available for download from an institutional data archive. This information may inform structure-based drug design and fragment screening efforts aimed at identifying specific antiviral therapies for the treatment of COVID-19.

Rigidity Analysis of Protein Molecules

Intrinsic flexibility of protein molecules enables them to change their 3D structure and perform their specific task. Therefore, identifying rigid regions and consequently flexible regions of proteins has a significant role in studying protein molecules' function. In this study, we developed a kinematic model of protein molecules considering all covalent and hydrogen bonds in protein structure. Then, we used this model and developed two independent rigidity analysis methods to calculate degrees of freedom (DOF) and identify flexible and rigid regions of the proteins. The first method searches for closed loops inside the protein structure and uses Grübler–Kutzbach (GK) criterion. The second method is based on a modified 3D pebble game. Both methods are implemented in a matlab program and the step by step algorithms for both are discussed. We applied both methods on simple 3D structures to verify the methods. Also, we applied them on several protein molecules. The results show that both methods are calculating the same DOF and rigid and flexible regions. The main difference between two methods is the run time. It's shown that the first method (GK approach) is slower than the second method. The second method takes 0.29 s per amino acid versus 0.83 s for the first method to perform this rigidity analysis.

PEBBLE GAMES AND LINEAR EQUATIONS

We give a new, simplified and detailed account of the correspondence between levels of the Sherali–Adams relaxation of graph isomorphism and levels of pebble-game equivalence with counting (higher-dimensional Weisfeiler–Lehman colour refinement). The correspondence between basic colour refinement and fractional isomorphism, due to Tinhofer [22; 23] and Ramana, Scheinerman and Ullman [17], is re-interpreted as the base level of Sherali–Adams and generalised to higher levels in this sense by Atserias and Maneva [1] and Malkin [14], who prove that the two resulting hierarchies interleave. In carrying this analysis further, we here give (a) a precise characterisation of the level k Sherali–Adams relaxation in terms of a modified counting pebble game; (b) a variant of the Sherali–Adams levels that precisely match the k-pebble counting game; (c) a proof that the interleaving between these two hierarchies is strict. We also investigate the variation based on boolean arithmetic instead of real/rational arithmetic and obtain analogous correspondences and separations for plain k-pebble equivalence (without counting). Our results are driven by considerably simplified accounts of the underlying combinatorics and linear algebra.