Domain Dependent Parameter Setting in SAT Solver Using Machine Learning Techniques
Autoři
Rok
2023
Publikováno
Agents and Artificial Intelligence 14th International Conference, ICAART 2022 Virtual Event, February 3–5, 2022 Revised Selected Papers. Cham: Springer International Publishing AG, 2023. p. 169-200. ISSN 0302-9743. ISBN 978-3-031-22952-7.
Typ
Stať ve sborníku
Pracoviště
Anotace
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
Autoři
Rok
2022
Publikováno
Proceedings of the 14th International Conference on Agents and Artificial Intelligence. Madeira: SciTePress, 2022. p. 586-597. ISBN 978-989-758-547-0.
Typ
Stať ve sborníku
Pracoviště
Anotace
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.