标签：efi mos class app rms ast unit key mes
希望从该文章中获取BCP的认识以及叙述方式
Thurley M. (2006) sharpSAT – Counting Models with Advanced Component Caching and Implicit BCP. In: Biere A., Gomes C.P. (eds) Theory and Applications of Satisfiability Testing - SAT 2006. SAT 2006. Lecture Notes in Computer Science, vol 4121. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11814948_38
| We introduce sharpSAT, a new #SAT solver that is based on the well known DPLL algorithm and techniques from SAT and #SAT solvers. Most importantly, we introduce an entirely new approach of coding components, which reduces the cache size by at least one order of magnitude, and a new cache management scheme. Furthermore, we apply a well known look ahead based on BCP in a manner that is well suited for #SAT solving. We show that these techniques are highly beneficial, especially on large structured instances, such that our solver performs significantly better than other #SAT solvers. | |
Conjunctive Normal Form Cache Size Unit Clause Bound Model Check Branch Variable
文献学习-sharpSAT – Counting Models with Advanced Component Caching and Implicit BCP
标签：efi mos class app rms ast unit key mes
原文地址：https://www.cnblogs.com/yuweng1689/p/14106772.html
