Theoretical Foundation of Solvers: Context, Directions and Open Problems
Vijay Ganesh (University of Waterloo), Laurent Simon (Bordeaux INP), and David Mitchell (Simon Fraser University)
5365 - 5376 of 19959 Results
Format results
Positive Moments for Scattering Amplitudes
Francesco Riva University of Geneva (UNIGE) - Department of Theoretical Physics
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
Theoretical Foundation of Solvers: Context, Directions and Open Problems
Vijay Ganesh (University of Waterloo), Laurent Simon (Bordeaux INP), and David Mitchell (Simon Fraser University)Topics: Vijay Ganesh: Perspectives on Practice and Theory of SAT Solving Abstract: Over the last two decades, SAT solvers have revolutionized many sub-fields of software engineering, security, and AI. This is largely due to a dramatic improvement in the scalability of these solvers vis-a-vis large real-world formulas. What is surprising is that the Boolean satisfiability problem is NP-complete, believed to be intractable, and yet these solvers easily solve industrial instances containing millions of variables and clauses in them. How can that be? In my talk, I will briefly survey what we know about the power of SAT solvers through the lens of parameterized and proof complexity, as well as how we can build better SAT solvers by combining machine learning and proof systems. Laurent Simon: Towards an (experimental) Understanding of SAT Solvers Abstract: Despite important progresses in the practical solving of SAT problems, the behavior of CDCL solvers are only partially understood. In this talk, we will review some of the experimental studies that have been conducted so far, uncovering some surprising structures CDCL solvers are working on. David Mitchell: On Using Structural Properties to Improve CDCL Solver Performance Abstract: Instance structure is widely discussed and studied in the SAT solving community, but has never been explicitly made use of in dominant "industrial" SAT solvers. We briefly review some structural properties of CNF formulas that have received attention, and some recent efforts to improve CDCL SAT solver performance using these properties.Positive Moments for Scattering Amplitudes
Francesco Riva University of Geneva (UNIGE) - Department of Theoretical Physics
I will discuss the conditions satisfied by the 2 → 2 scattering amplitude in unitarity and causal theories, presenting a simple formulation in term of moments of a positive measure. I will identify complete subsets of two-sided constraints, suitable to bound Effective Field Theories (EFTs) at any finite order in the energy expansion. I will also discuss the importance of IR loop effects on these bounds. A consequence of this study is that EFTs in which the scattering amplitude in some regime grows in energy faster than E6 (e.g. higher spin particles with masses smaller than their inverse size) cannot be UV-completed.
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.