Domain Dependent Parameter Setting in SAT Solver Using Machine Learning Techniques

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21240%2F22%3A00362980" target="_blank" >RIV/68407700:21240/22:00362980 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-031-22953-4_8" target="_blank" >https://doi.org/10.1007/978-3-031-22953-4_8</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-22953-4_8" target="_blank" >10.1007/978-3-031-22953-4_8</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Domain Dependent Parameter Setting in SAT Solver Using Machine Learning Techniques

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Domain Dependent Parameter Setting in SAT Solver Using Machine Learning Techniques

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA22-31346S" target="_blank" >GA22-31346S: logicMOVE: Logické uvažování v plánování pohybu pro mnoho robotických agentů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2022

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Agents and Artificial Intelligence 14th International Conference, ICAART 2022 Virtual Event, February 3–5, 2022 Revised Selected Papers

ISBN

978-3-031-22952-7

ISSN

2945-9133

e-ISSN

1611-3349

Počet stran výsledku

32

Strana od-do

169-200

Název nakladatele

Springer International Publishing AG

Místo vydání

Cham

Místo konání akce

Online

Datum konání akce

3. 2. 2022

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000971480800008