Learning-Sensitive Backdoors with Restarts
| Autor: | Jia Hui Liang, Vijay Ganesh, Krzysztof Czarnecki, Christoph M. Wintersteiger, Ruben Martins, Robert Robere, Edward Zulkoski |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Scheme (programming language)
Software_OPERATINGSYSTEMS Theoretical computer science Computer science 02 engineering and technology Mathematical proof 020202 computer hardware & architecture Through-the-lens metering 0202 electrical engineering electronic engineering information engineering Backjumping 020201 artificial intelligence & image processing Boolean satisfiability problem Heuristics computer Parametric statistics computer.programming_language |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783319983332 CP |
| DOI: | 10.1007/978-3-319-98334-9_30 |
| Popis: | Restarts are a pivotal aspect of conflict-driven clause-learning (CDCL) SAT solvers, yet it remains unclear when they are favorable in practice, and whether they offer additional power in theory. In this paper, we consider the power of restarts through the lens of backdoors. Extending the notion of learning-sensitive (LS) backdoors, we define a new parameter called learning-sensitive with restarts (LSR) backdoors. Broadly speaking, we show that LSR backdoors are a powerful parametric lens through which to understand the impact of restarts on SAT solver performance, and specifically on the kinds of proofs constructed by SAT solvers. First, we prove that when backjumping is disallowed, LSR backdoors can be exponentially smaller than LS backdoors. Second, we demonstrate that the size of LSR backdoors are dependent on the learning scheme used during search. Finally, we present new algorithms to compute upper-bounds on LSR backdoors that intrinsically rely upon restarts, and can be computed with a single run of a CDCL SAT solver. We empirically demonstrate that this can often produce much smaller backdoors than previous approaches to computing LS backdoors. We conclude with empirical results on industrial benchmarks which demonstrate that rapid restart policies tend to produce more “local” proofs than other heuristics, in terms of the number of unique variables found in learned clauses of the proof. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|