| Abstrakt: | Súčasné SAT solvery disponujú heuristikami, ktoré umožňujú efektívne rátať aj po-
merne veľké inštancie. Keďže SAT je NP-úplný problém, dá sa očakávať, že pre každý
solver existujú inštancie, na ktorých potrebuje exponenciálny čas. V praxi je ale ťažké
nájsť inštancie, na ktorých by daný solver bežal dlho. Takéto inštancie môžu jednak
slúžiť ako porovnávacie testy (benchmark) pre rôzne solvery, prípadne ich ďalšia ana-
lýza môže priniesť lepšie pochopenie štrukturálnych vlastností, ktoré spôsobujú rýchly
beh heuristík na bežných problémoch. Cieľom práce je navrhnúť algoritmus, ktorý je
schopný pre daný solver generovať ’ťažké’ inštancie. Zároveň nám to umožní porovnať
solvery z hľadiska toho, ako náročné je pre ne ťažké inštancie generovať.
|
|---|