In this study we continue the success story of fuzz testing automated reasoning tools by providing the ifrst extensive fuzzing study on MaxSAT solvers. As somewhat expected we identify interesting defects and failures in almost all MaxSAT solvers from the MaxSAT Evaluation 2022. A classification of these bugs into four main classes and various subclasses can help developers in debugging them. Finally, we show how to uncover additional issues by a preliminary MaxSAT delta debugging strategy on top of reducing the failing test cases significantly. This study clearly shows that MaxSAT solvers are less reliable and robust than expected, and further suggests that fuzzing and delta debugging can help to improve this situation. Furthermore, we provide a regression suite of interesting small instances.
https://cca.informatik.uni-freiburg.d(Te./ Paxian);https://cca.informatik.uni-freiburg.d(Ae/. Biere)
© 2023 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
SUB
PB
SMT
Others BB ILP
X X
X
X
Rank MaxSAT Solver
1. & 2. CASHWMaxSAT [
HS X
UB X X X X X X X X X
X X
X X
X X X
X X X X not yet available for the weighted variant. In our study we chose a third technique, a dynamic software testing approach, requiring no changes in the code of solvers. This approach, called fuzz testing or fuzzing, is applied to enhance the robustness of solvers.
Fuzz testing has been successful in detecting software vulnerabilities and bugs across various
ifelds [
In Table1 we describe the tested solvers, their ranking in the MSE and also point out the techniques they use.
Regarding related work, we are only aware of two available MaxSAT fuzzers supporting the old pre MSE22 WCNF format. The first fuzzer33[] tests only for invalid exit codes of the solver and a missing o-value or one which is bigger than sum of weights. The second fuz3z4e]r [ comes along with a MaxSAT solver GaussMax H35S],[which has not yet participated in the MSE. The authors generated a CNF, added xor gates and converted it with bit blasting into WCNF with a bundle of python and shell scripts. Our understanding is that both fuzzers do not check whether the o-value matches the model or an optimum is reached.
In this section we introduce the four key components of our study: We begin by discussing the techniques to construct random WCNF formulas by our fWuCzNzFeurzz. Next, we describe ourWCNFCompare tool, developed to compare and log the faults of solvers, providing a valuable direct comparison of their results. Following that, we describe our preliminary implementation of the delta debugging algorithm. Finally, we present our fault classification scheme, which categorizes the discovered faults frWoCmNFCompare.
Fuzzing is a technique to detect software vulnerabilities with the idea to treat software as a black
box and generate random inputs in order to uncover critical defects as segmentation faults,
overflows or incorrect result1s4][. Our novel tooWlCNFuzz is a generation-based
grammaraware 3[
There already exist successful fuzzing tools for CNF formulas like CNFuzz and Fuz1z7S]A.T [
CNFuzz generates structured instances, which results in problems closer to industrial examples,
than simply applying a variable clause ra3t7i,o3[
In the following we use our implementation of a “Linear Congruential Generator”, with values from the “Art of Computer Programmi4n0g]”, [to pick all random choiceWsC. NFuzz adds up to 10 layers of clauses with each containing up to 70 variables. Layers consist entirely either of hard or soft clauses. Soft clause layers are chosen randomly with higher chance initially and lower chance for the following soft layers. The clauses of the n’th layer contains variables of its own layer with high probability and with decreasing chances variables of lower layers. Most of the clauses (around 2/3) are ternary, with decreasing chances they are of higher order and around every tenth clause is binary. We calculate the number of clauses in each layer by picking a suitable clause-variable-ratio. As we want hard clauses to be satisfiable with a high chance, we pick a low ratio∈ [1, 2.5] for hard clause layers. For soft clause layers we want to have at least some clauses making the problem unsatisfiable, therefore we choose a high ratio ∈ [3.5, 5.5] .
Additionally, we add Tseitin encoded Equality, AND, 3-XOR and 4-XOR gates. We include an activation literal to all clau3s/e4s of the gate encodings and add one additional soft clause containing only the negated activation literal. Furthermore, one out of ten instances is forced to contain only soft clauses. In very rare cases, all layers and gates are decided to consist only of hard clauses.
The maximal weight in the MSE is often relatively small, and often there are unweighted
problems to solve. Therefore, the maximal weight is chosen to be in one of the following ranges,
for each interval the probability is [11/,51:]; [
In the following, we discuss challenges in fuzzing a single MaxSAT solver and present our solutionWCNFCompare, a Python tool to automate the comparison, validation, and logging of multiple MaxSAT solver results.
Evaluating the optimality of a single fuzzed MaxSAT solver presents a challenge in the absence of a certified proof or solver. To address these issues, we introWdCuNcFeCompare, a Python tool that automates the process of comparing the results produced by multiple MaxSAT solvers. In its default configuratioWnC,NFCompare runs all solvers mentioned in Sect1io,wnith a default timeout of 20 seconds for each solver. It then verifies the satisfiability of hard clauses, and checks the o-value against the model for each solver result, usWinCgNFoVuerrifier. We use the best model verified solution as a representative for the unverified optimal outcome. If other solvers do not produce the same o-value, it indicates an erroneous result. Subsequently, the tool classifies results into approximately 30 diferent fault classes, which are doubled again, depending on the sum of weights, as discussed in Sectio2.n4. Each solver is assigned a number, as are the types of faults that occur (see Se2c.t4i)o,wnith fault types numbered from 1 to 60 within the tool. If multiple errors occur, then the exit codes and solver position are added up and taken modulo 255, as 255 is the highest possible exit code.
One limitation of the comparison script is that identical exit codes can emerge from various solver failure combinations. Consequently, as the delta debugger reduces instances only considering the exit code, we can end up with diferent solver-fault combinations at the end of a reduction. To address this issue, we introduced a command line option that restricts the script to only return the exit code of a single solver for the delta debugger run.
WCNFCompare also logs results, generating individual files for each WCNF-solver-fault combination. As fuzzing and delta debugging can run concurrently on multiple cores, we need to prevent access to the same solver-fault combinations logfile from multiple cores, which is done by adding a unique seed. These files contain a clear fault comparison overview, the final o-values of each solver, error messages, and the solver’s output to stdout and stderr. At the end of the whole fuzzing/delta debugging run, these log files are consolidated into a single log file per solver fault combination. This approach ofers a significant advantage: it permits the use of any instance generation tool or shrinking tool, while maintaining a consistent logging process.
Delta debugging4[
This greedy approach attempts to remove portions of the input not contributing to the fault. Initially, the approach attempts to remove the whole input, then successively reduces this to half, a quarter, and so on. In the worst-case scenario, every second atomic element needs to be removed, which makes the algorithm worse than merely iterating once through all elements.
It still has(a) complexity, which makes it an advanced tool for isolating and simplifying failure-inducing inputs in MaxSAT problems, supporting developers in discovering root causes of solver bugs. Additionally, during the reduction proWcCeNsFs,Compare is called for all created WCNF instances. We are the first to log errors and saving fault triggering WCNFs arising during the reduction phase. Instances that might not have been generated by the initial fuzzer are produced. This aims to uncover additional interesting new solver-fault combinations that might have remained undetected otherwise.
We plan to elaborate on delta debugging in a forthcoming extended version.
Next, we discuss how faults, in the context of MaxSAT solvers, can be classified. Therefore, we introduce four main fault classes: Crashes, Lower/Upper Bound Violations, Performance Regressions, and Other Issues.
WCNFCompare originally returns 60 diferent fault classes for which 1-30 are for a sum of weight smaller tha2n32 and the 31-60 debug the same faults for bigger weights. We simplified this list into four main and 14 subclasses, still diferentiating between small and big weights.
In order to simplify the fault classification list, we propose the following notation for the diferent types of o-values: le tsolverdenote the best o-value given in the solver outmpuotde,l denotes the o-value represented by the solver’s model (as calculated by the model-verifier), and ifnally min denotes the best verified o-value of all solvers. Using this notation, we present the diferent fault classes and their respective errors: 1. Crashes: 1.1. MaxSAT solver’s exit code is 134 (SIGABRT, internal error or inconsistency) 1.2. MaxSAT solver’s exit code is 135 (SIGSEGV, segmentation fault) 1.3. MaxSAT solver’s exit code is 136 (SIGFPE, arithmetic error or overflow) 1.4. MaxSAT solver’s exit code is 137 (SIGKILL, immediately shutdown) 1.5. MaxSAT solver’s exit code is 139 (SIGSEGV / SIGBUS, segmentation or bus fault) 1.6. MaxSAT solver’s exit code is XXX (all other exit codes) 2. Bound Violations: 2.1. min < solverand solver== model 2.2. solver≠ modeland model ≠ min and solver≠ min . 2.3. Either modelor solverunequals min. 2.4. Verifier asserts that provided model is UNSATISFIABLE.
2.5. Verifier states hard clauses are SATISFIABLE, but solver states UNSATISFIABLE. 3. Performance Regressions: 3.1. Potential Fault: Solver had timeout, but this timeout is 50 times larger than the average time of the non-timeout solvers. 4. Other Issues: 4.1. Solver has an error either stated in stdout or stderr. 4.2. Inconsistency in status line and output.
4.3. Unexpected behavior of a verifier.
Determining the severity of these errors is a crucial aspect. As an example, fault 3.1. is only a potential fault that may indicate a performance issue or a more severe infinite loop problem. Generally it is not considered a serious fault. Crashes are more severe, but at least they do not deliver an incorrect value/model which we tend to trust. Bound violations, on the other hand are considered serious, as we cannot trust the solver reliability. Most of these faults can be detected with a sanity check, which implies a check if the hard clauses are satisfiable and if the model’s o-value matches the given solver o-value. This suggests that the most critical fault in these violations could occur if this quick check appears to be sane, yet a fault such as the one indicated by 2.1. is still present. In the current version of our tool, we overlooked the inclusion of a model sanity check. This means we only verify if the provided model already contradicts the formula, without checking if the number of variables is correct. We have acknowledged this oversight and plan to address it in the upcoming version of the tool.
The sequence in which these faults are evaluated during the fault classification process plays an important role in ensuring an accurate fault detection. The order should minimize the risk of missing important bugs as occurred in previous versions of the compare script. For instance, the solver status should be evaluated before evaluating the o-value and model. Is it worth considering the occurrence of multiple faults in a single solver run? If, for example an error message is thrown, but has at the same time a bound violation, we decided to only catch the bound violation, as we do not interpret error messages. Further some soMlavexrHaSsprint often such messages but still provides correct results. We believe that our approach has a good balance between not over-categorizing faults and not neglecting important faults.
In this section, we present results of our MaxSAT solver fuzzing and delta debugging experiments. The tests were run on a system powered by an i9-12900 processor with 16 cores and 128 GB of memory. The experiments were executed on all 16 cores around one week for fuzzing and afterwards we performed delta debugging on the first five faults that occurred in each class of the original 60 classes, which took another week. All experimental data, the regression suite, and source code is availablehatttps://cca.informatik.uni-freiburg.de/maxsat.fDuzuzring setup, we challenged the following issues: • Z3 doesn’t support competition standard output, therefore we implemented a transformation script. • The MSE provides a useful benchmark code base for verifying models, transforming WCNFs from new to old format and vice versa, and more. However, we could not use these tools as they only accept a sum of weights u2p63t,oand we aimed to support the full range up t2o64 − 2, as it is standard in the competition.
CASHWMaxSAT-CoreP* ... SCIP 7.0.3 ... c SCIP optimum = 2 v 100110 o 2 s OPTIMUM FOUND MaxHS ... c #vars: 5 c #Clauses: 8 ... o 2 s OPTIMUM FOUND v 11011
CASHWMaxSAT-Plus ...
SCIP 7.0.3 ... c SCIP optimum = 2 v 100110 o 2 s OPTIMUM FOUND z3rc2 c Convert WCNF c Convert Output s OPTIMUM FOUND o 2 v 010111
UWrMaxSat-SCIP ... SCIP 8.0.0 ... c SCIP optimum: 2 v 100110 o 2 s OPTIMUM FOUND EvalMaxSAT s OPTIMUM FOUND o 1 v 000111 c Total time: 347 µs • Z3 and Pacose require the old evaluation format as input, we added a script to rewrite the instances. However, this led to additional fault classes during parallel execution, which were non-reproducible and hence, excluded from our results. • Maxpre2 outputs the old v-line format. We implemented a script to rewrite the output, which likely triggered unverifiable fault classes. These were also excluded from our results. In an updated version Maxpre2 can handle also the new v-line output format. • Pacose sometimes writes ”SATISFIABLE” instead of ”s SATISFIABLE.” • Solvers throw diferent exit codes. For instance, when an optimum solution is found,
Exact returns 30, whilPeacose returns an exit code of 10. • CGSS and Exact only work with *.wcnf named files. • In UWrMaxSat-SCIP, grepping for ”UNSAT” in the verbose=0 variant let the status line disappear.
Table2 presents our findings, displaying the number of faults detected for each fault class, as outlined in Sectio2n.4, in fuzzing and delta debugging runs. The exact numbers are not crucial, as the detected faults increase at a consistent rate, if run for extended periods. A detailed examination of the solvers during this study led to several interesting observations: • OnlyMaxHS and Z3 can handle empty instances. This is the reason wEhvyalMaxSAT crashed 822 times with exit code 255 and tUhWe rMaxSAT and CASHWMaxSAT variants with exit code 139. This happens only during the reduction phase, as no empty instance is generated with our fuzzer. • CGSS and Pacose do not accept a wcnf with only hard clauses, resulting in 271 131 crashes. • The following invalid exit codes occured causing a crash fault (fault category 1.): 1, 3, 105, 108, 134, 135, 136, 139, 141, 255 • CGSS throws exit code 1 for unsatisfiable instances - but the same exit code is thrown, if the whole instance is empty. This means, that these instances are reduced to the empty instance, after the first solver call of the delta debugger.
Our preliminary delta debugger showed already significant efectiveness. Some instances took up to a week to reduce, particularly when performance regression (3.1) occurred for instances with large numbers, making weight reduction a very time-intensive task.
The reduced instances uncovered intriguing problems, such as in Fig1u,wrehere a fault was significantly minimized. Another issue occurred with the timeout fault classM3a.1xiHnS due to a simple instance with just three soft and one hard clause, the original instance (reproducible with seed 193251431004265909) having 41 soft and 157 hard clauses. This problem forcMedaxHS into a type of infinite loop, only terminated by the technique’s 1500-second timeout. A nearly identical error with another instance occurred wiEtxhatchtesolver, but this time with a real timeout. That instance (seed 1795142913688699408) could be reduced to 7 soft and 24 hard clauses, underscoring that even timeouts can reveal interesting bugs.
Furthermore, we highlight that we could trigger 20 additional solver-fault combinations during our delta debugging phase. As demonstrated in Ta2b,tlehese additional combinations are additional entries within the second line. The ability to invoke these additional combinations is significant, as it provides further opportunities to probe the robustness of the solvers and expose potential vulnerabilities. This observation underscores the value of our novel approach of logging during the delta debugging phase, as it notably enhances the comprehensiveness of our testing process.
The results of our MaxSAT solver fuzzing and delta debugging experiments reveal crucial insights into the behavior and robustness of various solvers. Our WfuCzNzFeurzz efectively detects a significant number of interesting faults duWeCtNoFcompare, in various fault classes. Despite some initial challenges, our preliminary delta debugging tool leads to considerable reductions in input instances and exposes interesting issues, such as unexpected exit codes, timeout faults and interesting bound violations. These findings highlight the importance of rigorous testing and debugging in the development and refinement of MaxSAT solvers.
In the course of our research, we have constructed a useful regression set of interesting instances that we believe will be beneficial for solver development. These instances include: • Empty instance, empty soft/hard clause. • Non trivial reducible maximal weight instances with a maximum single w26e3ig−h1t and a maximal sum of weight2s64 − 2. • Simple unsatisfiable instances. • Tautology soft/hard clauses • With our fuzzer created and delta debugged instances for each fault class-solver combination, causing each at least one solver to crash.
At least one of these instances are triggering a fault in all the tested solvers, as some of these instances are not yet supported by the oficial rules. E.g. empty clauses / instances cannot be handled even by most SAT solvers. We suggest the following rules be incorporated into the competition solver rules: • An empty instance should yield a weight ”o 0”, with an empty model line ”v” and the status line ”s OPTIMUM FOUND”. • An unsatisfiable instance should produce the status line ”s UNSATISFIABLE”. • An empty hard clause should result in an unsatisfiable instance. • An empty soft clause should be unsatisfiable, but the instance can still be satisfiable. • The exit code of a solver should be 0 for all results but ”s UNKNOWN”.
We would like to ofer the MaxSAT community these instances, provided as a zip file from the MSE homepage, along with a script executing the solver with a subset or all instances and verifying the results and models. This surely would assist developers in improving the robustness of their solvers.
In this research, we explored an automated testing approach for MaxSAT solvers, utilizing fuzzing and delta debugging to uncover and minimize intriguing faults.
The input instances were significantly reduced during the delta debugging phase and our methods allowed us to identify and isolate critical issues, even within large, complex instances.
We also created a compact regression suite of small instances for solver development, which were shown to trigger specific errors in all tested solvers. We will provide these instances along with a script for executing and verifying the solver’s results to the MaxSAT community. We also proposed new rules to include in the MaxSAT Evaluation rule-book, to ensure the standard handling of basic clauses as provided by our regression suite.
In a extended version of this paper, we aim to expand upon our preliminary delta debugger, providing a more detailed exposition of its workings. Additionally, we intend to communicate with all authors regarding the discovered bugs to assist them in debugging their MaxSAT solvers.
In conclusion, our research demonstrates that automated testing methods, such as fuzzing and delta debugging, can trigger severe faults in MaxSAT solvers. We believe that our work will significantly contribute to the ongoing eforts to enhance the robustness and reliability of these solvers. Melbourne, VIC, Australia, August 28–September 1, 2017, Proceedings 20, Springer, 2017, pp. 449–456. [33] N. Manthey, MaxSAT fuzzer, 2020. URLh: ttps://github.com/conp-solutions/maxsat-fu.zzer [34] M. Soos, K. S. Meel, GaussMaxHS github repository, 2021. URhLt:tps://github.com/ meelgroup/gaussmaxh,savailable ahtttps://github.com/meelgroup/gaussmax.hs [35] M. Soos, K. S. Meel, Gaussian elimination meets maximum satisfiability, in: Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 18, 2021, pp. 581–587. [36] J. Wang, B. Chen, L. Wei, Y. Liu, Superion: Grammar-aware greybox fuzzing, in: 2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE), IEEE, 2019, pp. 724–735. [37] D. Mitchell, B. Selman, H. Levesque, et al., Hard and easy distributions of SAT problems, in: Aaai, volume 92, 1992, pp. 459–465. [38] E. Nudelman, K. Leyton-Brown, H. H. Hoos, A. Devkar, Y. Shoham, Understanding random SAT: Beyond the clauses-to-variables ratio, in: Principles and Practice of Constraint Programming–CP 2004: 10th International Conference, CP 2004, Toronto, Canada, September 27-October 1, 2004. Proceedings 10, Springer, 2004, pp. 438–452. [39] J. A. Navarro, A. Voronkov, Generation of hard non-clausal random satisfiability problems, in: Proceedings of the National Conference on Artificial Intelligence, volume 20, Menlo Park, CA; Cambridge, MA; London; AAAI Press; MIT Press; 1999, 2005, p. 436. [40] D. E. Knuth, The art of computer programming. volume 2: Seminumerical algorithms,
Bull. Amer. Math. Soc (1997). [41] A. Zeller, R. Hildebrandt, Simplifying and isolating failure-inducing input, IEEE Transactions on Software Engineering 28 (2002) 183–200. [42] G. Misherghi, Z. Su, HDD: hierarchical delta debugging, in: Proceedings of the 28th international conference on Software engineering, 2006, pp. 142–151. [43] A. Zeller, Why programs fail: a guide to systematic debugging, Elsevier, 2009.