A Signal Correlation Guided Circuit-SAT Solver

Простая страница элемента
dc.creatorLu,Feng
dc.creatorWang,Li-C.
dc.creatorMoondanos,John
dc.creatorHanna,Ziyad
dc.date2004
dc.date.accessioned2024-02-06T12:53:16Z
dc.date.available2024-02-06T12:53:16Z
dc.descriptionWe propose two heuristics, implicit learning and explicit learning, that utilize circuit topological information and signal correlations to derive conflict clauses that could efficiently prune the search space for solving circuit based SAT problem instances. We implemented a circuit-SAT solver SC-C-SAT based on the proposed heuristics and the concepts used in other state-of-the-art SAT solvers. For solving unsatisfiable circuit examples and for solving difficult circuit-based problems at Intel, our solver is able to achieve speedup of one order of magnitude over other state-of-the-art SAT solvers that do not use the heuristics.
dc.formattext/html
dc.identifierhttps://doi.org/10.3217/jucs-010-12-1629
dc.identifierhttps://lib.jucs.org/article/28326/
dc.identifier.urihttps://openrepository.mephi.ru/handle/123456789/8665
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): 1629-1654
dc.subjectBoolean satisfiability
dc.subjectBoolean equivalence checking
dc.subjectATPG
dc.titleA Signal Correlation Guided Circuit-SAT Solver
dc.typeResearch Article
Файлы
Коллекции