Boolean satisfiability (SAT) is an NP-complete problem with important applications, notably in hardware and software verification. Characterising a SAT instance by a set of features has shown great potential for various tasks, ranging from algorithm selection to benchmark generation. In this work, we revisit the widely used SATZilla features and introduce a new version of the tool used to compute them. In particular, we utilise a new preprocessor and SAT solvers, adjust the code to accommodate larger formulas, and determine better settings of the feature extraction time limits. We evaluate the extracted features on three downstream tasks: satisfiability prediction, running time prediction, and algorithm selection. We observe that our new tool is able to extract features from a broader range of instances than before. We show that the new version of the feature extractor produces features that achieve up to 26% lower RMSE for running time prediction, up to 3% higher accuracy for satisfiability prediction, and up to 15 times higher closed gap for algorithm selection on benchmarks from recent SAT competitions.
@InProceedings{shavit_et_al:LIPIcs.SAT.2024.27, author = {Shavit, Hadar and Hoos, Holger H.}, title = {{Revisiting SATZilla Features in 2024}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {27:1--27:26}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.27}, URN = {urn:nbn:de:0030-drops-205496}, doi = {10.4230/LIPIcs.SAT.2024.27}, annote = {Keywords: Satisfiability, feature extraction, running time prediction, satisfiability prediction} }
Feedback for Dagstuhl Publishing