Efektivní heuristika pro SAT založená na znalosti komponent souvislosti grafu problému

Abstrakt

Článek pojednává o nové heuristice pro určování pořadí proměnných při řešení problémů booleovské splnitelnosti (SAT problémy) prohledáváním metodou DPLL. Základní ideou navržené heuristiky je použití dynamického grafu odvozeného ze stavu booleovské formule definující problém v průběhu řešení.

Klíčová slova

• Efficient
• Heuristic
• Exploiting
• Connected
• Components
• Problem