Relating Complexity-theoretic Parameters with SAT Solver Performance
Over the years complexity theorists have proposed many structural parameters to explain the surprising efficiency of conflict-driven clause-learning (CDCL) SAT solvers on a wide variety of large industrial Boolean instances. While some of these parameters have been studied empirically, until now there has not been a unified comparative study of their explanatory power on a comprehensive benchmark. We correct this state of affairs by conducting a large-scale empirical evaluation of CDCL SAT solver performance on nearly 7000 industrial and crafted formulas against several structural parameters such as backdoors, treewidth, backbones, and community structure. Our study led us to several results. First, we show that while such parameters only weakly correlate with CDCL solving time, certain combinations of them yield much better regression models. Second, we show how some parameters can be used as a "lens" to better understand the efficiency of different solving heuristics. Finally, we propose a new complexity-theoretic parameter, which we call learning-sensitive with restarts (LSR) backdoors, that extends the notion of learning-sensitive (LS) backdoors to incorporate restarts and discuss algorithms to compute them. We mathematically prove that for certain class of instances minimal LSR-backdoors are exponentially smaller than minimal-LS backdoors.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Prevention is Better than Cure: Handling Basis Collapse and Transparency in Dense Networks
Dense nets are an integral part of any classification and regression problem. Recently, these networks have found a new application as solvers for known representations in various domains. However, one crucial issue with…
Performance-Guaranteed ODE Solvers with Complexity-Informed Neural Networks
Traditionally, we provide technical parameters for ODE solvers, such as the order, the stepsize and the local error threshold. However, there is no for performance metrics that users care about, such as the time consumpt…
Provable Target Sample Complexity Improvements as Pre-Trained Models Scale
Pre-trained models have become indispensable for efficiently building models across a broad spectrum of downstream tasks. The advantages of pre-trained models have been highlighted by empirical studies on scaling laws, w…
parameter-efficient fine-tuningStructure from Motion on a Sphere
We describe a special case of structure from motion where the camera rotates on a sphere. The camera's optical axis lies perpendicular to the sphere's surface. In this case, the camera's pose is minimally represented by …
On the Local Complexity of Linear Regions in Deep ReLU Networks
We define the local complexity of a neural network with continuous piecewise linear activations as a measure of the density of linear regions over an input data distribution. We show theoretically that ReLU networks that…
Adversarial Robustness