Format results
The Rise of Approximate Model Counting: Beyond Classical Theory and Practice of SAT
Kuldeep Meel (National University of Singapore)Stellar streams in the Gaia era
Vasily Belokurov University of Cambridge
Correlations and topology in the magic angle twisted bilayer graphene
Oskar Vafek Florida State University
Finite quantum geometry, octonions and the theory of fundamental particles.
Michel Dubois-Violette University of Paris-Saclay
Welcome and Opening Remarks
Kirill Krasnov University of Nottingham
Reactive Synthesis
Bernd Finkbeiner (CISPA Helmholtz Center for Information Security)Using SAT Solvers to Prevent Causal Failures in the Cloud
Ruzica Piskac (Yale University)Gravity Gradient Noise from Asteroids
Michael Fedderke Perimeter Institute for Theoretical Physics
Approximate Counting and Sampling
Kuldeep Meel (National University of Singapore)
Tackling the challenges of galaxy-dark matter connection modeling and new insights into secondary (assembly) biases
Sihan Yuan Harvard University
Modeling galaxy-dark matter connection is essential in deriving unbiased cosmological constraints from galaxy clustering observations. We show that a more physically motivated galaxy-dark matter incorporating secondary (assembly) biases results in more accurate predictions of galaxy clustering, yields novel insights into effects such as baryonic feedback, and significantly reduces the tension in galaxy lensing. We further present progress and opportunities in building a multi-tracer galaxy-dark matter connection framework that is rich in features and highly efficient, enabling more robust cosmological analyses with upcoming DESI data.
The Rise of Approximate Model Counting: Beyond Classical Theory and Practice of SAT
Kuldeep Meel (National University of Singapore)Approximate Model Counting asks to compute the number of solutions of a formula F within a desired tolerance and confidence. While the earliest algorithmic ideas go back to the seminal work in the 1980's, scalable approximate counters were elusive until recently. In this talk, we will shed light on what makes the state of the art counters such as ApproxMC tick. In particular, we will illustrate how algorithmic frameworks' design needs considerations beyond the classical theory. The practical realization of these frameworks requires one to go beyond the traditional CNF solving.Stellar streams in the Gaia era
Vasily Belokurov University of Cambridge
Stellar streams are a powerful tool for mapping of the Galactic matter distribution. Thanks to Gaia we now have full 6D (complete phase-space) view of a quickly growing subset of the Milky Way streams. These stars are precious as they can shed light not only on the broad-brush structure of the Galaxy, but also reveal small time-evolving perturbations of the Galactic potential. I will use the Sagittarius and the Orphan streams to present the most recent measurements of the dark matter halo of the Milky Way and one of its sub-halos.
Correlations and topology in the magic angle twisted bilayer graphene
Oskar Vafek Florida State University
When the twist angle of a bilayer graphene is near the ``magic'' value, there are four narrow bands near the neutrality point, each two-fold spin degenerate. These bands are separated from the rest of the bands by energy gaps. In the first part of the talk, the topology of the narrow bands will be discussed, as well as the associated obstructions --or lack there of -- to construction of a complete localized basis [1,3].
In the second part of the talk, I will present a two stage renormalization group treatment [4] which connects the continuum Hamiltonian at length scales shorter than the moire superlattice period to the Hamiltonian for the active narrow bands only, which is valid at distances much longer than the moire period. Via a progressive numerical elimination of remote bands the relative strength of the one-particle-like dispersion and the interactions within the active narrow band Hamiltonian will be determined, thus quantifying the residual correlations and justifying the strong coupling approach in the final step.
In the last part of the talk, the states favored by electron-electron Coulomb interactions within the narrow bands will be discussed. Analytical and DMRG results based on 2D localized Wannier states [2,5], 1D localized hybrid Wannier states [3] and Bloch states [3,4] will be compared. Topological and symmetry constraints on the spectra of charged and neutral excitation[4] for various ground states, as well as non-Abelian braiding of Dirac nodes[3] , will also be presented.
[1] Jian Kang and Oskar Vafek, Phys. Rev. X 8, 031088 (2018).
[2] Jian Kang and Oskar Vafek, Phys. Rev. Lett. 122, 246401 (2019)
[3] Jian Kang and Oskar Vafek, Phys. Rev. B 102, 035161 (2020)
[4] Oskar Vafek and Jian Kang Phys. Rev. Lett. 125, 257602 (2020)
[5] Bin-Bin Chen, Yuan Da Liao, Ziyu Chen, Oskar Vafek, Jian Kang, Wei Li, Zi Yang Meng arXiv:2011.07602
Finite quantum geometry, octonions and the theory of fundamental particles.
Michel Dubois-Violette University of Paris-Saclay
We will describe an approach to the theory of fundamental particlesbased on finite-dimensional quantum algebras of observables. We will explain why the unimodularity of the color group suggests an interpretation of the quarklepton symmetry which involves the octonions and leads to the quantum spaces underlying the Jordan algebras of octonionic hermitian 2 × 2 and 3 × 3 matrices as internal geometry for fundamental particles. In the course of this talk, we will remind shortly why the finite-dimensional algebras of observables are the finite-dimensional euclidean Jordan agebras and we will describe their classifications. We will also explain our differential calculus on Jordan algebras and the theory of connections on Jordan modules. It is pointed out that the above theory of connections implies potentially a lot of scalar particles.
Welcome and Opening Remarks
Kirill Krasnov University of Nottingham
Reactive Synthesis
Bernd Finkbeiner (CISPA Helmholtz Center for Information Security)Reactive synthesis is the problem of translating a logical specification into a reactive system that is guaranteed to satisfy the specification for all possible behaviors of its environment. More than 60 years after its introduction by Alonzo Church, the synthesis problem is still one of the most intriguing challenges in the theory of reactive systems. Recent years have brought advances both in reasoning methods that can be used as tools in the synthesis process and in the synthesis approaches themselves. As a result, the complexity of the synthesized systems has risen steadily. However, the logical and algorithmic foundations of the synthesis problem are still far from complete. In this tutorial, I will give an overview of both the classic constructions and more recent ideas such as bounded synthesis and the synthesis of distributed systems. In the latter, we try to find a combination of process implementations that jointly guarantee that a given specification is satisfied. A reduction from multi-player games shows that the problem is in general undecidable. Despite this negative result, there is a long history of discoveries where the decidability of the synthesis problem was established for distributed systems with specific architectures, although usually with high computational cost. Compositional approaches and new specification languages like HyperLTL, which offer a more comprehensive logical representation of the distributed synthesis problem, are potential ways forward.Using SAT Solvers to Prevent Causal Failures in the Cloud
Ruzica Piskac (Yale University)Today's cloud systems heavily rely on redundancy for reliability. Nevertheless, as cloud systems become ever more structurally complex, independent infrastructure components may unwittingly share deep dependencies. These unexpected common dependencies may result in causal failures that undermine redundancy efforts. The state-of-the-art efforts, e.g., post-failure forensics, not only lead to prolonged failure recovery time in the face of structurally complex systems, but also fail to avoid expensive service downtime. We describe RepAudit, an auditing system which builds on the so-called fault graph, to identify causal failures in the cloud. To ensure the practicality, efficiency, and accuracy of our approach, we further equip RepAudit with a domain-specific auditing language framework, a set of high-performance auditing primitives. We leverage SAT solvers to construct efficient fault graph analysis algorithms. To empirically evaluate this claim, we run RepAudit on a real-world cloud storage dataset and we observed that RepAudit is 300 times more efficient than other state-of-the-art auditing tools. RepAudit technique has been used in Alibaba Group---the system is named CloudCanary---to perform real-time audits on service update scenarios to identify the root causes of correlated failure risks, and generate improvement plans with increased reliability. CloudCanary has successfully detected various correlated failure risks such as single-point microservice, common power source, and shared network components, preventing service outages ahead of time. The talk will conclude with an overview of the state of the arts on network verification community which widely relies on using SAT/SMT solver to check the correctness of network behaviors. References: [1] Ennan Zhai, Ruichuan Chen, David Isaac Wolinsky, Bryan Ford: Heading Off Correlated Failures through Independence-as-a-Service. OSDI 2014: 317-334 [2] Ennan Zhai, Ruzica Piskac, Ronghui Gu, Xun Lao, Xi Wang: An auditing language for preventing correlated failures in the cloud. PACMPL 1(OOPSLA): 97:1-97:28 (2017) This talk will be given in collaboration with Ennan Zhai, a researcher at Alibaba Group.Gravity Gradient Noise from Asteroids
Michael Fedderke Perimeter Institute for Theoretical Physics
The gravitational coupling of nearby massive bodies to test masses in a gravitational wave (GW) detector cannot be shielded, and gives rise to 'gravity gradient noise’ (GGN) in the detector. In this talk, I will discuss how any GW detector using local test masses in the Inner Solar System is subject to GGN from the motion of the field of 10^5 Inner Solar System asteroids, which presents an irreducible noise floor for the detection of GW that rises exponentially at low frequencies. This severely limits prospects for GW detection using local test masses for frequencies below (few) x 10^{-7} Hz. At higher frequencies, I’ll show that the asteroid GGN falls rapidly enough that detection may be possible; however, the incompleteness of existing asteroid catalogs with regard to small bodies makes this an open question around microHz frequencies, and I’ll outline why further study is warranted here. Additionally, I’ll mention some prospects for GW detection in the ~10 nHz-microHz band that could evade this noise source.
Programming Z3
Nikolaj Björner (Microsoft Research)This tutorial provides a programmer's introduction to Satisfiability Modulo Theories based on Z3. It illustrates how to define and solve SMT problems using scripts and walks through algorithms using exposed functionality. Pre-recorded videos not available for Friday session.Approximate Counting and Sampling
Kuldeep Meel (National University of Singapore)Pre-recorded videos not available for Friday session. The availability of efficient SAT solvers presents opportunity for designing techniques for problems "beyond SAT". We will discuss two such problems that have witnessed increase in interest over the past decade: counting and sampling. Given a formula, the problem of counting is to compute the total number of solutions while sampling seeks to sample solutions uniformly at random. Counting and sampling are fundamental problems with applications such as probabilistic reasoning, information leakage, verification, and the like. In this talk, we will discuss approach that combines the classical ideas of universal hashing with CDCL solvers to design scalable approximate counters and samplers.Einstein's Equivalence principle for superpositions of gravitational fields
Flaminia Giacomini ETH Zurich
The Principle of Equivalence, stating that all laws of physics take their special-relativistic form in any local inertial frame, lies at the core of General Relativity. Because of its fundamental status, this principle could be a very powerful guide in formulating physical laws at regimes where both gravitational and quantum effects are relevant. However, its formulation implicitly presupposes that reference frames are abstracted from classical systems (rods and clocks) and that the spacetime background is well defined. Here, we we generalise the Einstein Equivalence Principle to quantum reference frames (QRFs) and to superpositions of spacetimes. We build a unitary transformation to the QRF of a quantum system in curved spacetime, and in a superposition thereof. In both cases, a QRF can be found such that the metric looks locally flat. Hence, one cannot distinguish, with a local measurement, if the spacetime is flat or curved, or in a superposition of such spacetimes. This transformation identifies a Quantum Local Inertial Frame. These results extend the Principle of Equivalence to QRFs in a superposition of gravitational fields. Verifying this principle may pave a fruitful path to establishing solid conceptual grounds for a future theory of quantum gravity.