اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدOn Dedicated CDCL Strategies for PB Solvers
75
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Current implementations of pseudo-Boolean (PB) solvers working on native PB constraints are based on the CDCL architecture which empowers highly efficient modern SAT solvers. In particular, such PB solvers not only implement a (cutting-planes-based) conflict analysis procedure, but also complementary strategies for components that are crucial for the efficiency of CDCL, namely branching heuristics, learned constraint deletion and restarts. However, these strategies are mostly reused by PB solvers without considering the particular form of the PB constraints they deal with. In this paper, we present and evaluate different ways of adapting CDCL strategies to take the specificities of PB constraints into account while preserving the behavior they have in the clausal setting. We implemented these strategies in two different solvers, namely Sat4j (for which we consider three configurations) and RoundingSat. Our experiments show that these dedicated strategies allow to improve, sometimes significantly, the performance of these solvers, both on decision and optimization problems.
قيم البحث
اقرأ أيضاً
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.
There has been a recent surge of interest in nonparametric bandit algorithms based on subsampling. One drawback however of these approaches is the additional complexity required by random subsampling and the storage of the full history of rewards. Ou
r first contribution is to show that a simple deterministic subsampling rule, proposed in the recent work of Baudry et al. (2020) under the name of last-block subsampling, is asymptotically optimal in one-parameter exponential families. In addition, we prove that these guarantees also hold when limiting the algorithm memory to a polylogarithmic function of the time horizon. These findings open up new perspectives, in particular for non-stationary scenarios in which the arm distributions evolve over time. We propose a variant of the algorithm in which only the most recent observations are used for subsampling, achieving optimal regret guarantees under the assumption of a known number of abrupt changes. Extensive numerical simulations highlight the merits of this approach, particularly when the changes are not only affecting the means of the rewards.
Equation systems resulting from a p-version FEM discretisation typically require a special treatment as iterative solvers are not very efficient here. Applying hierarchical concepts based on a nested dissection approach allow for both the design of s
ophisticated solvers as well as for advanced parallelisation strategies. To fully exploit the underlying computing power of parallel systems, dynamic load balancing strategies become an essential component.
New colorless electroweak (EW) charged spin-1 particles with mass of a few TeV arise in numerous extensions of the Standard Model (SM). Decays of such a vector into a pair of SM particles, either fermions or EW bosons, are well studied. Many of these
models have an additional scalar, which can lead to (and even dominate in certain parameter regions) a novel decay channel for the heavy vector particles instead - into a SM EW boson and the scalar, which subsequently decays into a SM EW boson pair. In this work, we focus on the scalar being relatively heavy, roughly factor of two lighter than the vector particles, rendering its decay products well separated. Such a cascade decay results in a final state with three isolated bosons. We argue that for this triboson signal the existing diboson searches are not quite optimal due to combinatorial ambiguity for three identical bosons, and in addition, due to a relatively small signal cross-section determined by the heaviness of the decaying vector particle. In order to isolate the signal, we demonstrate that tagging all three bosons, followed by use of the full triboson invariant mass distribution as well as that of appropriate subsets of dibosons, is well motivated. We develop these general strategies in detail within the context of a specific class of models that are based on extensions of the standard warped extra-dimensional scenario. We also point out that a similar analysis would apply to models with an enlarged EW gauge sector in four dimensions, even if they involve a different Lorentz structure for the relevant couplings.
Recent research has shown that a single arbitrarily efficient solver can be significantly outperformed by a portfolio of possibly slower on-average solvers. The solver selection is usually done by means of (un)supervised learning techniques which exp
loit features extracted from the problem specification. In this paper we present an useful and flexible framework that is able to extract an extensive set of features from a Constraint (Satisfaction/Optimization) Problem defined in possibly different modeling languages: MiniZinc, FlatZinc or XCSP. We also report some empirical results showing that the performances that can be obtained using these features are effective and competitive with state of the art CSP portfolio techniques.
الأسئلة المقترحة
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
