Главная » Просмотр файлов » Learning Rate Based Branching Heuristic for SAT Solvers

Learning Rate Based Branching Heuristic for SAT Solvers (1185836)

Файл №1185836 Learning Rate Based Branching Heuristic for SAT Solvers (Презентации лекций)Learning Rate Based Branching Heuristic for SAT Solvers (1185836)2020-08-25СтудИзба
Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Learning Rate Based Branching Heuristic forSAT SolversJia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof CzarneckiUniversity of Waterloo, Waterloo, CanadaAbstract. In this paper, we propose a framework for viewing solverbranching heuristics as optimization algorithms where the objective isto maximize the learning rate, defined as the propensity for variablesto generate learnt clauses.

By viewing online variable selection in SATsolvers as an optimization problem, we can leverage a wide variety ofoptimization algorithms, especially from machine learning, to design effective branching heuristics. In particular, we model the variable selectionoptimization problem as an online multi-armed bandit, a special-case ofreinforcement learning, to learn branching variables such that the learning rate of the solver is maximized. We develop a branching heuristic thatwe call learning rate branching or LRB, based on a well-known multiarmed bandit algorithm called exponential recency weighted average andimplement it as part of MiniSat and CryptoMiniSat. We upgrade theLRB technique with two additional novel ideas to improve the learningrate by accounting for reason side rate and exploiting locality. The resulting LRB branching heuristic is shown to be faster than the VSIDS andconflict history-based (CHB) branching heuristics on 1975 applicationand hard combinatorial instances from 2009 to 2014 SAT Competitions.We also show that CryptoMiniSat with LRB solves more instances thanthe one with VSIDS.

To the best of our knowledge, the VSIDS branchingheuristic and its variants have been the dominant class of such heuristicsfor SAT solvers since 2001, until we introduced a novel class of machinelearning based branching heuristics.1IntroductionModern Boolean SAT solvers are a critical component of many innovative techniques in security, software engineering, hardware verification, and AI such assolver-based automated testing with symbolic execution [9], bounded modelchecking [11] for software and hardware verification, and planning in AI [27]respectively.

Conflict-driven clause-learning (CDCL) SAT solvers [29, 23, 24, 4,12, 6] in particular have made these techniques feasible as a consequence oftheir surprising efficacy at solving large classes of real-world Boolean formulas.The development of various heuristics, notably the Variable State IndependentDecaying Sum (VSIDS) [24] branching heuristic (and its variants) and conflictanalysis techniques [23], have dramatically pushed the limits of CDCL solverperformance. The VSIDS heuristic is used in the most competitive CDCL SATsolvers such as Glucose [4], Lingeling [6], and CryptoMiniSat [29].

Since its introduction in 2001, VSIDS has remained one of the most effective and dominant branching heuristic despite intensive efforts by many researchers to replaceit [16, 7, 28, 15]. In 2015, we provided the first branching heuristic, we call conflict history-based (CHB) branching heuristic, that was much more effective thanVSIDS. The branching heuristic introduced in this paper, which we refer to aslearning rate branching (LRB), significantly outperforms CHB and VSIDS.In this paper, we introduce a general principle for designing branching heuristics wherein online variable selection in SAT solvers is viewed as an optimizationproblem. The objective to be maximized is called the learning rate (LR), a numerical characterization of a variable’s propensity to generate learnt clauses.The goal of the branching heuristic, given this perspective, is to select branchingvariables that will maximize the cumulative LR during the run of the solver.

Intuitively, achieving a perfect LR of 1 implies the assigned variable is responsiblefor every learnt clause generated during its lifetime on the assignment trail.We put this principle into practice in this paper. Although there are manyalgorithms for solving optimization problems, we show that multi-armed banditlearning (MAB) [31], a special-case of reinforcement learning, is particularly effective in our context of selecting branching variables. In MAB, an agent selectsfrom a set of actions to receive a reward. The goal of the agent is to maximize the cumulative rewards received through the selection of actions. As wewill describe in more details later, we abstract the branching heuristic as theagent, the available branching variables are abstracted as the actions, and LR isdefined to be the reward.

Abstracting online variable selection as a MAB problem provides the bridge to apply MAB algorithms from the literature directlyas branching heuristics. In our experiments, we show that the MAB algorithmcalled exponential recency weighted average (ERWA) [31] in our abstraction surpasses the VSIDS and CHB branching heuristics at solving the benchmarks fromthe 4 most recent SAT Competitions in an apple-to-apple comparison.

Additionally, we provide two extensions to ERWA that increases its ability to maximizeLR and its performance as a branching heuristic. The final branching heuristic, called learning rate branching (LRB), is shown to dramatically outperformCryptoMiniSat [29] with VSIDS.1.1ContributionsContribution I: We define a principle for designing branching heuristics, thatis, a branching heuristic should maximize the learning rate (LR). We showthat this principle yields highly competitive branching heuristics in practice.Contribution II: We show how to abstract online variable selection in themulti-armed bandit (MAB) framework.

This abstraction provides an interface for applying MAB algorithms directly as branching heuristics. Previously, we developed the conflict history-based (CHB) branching heuristic [19],also inspired by MAB. The key difference between this paper and CHB isthat in the case of CHB the rewards are known a priori, and there is nometric being optimized. Whereas in this work, the learning rate is beingmaximized and is unknown a priori, which requires a bona fide machinelearning algorithm to optimize under uncertainty.Contribution III: We use the MAB abstraction to develop a new branchingheuristic called learning rate branching (LRB). The heuristic is built ona well-known MAB algorithm called exponential recency weighted average(ERWA). Given our domain knowledge of SAT solving, we extend ERWAto take advantage of reason side rate and locality [20] to further maximizethe learning rate objective.

We show in comprehensive apple-to-apple experiments that it outperforms the current state-of-the-art VSIDS [24] andCHB [19] branching heuristics on 1975 instances from four recent SAT Competition benchmarks from 2009 to 2014 on the application and hard combinatorial categories.

Additionally, we show that a modified version of CryptoMiniSat with LRB outperforms Glucose, and is very close to matchingLingeling over the same set of 1975 instances.22.1PreliminariesSimple Average and Exponential Moving AverageGiven a time series of Pnumbers hr1 , r1 , r2 , ..., rn i, the simple average is computednas avg(hr1 , ..., rn i) = i=1 n1 ri . Note that every ri is given the same coefficient(also called weight) of n1 .In a time series however, recent data is more pertinent to the current situation than old data. For example, consider a time series of the price of a stock. Theprice of the stock from yesterday is more correlated with today’s price than theprice of the stock from a year ago. The exponential moving average (EMA) [8] follows this intuition by giving the recent data higher weights than past data whenaveraging.

Incidentally, the same intuition is built into the multiplicativedecay inPnVSIDS [5, 20]. The EMA is computed as emaα (hr1 , ..., rn i) = i=1 α(1−α)n−i riwhere 0 < α < 1 is called the step-size parameter. α controls the relativeweights between recent and past data. EMA can be computed incrementallyas emaα (hr1 , ..., rn i) = (1 − α) · emaα (hr1 , ..., rn−1 i) + αrn , and we define thebase case emaα (hi) = 0.2.2Multi-Armed Bandit (MAB)We will explain the MAB problem [31] through a classical analogy. Consider agambler in a casino with n slot machines, where the objective of the gambleris to maximize payouts received from these machines.

Характеристики

Тип файла
PDF-файл
Размер
425 Kb
Тип материала
Высшее учебное заведение

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций

Свежие статьи
Популярно сейчас
А знаете ли Вы, что из года в год задания практически не меняются? Математика, преподаваемая в учебных заведениях, никак не менялась минимум 30 лет. Найдите нужный учебный материал на СтудИзбе!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
6510
Авторов
на СтудИзбе
302
Средний доход
с одного платного файла
Обучение Подробнее