This paper describes a new variable ordering heuristic for a Boolean satisfiability problem (SAT) solver based on search by the method DPLL. The basic idea of the heuristic is to derive a dynamic graph from the state of the problem during search. (en)
Č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í.
Č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í. (cs)