Ing. Filip Beskyd

Publications

Domain Dependent Parameter Setting in SAT Solver Using Machine Learning Techniques

Authors
Beskyd, F.; Surynek, P.
Year
2022
Published
Agents and Artificial Intelligence 14th International Conference, ICAART 2022 Virtual Event, February 3–5, 2022 Revised Selected Papers. Cham: Springer International Publishing AG, 2022. p. 169-200. ISSN 2945-9133. ISBN 978-3-031-22952-7.
Type
Proceedings paper
Annotation
We address the problem of variable and truth-value choice in modern search-based Boolean satisfiability (SAT) solvers depending on the problem domain. The SAT problem is the task to determine truth-value assignment for variables of a given Boolean formula under which the formula evaluates to true. The SAT problem is often used as a canonical representation of combinatorial problems in many domains of computer science ranging from artificial intelligence to software engineering. Modern complete search-based SAT solvers represent a universal problem solving tool which often provide higher efficiency than ad-hoc direct solving approaches. Many efficient variable and truth-value selection heuristics were devised. Heuristics can usually be fine tuned by single or multiple numerical parameters prior to executing the search process over the concrete SAT instance. In this paper we present a machine learning approach that predicts the parameters of heuristic from the underlying structure of a graph derived from the input SAT instance. Using this approach we effectively fine tune the SAT solver for specific problem domain.

Parameter Setting in SAT Solver Using Machine Learning Techniques

Authors
Beskyd, F.; Surynek, P.
Year
2022
Published
Proceedings of the 14th International Conference on Agents and Artificial Intelligence. Madeira: SciTePress, 2022. p. 586-597. ISBN 978-989-758-547-0.
Type
Proceedings paper
Annotation
Boolean satisfiability (SAT) solvers are essential tools for many domains in computer science and engineering. Modern complete search-based SAT solvers represent a universal problem solving tool which often provide higher efficiency than ad-hoc direct solving approaches. Over the course of at least two decades of SAT related research, many variable and value selection heuristics were devised. Heuristics can usually be tuned by single or multiple numerical parameters prior to executing the search process over the concrete SAT instance. In this paper we present a machine learning approach that predicts the parameters of heuristic from the underlying structure of the input SAT instance.