资源论文On the Empirical Time Complexity of Random 3-SAT at the Phase Transition

On the Empirical Time Complexity of Random 3-SAT at the Phase Transition

2019-11-18 | |  61 |   62 |   0
Abstract The time complexity of problems and algorithms, i.e., the scaling of the time required for solving a problem instance as a function of instance size, is of key interest in theoretical computer science and practical applications. In this context, propositional satisfiability (SAT) is one of the most intensely studied problems, and it is generally believed that solving SAT requires exponential time in the worst case. For more than two decades, random 3-SAT at the solubility phase transition has played a pivotal role in the theoretical and empirical investigation of SAT solving, and to this day, it is arguably the most prominent model for difficult SAT instances. Here, we study the empirical scaling of the running time of several prominent, high-performance SAT solvers on random 3-SAT instances from the phase transition region. After introducing a refined model for the location of the phase transition point, we show that the median running time of three incomplete, SLS-based solvers – WalkSAT/SKC, BalancedZ and probSAT – scales polynomially with instance size. An analogous analysis of three complete, DPLL-based solvers – kcnfs, march_hi and march_br – clearly indicates exponential scaling of median running time. Moreover, exponential scaling is witnessed for these DPLL-based solvers when solving only satisfiable and only unsatisfiable instances, and the respective scaling models for each solver differ mostly by a constant factor.

上一篇:Towards Automatic Dominance Breaking for Constraint Optimization Problems

下一篇:Efficient Operations on MDDs for Building Constraint Programming Models

用户评价
全部评价

热门资源

  • The Variational S...

    Unlike traditional images which do not offer in...

  • Learning to Predi...

    Much of model-based reinforcement learning invo...

  • Stratified Strate...

    In this paper we introduce Stratified Strategy ...

  • A Mathematical Mo...

    Direct democracy, where each voter casts one vo...

  • Rating-Boosted La...

    The performance of a recommendation system reli...