-
Towards an Understanding of Long-Tailed Runtimes of SLS Algorithms
Authors:
Jan-Hendrik Lorenz,
Florian Wörz
Abstract:
The satisfiability problem is one of the most famous problems in computer science. Its NP-completeness has been used to argue that SAT is intractable. However, there have been tremendous advances that allow SAT solvers to solve instances with millions of variables. A particularly successful paradigm is stochastic local search.
In most cases, there are different ways of formulating the underlying…
▽ More
The satisfiability problem is one of the most famous problems in computer science. Its NP-completeness has been used to argue that SAT is intractable. However, there have been tremendous advances that allow SAT solvers to solve instances with millions of variables. A particularly successful paradigm is stochastic local search.
In most cases, there are different ways of formulating the underlying problem. While it is known that this has an impact on the runtime of solvers, finding a helpful formulation is generally non-trivial. The recently introduced GapSAT solver [Lorenz and Wörz 2020] demonstrated a successful way to improve the performance of an SLS solver on average by learning additional information which logically entails from the original problem. Still, there were cases in which the performance slightly deteriorated. This justifies in-depth investigations into how learning logical implications affects runtimes for SLS.
In this work, we propose a method for generating logically equivalent problem formulations, generalizing the ideas of GapSAT. This allows a rigorous mathematical study of the effect on the runtime of SLS solvers. If the modification process is treated as random, Johnson SB distributions provide a perfect characterization of the hardness. Since the observed Johnson SB distributions approach lognormal distributions, our analysis also suggests that the hardness is long-tailed. As a second contribution, we theoretically prove that restarts are useful for long-tailed distributions. This implies that additional restarts can further refine all algorithms employing above mentioned modification technique. Since the empirical studies compellingly suggest that the runtime distributions follow Johnson SB distributions, we investigate this property theoretically. We succeed in proving that the runtimes for Schöning's random walk algorithm are approximately Johnson SB.
△ Less
Submitted 24 October, 2022;
originally announced October 2022.
-
Too much information: why CDCL solvers need to forget learned clauses
Authors:
Tom Krüger,
Jan-Hendrik Lorenz,
Florian Wörz
Abstract:
Conflict-driven clause learning (CDCL) is a remarkably successful paradigm for solving the satisfiability problem of propositional logic. Instead of a simple depth-first backtracking approach, this kind of solver learns the reason behind occurring conflicts in the form of additional clauses. However, despite the enormous success of CDCL solvers, there is still only a limited understanding of what…
▽ More
Conflict-driven clause learning (CDCL) is a remarkably successful paradigm for solving the satisfiability problem of propositional logic. Instead of a simple depth-first backtracking approach, this kind of solver learns the reason behind occurring conflicts in the form of additional clauses. However, despite the enormous success of CDCL solvers, there is still only a limited understanding of what influences the performance of these solvers in what way.
Considering different measures, this paper demonstrates, quite surprisingly, that clause learning (without being able to get rid of some clauses) can not only help the solver but can oftentimes deteriorate the solution process dramatically. By conducting extensive empirical analysis, we furthermore find that the runtime distributions of CDCL solvers are multimodal. This multimodality can be seen as a reason for the deterioration phenomenon described above. Simultaneously, it also gives an indication of why clause learning in combination with clause deletion is virtually the de facto standard of SAT solving, in spite of this phenomenon. As a final contribution, we show that Weibull mixture distributions can accurately describe the multimodal distributions. Thus, adding new clauses to a base instance has an inherent effect of making runtimes long-tailed. This insight provides an explanation as to why the technique of forgetting clauses is useful in CDCL solvers apart from the optimization of unit propagation speed.
△ Less
Submitted 16 June, 2022; v1 submitted 1 February, 2022;
originally announced February 2022.
-
Evidence for Long-Tails in SLS Algorithms
Authors:
Florian Wörz,
Jan-Hendrik Lorenz
Abstract:
Stochastic local search (SLS) is a successful paradigm for solving the satisfiability problem of propositional logic. A recent development in this area involves solving not the original instance, but a modified, yet logically equivalent one. Empirically, this technique was found to be promising as it improves the performance of state-of-the-art SLS solvers.
Currently, there is only a shallow und…
▽ More
Stochastic local search (SLS) is a successful paradigm for solving the satisfiability problem of propositional logic. A recent development in this area involves solving not the original instance, but a modified, yet logically equivalent one. Empirically, this technique was found to be promising as it improves the performance of state-of-the-art SLS solvers.
Currently, there is only a shallow understanding of how this modification technique affects the runtimes of SLS solvers. Thus, we model this modification process and conduct an empirical analysis of the hardness of logically equivalent formulas. Our results are twofold. First, if the modification process is treated as a random process, a lognormal distribution perfectly characterizes the hardness; implying that the hardness is long-tailed. This means that the modification technique can be further improved by implementing an additional restart mechanism. Thus, as a second contribution, we theoretically prove that all algorithms exhibiting this long-tail property can be further improved by restarts. Consequently, all SAT solvers employing this modification technique can be enhanced.
△ Less
Submitted 1 July, 2021;
originally announced July 2021.
-
On the Effect of Learned Clauses on Stochastic Local Search
Authors:
Jan-Hendrik Lorenz,
Florian Wörz
Abstract:
There are two competing paradigms in successful SAT solvers: Conflict-driven clause learning (CDCL) and stochastic local search (SLS). CDCL uses systematic exploration of the search space and has the ability to learn new clauses. SLS examines the neighborhood of the current complete assignment. Unlike CDCL, it lacks the ability to learn from its mistakes. This work revolves around the question whe…
▽ More
There are two competing paradigms in successful SAT solvers: Conflict-driven clause learning (CDCL) and stochastic local search (SLS). CDCL uses systematic exploration of the search space and has the ability to learn new clauses. SLS examines the neighborhood of the current complete assignment. Unlike CDCL, it lacks the ability to learn from its mistakes. This work revolves around the question whether it is beneficial for SLS to add new clauses to the original formula. We experimentally demonstrate that clauses with a large number of correct literals w. r. t. a fixed solution are beneficial to the runtime of SLS. We call such clauses high-quality clauses.
Empirical evaluations show that short clauses learned by CDCL possess the high-quality attribute. We study several domains of randomly generated instances and deduce the most beneficial strategies to add high-quality clauses as a preprocessing step. The strategies are implemented in an SLS solver, and it is shown that this considerably improves the state-of-the-art on randomly generated instances. The results are statistically significant.
△ Less
Submitted 7 May, 2020;
originally announced May 2020.
