Following our comparison of the efficiency of SAT-solvers [19, 20], we analyse DIMACS input files previously generated for benchmarking purposes in an attempt to pinpoint some common characteristics for the CNF formulas that were relatively easier to process, i.e., were verified faster than comparable instances of the same size.
Since the early 1970s, when Cooke first proved it to be NP-complete, the Boolean
satisfiability problem, or SAT, has undergone a dramatic rise in importance. From the
subject of purely theoretical research in the area of computational complexity,
SATsolving algorithms have become the cornerstone of a broad range of important practical
applications that rely on their efficiency. They include, but are not limited to: verification
[
In our recent papers [
The focus of this paper is not on SAT-solvers as such, but rather, on the input Boolean formulas themselves. Specifically, we will investigate CNF formulas that are comparatively easier or harder to verify compared to other generated instances of the same size, attempting to identify some common patterns in their properties. Given that this area that has not really been previously explored, this work is aiming to be an initial, small step rather than an exhaustive investigation.
The rest of this paper is organized as follows. The next section summarises existing work related to the subject. Section 3 shortly presents DIMACS, the standardised input format used by SAT-solvers, as well as details the generation and analysis of input CNF formulas. In Section 4 experimental results are compared and discussed. The final section contains conclusions.
In this section we discuss prior research into the difficulty of randomly generated instances of NP-complete problems.
Many well-known, classical computational problems, though NP-complete, are
relatively easy to solve when it comes to typical instances [
It has been long observed that certain specific instances of SAT pose an
unusually significant challenge to the the DPLL algorithm, contrary to perceived average
difficulty. In [
This phase transition is investigated further by Gent and Walsh in [
Gent and Walsh postulate the ’constraint gap’ to cause such unexpectedly hard problems to occur in an otherwise satisfiable region. In the DPLL algorithm, neither unit propagation nor pure literal elimination ever branch out the search, leaving splitting (i.e., the choice of the branching literal) as the only critical point which can potentially result in an exponential blow-up in the number of explored assignments. This naturally leads to the conclusion that the harder the instance, the more the algorithm is forced to use the splitting rule compared to the other two. In other words, the hardest instances are ’constrained’ in the sense they have just enough constraints to be unsatisfiable, but very few more (or even none), forcing DPLL to utilize heuristics-based branching and thus increasing verification time dramatically.
These results were further experimentally confirmed in other papers, including
analyses for 3-SAT formulas by Larrabee and Tsuji [
In this section we present the DIMACS input format commonly used by SAT-solvers, discuss the input files used for our analysis and the factors taken into account during the latter.
The renewed scientific interest in the Boolean satisfiability problem, and in particular the emergence of SAT Competitions in the early 2000s, resulted in the need of a single, unified input file format. DIMACS has become such a standard.
The format uses plain text to represent a Boolean formula in conjunctive normal form (CNF). Following an optional comment line and a header containing the number of clauses and literals in the formula, each subsequent line corresponds to a new clause. Variables are represented by subsequent natural numbers, with the minus sign denoting negation. Spaces separate literals in clauses, and zeroes signal end of clause. An example of a very simple CNF formula in the DIMACS format is shown below. Listing 1.1. The input file corresponding to a simple formula (x1 _ :x3) ^ (x2 _ x3 _ :x1) c Example DIMACS i n p u t p c n f 3 2 1 3 0 2 3 1 0
The input files contain formulas resulting from the translations to SAT of several
NP-complete problems, including classical graph problems (vertex coloring, vertex
cover, Hamiltonian path) [
For the purposes of this analysis, we have identified and separated groups of the
most and least difficult instances for each of the aforementioned problems, that is, the
input files whose processing required the most and the least time, respectively. When
calculating verification time, the average of individual solvers’ processing times was
considered. The solvers used were the same as in the aforementioned comparison:
Lingeling and Plingeling [
The DIMACS files in both groups were subsequently analysed and compared w.r.t. factors such as total number of literals and clauses, average and maximum clause length, percentage of negative literals and percentage of Horn clauses. 4
In this section we discuss and compare the results of our analysis.
In Tab. 1, several characteristics are compared between the groups of easiest and hardest generated instances of vertex k-colouring and vertex k-cover. For the former, parameters of n = 100 (graph size) and k = 10 (number of colours) were set. For the latter, graphs of size n = 50 were generated, with the vertex cover size at k = 30. Avg running time Avg number of clauses Avg number of literals Avg clause size Longest clause Negative literals Horn clauses
Vertex k-colouring Vertex k-cover Easier instances Harder instances Easier instances Harder instances 0.018 s 364.759 s 0.108 s 38.941 s 24507 36007 36774 36994 49813 72813 74967 88127 2.033 2.022 2.039 2.382
10 10 60 60 97.96% 98.63% 98.04% 83.41%
0% 0% 99.03% 99.34%
It can be observed that the characteristics of hard instances depend primarily on the computational problem and its specific translation to SAT. For instance, in the vertex k-colouring problem, they have up to 50% more literals and clauses. This in turn can be attributed to the randomly generated input graphs for these instances having significantly more edges, and as such requiring more constraints in the form of clauses. Notably, despite the overwhelming majority of literals in both groups of instances being negative, there are no Horn clauses, again due to the specifics of the SAT encoding.
On the other hand, for vertex k-cover the average number of clauses is roughly the same in easy and hard instances. However, the number of literals, and thus average clause length, is generally higher (up to 15%) in the latter group. Furthermore, an even more noteworthy difference is in the percentage of negative literals, which is also around 15% lower, suggesting that the extra literals in hard instances are positive.
In the same way, Tab. 2 compares instances of the Hamiltonian path problem and the extended string-to-string correction problem (ESCP). For the former, generated graphs were of size n = 200, whereas the parameters for ESCP were set as n = 20 (length of input strings), k = 15 (maximum number of operations) and l = 5 (alphabet size).
In the case of the Hamiltonian path problem, the harder instances actually have less literals and thus, on average, shorter clauses. This, too, is consistent with the nature of the problem in question: fewer edges (and thus shorter conditional clauses in the resultant formula) make for a graph that is harder to find a Hamiltonian path, while the most trivial satisfiable instance is actually one in which all possible edges exist.
Finally, in the comparison of ESCP instances, all analysed characteristics are virtually identical, further emphasising the lack of any clear pattern behind the relative difficulty of specific instances of SAT.
It is important to note that our analysis is not yet another attempt to back up the the findings previously described in Section 2, i.e., the existence of a phase transition and a ’constraint gap’ at the boundary between regions of expected (un)satisfiability. Instead of considering the distribution of difficulty across some order parameter, we took into account benchmarks generated using the same settings, i.e., the same order parameter, in an attempt to pinpoint patterns related to the composition of the formulas themselves. However, it clearly appears that the differences are related to the specific characteristics of computational problems translated to SAT. 5
We have analysed Boolean formulas in CNF, representing translations of well-known NP-complete problems to SAT. The input files were grouped depending on their average processing time by SAT-solvers, and compared on several factors, including average clause length and percentage of Horn clauses, between the easiest and most difficult instances.
There do not appear to be easily noticeable global characteristics of CNF formulas representing harder instances of NP-complete problems. Depending on the specific problem and its translation to SAT, the formulas whose processing takes longer can, for instance, have longer clauses, or conversely, more clauses of similar average length to that in the ’easier’ group. Similarly, the percentage of negative literals or Horn clauses are also dependent on the NP-complete problem translated to SAT, and not some pattern prevalent across all comparatively easier or harder instances.
These observations seem in line with SAT being NP-complete, and as such, a difficult computational problem. Just as there is not a single SAT-solver always offering superior performance, no single factor contributes to a particular instance of SAT being comparatively easier or harder to verify than others of same size. This was most evident in the ESCP comparison: characteristics of both groups of instances were nearly identical, clearly showing that we cannot expect easy answers when it comes to hard computational problems. At least, not yet.