Exploiting Configurations of MaxSAT Solvers
Exploiting Configurations of MaxSAT Solvers: In-Proceedings, currently on Arxiv
In this paper, we describe how we can effectively exploit alternative parameter configurations to a MaxSAT solver. We describe how these configurations can be computed in the context of MaxSAT. In particular, we experimentally show how to easily combine configurations of a non-competitive solver to obtain a better solving approach.
Author List:
Link: https://arxiv.org/abs/2306.07635
Cite
@misc{alòs2023exploiting,
title={Exploiting Configurations of MaxSAT Solvers},
author={Josep Alòs and Carlos Ansótegui and Josep M. Salvia and Eduard Torres},
year={2023},
eprint={2306.07635},
archivePrefix={arXiv},
primaryClass={cs.AI}
}OptiLog V2: Model, Solve, Tune and Run
OptiLog V2: Model, Solve, Tune and Run: International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
We present an extension of the OptiLog Python framework. We fully redesign the solvers module to support the dynamic loading of incremental SAT solvers with support for external libraries. We introduce new modules for modelling problems into Non-CNF format with support for Pseudo Boolean constraints, for evaluating and parsing the results of applications, and we add support for constrained execution of blackbox programs and SAT-heritage integration. All these enhancements allow OptiLog to become a swiss knife for SAT-based applications in academic and industrial environments.
Author List:
Link: https://link.springer.com/article/10.1007/s10732-022-09495-3
Cite
@InProceedings{alos_et_al:LIPIcs.SAT.2022.25,
author = {Al\`{o}s, Josep and Ans\'{o}tegui, Carlos and Salvia, Josep M. and Torres, Eduard},
title = {{OptiLog V2: Model, Solve, Tune and Run}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {25:1--25:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16699},
URN = {urn:nbn:de:0030-drops-166996},
doi = {10.4230/LIPIcs.SAT.2022.25},
annote = {Keywords: Tool framework, Satisfiability, Modelling, Solving}
}Incomplete MaxSAT approaches for combinatorial testing
Incomplete MaxSAT approaches for combinatorial testing: Journal of Heuristics volume 28, pages 377–431 (2022)
We present a Satisfiability (SAT)-based approach for building Mixed Covering Arrays with Constraints of minimum length, referred to as the Covering Array Number problem. This problem is central in Combinatorial Testing for the detection of system failures. In particular, we show how to apply Maximum Satisfiability (MaxSAT) technology by describing efficient encodings for different classes of complete and incomplete MaxSAT solvers to compute optimal and suboptimal solutions, respectively. Similarly, we show how to solve through MaxSAT technology a closely related problem, the Tuple Number problem, which we extend to incorporate constraints. For this problem, we additionally provide a new MaxSAT-based incomplete algorithm. The extensive experimental evaluation we carry out on the available Mixed Covering Arrays with Constraints benchmarks and the comparison with state-of-the-art tools confirm the good performance of our approaches.
Author List:
Link: https://link.springer.com/article/10.1007/s10732-022-09495-3
Cite
@article{article,
author = {Ansótegui, Carlos and Manyà, Felip and Ojeda, Jesus and Salvia, Josep and Torres, Eduard},
year = {2022},
month = {08},
pages = {1-55},
title = {Incomplete MaxSAT approaches for combinatorial testing},
volume = {28},
journal = {Journal of Heuristics},
doi = {10.1007/s10732-022-09495-3},
abstract = {We present a Satisfiability (SAT)-based approach for building Mixed Covering Arrays with Constraints of minimum length, referred to as the Covering Array Number problem. This problem is central in Combinatorial Testing for the detection of system failures. In particular, we show how to apply Maximum Satisfiability (MaxSAT) technology by describing efficient encodings for different classes of complete and incomplete MaxSAT solvers to compute optimal and suboptimal solutions, respectively. Similarly, we show how to solve through MaxSAT technology a closely related problem, the Tuple Number problem, which we extend to incorporate constraints. For this problem, we additionally provide a new MaxSAT-based incomplete algorithm. The extensive experimental evaluation we carry out on the available Mixed Covering Arrays with Constraints benchmarks and the comparison with state-of-the-art tools confirm the good performance of our approaches.}
}OptiLog: A Framework for SAT-based Systems
OptiLog: A Framework for SAT-based Systems: International Conference on Theory and Applications of Satisfiability Testing (SAT 2021)
We present OptiLog, a new Python framework for rapid prototyping of SAT-based systems. OptiLog allows to use and integrate SAT solvers currently developed in C/C++ just by implementing the iSAT C++ interface. It also provides a Python binding to the PBLib C++ toolkit for encoding Pseudo Boolean and Cardinality constraints. Finally, it leverages the power of automatic configurators by allowing to easily create configuration scenarios including multiple solvers and encoders.
Author List:
OptiLog V2: Model, Solve, Tune and Run International Conference on Theory and Applications of Satisfiability Testing (SAT 2022): https://drops.dagstuhl.de/opus/volltexte/2022/16699/
Link: https://link.springer.com/chapter/10.1007/978-3-030-80223-3_1
Cite
@InProceedings{10.1007/978-3-030-80223-3_1,
author="Ans{\'o}tegui, Carlos
and Ojeda, Jes{\'u}s
and Pacheco, Antonio
and Pon, Josep
and Salvia, Josep M.
and Torres, Eduard",
editor="Li, Chu-Min
and Many{`a}, Felip",
title="OptiLog: A Framework for SAT-based Systems",
booktitle="Theory and Applications of Satisfiability Testing -- SAT 2021",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="1--10",
abstract="We present OptiLog, a new Python framework for rapid prototyping of SAT-based systems. OptiLog allows to use and integrate SAT solvers currently developed in C/C++ just by implementing the iSAT C++ interface. It also provides a Python binding to the PBLib C++ toolkit for encoding Pseudo Boolean and Cardinality constraints. Finally, it leverages thepower of automatic configurators by allowing to easily create configuration scenarios including multiple solvers and encoders.",
isbn="978-3-030-80223-3"
}