MINCE: A Static Global Variable-Ordering Heuristic for SAT Search and BDD Manipulation

Простая страница элемента
dc.creatorAloul,Fadi
dc.creatorMarkov,Igor
dc.creatorSakallah,Karem
dc.date2004
dc.date.accessioned2024-02-06T12:53:16Z
dc.date.available2024-02-06T12:53:16Z
dc.descriptionThe increasing popularity of SAT and BDD techniques in formal hardware verification and automated synthesis of logic circuits encourages the search for additional speedups. Since typical SAT and BDD algorithms are exponential in the worst-case, the structure of realworld instances is a natural source of improvements. While SAT and BDD techniques are often presented as mutually exclusive alternatives, our work points out that both can be improved via the use of the same structural properties of instances. Our proposed methods are based on efficient problem partitioning and can be easily applied as pre-processing with arbitrary SAT solvers and BDD packages without modifying the source code of SAT/BDD tools. Finding a better variable ordering is a well recognized problem for both SAT solvers and BDD packages. Currently, the best variable-ordering algorithms are dynamic, in the sense that they are invoked many times in the course of the host algorithm that solves SAT or manipulates BDDs. Examples include the DLCS ordering for SAT solvers and variable sifting during BDD manipulations. In this work we propose a universal variable-ordering algorithm MINCE (MIN Cut Etc.) that pre-processes a given Boolean formula in CNF. MINCE is completely independent from target SAT algorithms and in some cases outperforms both the variable state independent decaying sum (VSIDS) decision heuristic for SAT and variable sifting for BDDs. We argue that MINCE tends to capture structural properties of Boolean functions arising from real-world applications. Our contribution is validated on the ISCAS circuits and the DIMACS benchmarks. Empirically, our technique often outperforms existing SAT/BDD techniques by a factor of two or more. Our results motivate the search for better dynamic ordering heuristics and combined static/dynamic techniques.
dc.formattext/html
dc.identifierhttps://doi.org/10.3217/jucs-010-12-1562
dc.identifierhttps://lib.jucs.org/article/28323/
dc.identifier.urihttps://openrepository.mephi.ru/handle/123456789/8663
dc.languageen
dc.publisherJournal of Universal Computer Science
dc.relationinfo:eu-repo/semantics/altIdentifier/eissn/0948-6968
dc.relationinfo:eu-repo/semantics/altIdentifier/pissn/0948-695X
dc.rightsinfo:eu-repo/semantics/openAccess
dc.rightsJ.UCS License
dc.sourceJUCS - Journal of Universal Computer Science 10(12): 1562-1596
dc.subjectSAT
dc.subjectCNF
dc.subjectBDDs
dc.subjectbacktrack search
dc.subjectdecision heuristics
dc.subjectvariable ordering
dc.subjectformal verification
dc.subjectpartitioning
dc.titleMINCE: A Static Global Variable-Ordering Heuristic for SAT Search and BDD Manipulation
dc.typeResearch Article
Файлы
Коллекции