首页>
外国专利>
DPLL-based SAT solver using with application-aware branching
DPLL-based SAT solver using with application-aware branching
展开▼
机译:结合应用感知分支的基于DPLL的SAT求解器
展开▼
页面导航
摘要
著录项
相似文献
摘要
A system and method for determining satisfiability of a bounded model checking instance by restricting the decision variable ordering of the SAT solver to a sequence wherein a set of control state variables is given higher priority over the rest variables appearing in the formula. The order for control state variables is chosen based on an increasing order of the control path distance of corresponding control states from the target control state. The order of the control variables is fixed, while that of the rest is determined by the SAT search. Such a decision variable ordering strategy leads to improved performance of SAT solver by early detection and pruning of the infeasible path segments that are closer to target control state.
展开▼