Using Algorithm Configuration Tools to Generate Hard SAT Benchmarks

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F18%3A10389947" target="_blank" >RIV/00216208:11320/18:10389947 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/68407700:21230/18:00322875

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Using Algorithm Configuration Tools to Generate Hard SAT Benchmarks

Popis výsledku v původním jazyce

Algorithm configuration tools have been successfully used to speed up local search satisfiability (SAT) solvers and other search algorithms by orders of magnitude. In this paper, we show that such tools are also very useful for generating hard SAT formulas with a planted solution, which is useful for benchmarking SAT solving algorithms and also has cryptographic applications. Our experiments with state-of-the-art local search SAT solvers show that by using this approach we can randomly generate satisfiable formulas that are considerably harder than uniform random formulas of the same size from the phase-transition region or formulas generated by state-of-the-art approaches. Additionally, we show how to generate small satisfiable formulas that are hard to solve by CDCL solvers

Název v anglickém jazyce

Using Algorithm Configuration Tools to Generate Hard SAT Benchmarks

Popis výsledku anglicky

Algorithm configuration tools have been successfully used to speed up local search satisfiability (SAT) solvers and other search algorithms by orders of magnitude. In this paper, we show that such tools are also very useful for generating hard SAT formulas with a planted solution, which is useful for benchmarking SAT solving algorithms and also has cryptographic applications. Our experiments with state-of-the-art local search SAT solvers show that by using this approach we can randomly generate satisfiable formulas that are considerably harder than uniform random formulas of the same size from the phase-transition region or formulas generated by state-of-the-art approaches. Additionally, we show how to generate small satisfiable formulas that are hard to solve by CDCL solvers

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/GA18-07252S" target="_blank" >GA18-07252S: MoRePlan: Modelování a reformulace plánovacích problémů</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2018

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

Proceedings of the Eleventh International Symposium on Combinatorial Search, SOCS 2018

ISBN

978-1-57735-802-2

ISSN

—

e-ISSN

neuvedeno

Počet stran výsledku

5

Strana od-do

133-137

Název nakladatele

AAAI press

Místo vydání

Neuveden

Místo konání akce

Stockholm, Sweden

Datum konání akce

14. 7. 2018

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

WRD - Celosvětová akce

Kód UT WoS článku

—