Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userAdvances in Symmetry Breaking for SAT Modulo Theories
262
0
0.0
(
0
)
Added by
Saket Dingliwal
Publication date
2019
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Symmetry breaking is a popular technique to reduce the search space for SAT solving by exploiting the underlying symmetry over variables and clauses in a formula. The key idea is to first identify sets of assignments which fall in the same symmetry class, and then impose ordering constraints, called Symmetry Breaking Predicates (SBPs), such that only one (or a small subset) of these assignments is allowed to be a solution of the original SAT formula. While this technique has been exploited extensively in the SAT literature, there is little work on using symmetry breaking for SAT Modulo Theories (SMT). In SMT, logical constraints in SAT theories are combined with another set of theory operations defined over non-Boolean variables such as integers, reals, etc. SMT solvers typically use a combination of SAT solving techniques augmented with calls to the theory solver. In this work, we take up the advances in SAT symmetry breaking and apply them to the domain of SMT. Our key technical contribution is the formulation of symmetry breaking over the Boolean skeleton variables, which are placeholders for actual theory operations in SMT solving. These SBPs are then applied over the SAT solving part of the SMT solver. We implement our SBP ideas on top of CVC4, which is a state-of-the-art SMT solver. Our approach can result in significantly faster solutions on several benchmark problems compared to the state-of-the-art. Our final solver is a hybrid of the original CVC4 solver, and an SBP based solver, and can solve up to 3.8% and 3.1% more problems in the QF_NIA category of 2018 and 2019 SMT benchmarks, respectively, compared to CVC4, the top performer in this category.
rate research
Read More
We introduce an approach that aims to combine the usage of satisfiability modulo theories (SMT) solvers with the Combinatory Logic Synthesizer (CL)S framework. (CL)S is a tool for the automatic composition of software components from a user-specified repository. The framework yields a tree grammar that contains all composed terms that comply with a target type. Type specifications for (CL)S are based on combinatory logic with intersection types. Our approach translates the tree grammar into SMT functions, which allows the consideration of additional domain-specific constraints. We demonstrate the usefulness of our approach in several experiments.
Over the last two decades, we have seen a dramatic improvement in the efficiency of conflict-driven clause-learning Boolean satisfiability (CDCL SAT) solvers on industrial problems from a variety of domains. The availability of such powerful general-purpose search tools as SAT solvers has led many researchers to propose SAT-based methods for cryptanalysis, including techniques for finding collisions in hash functions and breaking symmetric encryption schemes. Most of the previously proposed SAT-based cryptanalysis approaches are blackbox techniques, in the sense that the cryptanalysis problem is encoded as a SAT instance and then a CDCL SAT solver is invoked to solve the said instance. A weakness of this approach is that the encoding thus generated may be too large for any modern solver to solve efficiently. Perhaps a more important weakness of this approach is that the solver is in no way specialized or tuned to solve the given instance. To address these issues, we propose an approach called CDCL(Crypto) (inspired by the CDCL(T) paradigm in Satisfiability Modulo Theory solvers) to tailor the internal subroutines of the CDCL SAT solver with domain-specific knowledge about cryptographic primitives. Specifically, we extend the propagation and conflict analysis subroutines of CDCL solvers with specialized codes that have knowledge about the cryptographic primitive being analyzed by the solver. We demonstrate the power of this approach in the differential path and algebraic fault analysis of hash functions. Our initial results are very encouraging and reinforce the notion that this approach is a significant improvement over blackbox SAT-based cryptanalysis.
We study holographically Lifshitz-scaling theories with broken symmetries. In order to do this, we set up a bulk action with a complex scalar and a massless vector on a background which consists in a Lifshitz metric and a massive vector. We first study separately the complex scalar and the massless vector, finding a similar pattern in the two-point functions that we can compute analytically. By coupling the probe complex scalar to the background massive vector we can construct probe actions that are more general than the usual Klein--Gordon action. Some of these actions have Galilean boost symmetry. Finally, in the presence of a symmetry breaking scalar profile in the bulk, we reproduce the expected Ward identities of a Lifshitz-scaling theory with a broken global continuous symmetry. In the spontaneous case, the latter imply the presence of a gapless mode, the Goldstone boson, which will have dispersion relations dictated by the Lifshitz scaling.
QCD monopoles are magnetically charged quasiparticles whose Bose-Einstein condensation (BEC) at $T<T_c$ creates electric confinement and flux tubes. The magnetic scenario of QCD proposes that scattering on the non-condensed component of the monopole ensemble at $T>T_c$ plays an important role in explaining the properties of strongly coupled quark-gluon plasma (sQGP) near the deconfinement temperature. In this paper, we study the phenomenon of chiral symmetry breaking and its relation to magnetic monopoles. Specifically, we study the eigenvalue spectrum of the Dirac operator in the basis of fermionic zero modes in an SU(2) monopole background. We find that as the temperature approaches the deconfinement temperature $T_c$ from above, the eigenvalue spectrum has a finite density at $omega = 0$, indicating the presence of a chiral condensate. In addition, we find the critical scaling of the eigenvalue gap to be consistent with that of the correlation length in the 3d Ising model and the BEC transition of monopoles on the lattice.
We find stealth Schwarzschild solutions with a nontrivial profile of the scalar field regular on the horizon in the Einstein gravity coupled to the scalar field with the k-essence and/or generalized cubic galileon terms, which is a subclass of the Horndeski theory breaking the shift symmetry, where the propagation speed of gravitational waves coincides with the speed of light. After deriving sufficient conditions for the shift symmetry breaking theory to allow a general Ricci-flat metric solution with a nontrivial scalar field profile, we focus on the stealth Schwarzschild solution with the scalar field with or without time dependence. For the profile $phi=phi_0(r)$, we explicitly obtain two types of stealth Schwarzschild solutions, one of which is regular on the event horizon. The linear perturbation analysis clarifies that the kinetic term of the scalar mode identically vanishes, indicating that the scalar mode is strongly coupled. The absence of the kinetic term of the scalar mode in the quadratic action would inevitably arise for the stealth Schwarzschild solutions in the theory with a general scalar field profile depending only on the spatial coordinates. On the other hand, for the time-dependent scalar field profile, we clarify that there does not exist a stealth Schwarzschild solution in the shift symmetry breaking theories.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
