一种改进的子集可满足性算法用于FPGA布线

The Improvement of Sub-SAT for FPGA Routing

介绍了用布尔可满足性(SAT)和子集可满足性(sub-SAT)算法解决FPGA的详细布线问题。在布线资源固定的FPGA布线环境中,布尔公式可以证明所给电路的不可布通性,这一点要优于典型的one-net-at-a-time方法。子集可满足性方法把一个有N个约束的"严格的"SAT问题转换成一个新的"松弛的"SAT问题,仅当在原始问题中变量的不可满足个数不超过阈值k(kN)时,这一问题是可满足的。它改进了布尔可满足性,但是却产生了很多额外的变量和子句。针对这一问题,提出了用伪布尔可满足性(PBS)来消除子集可满足性公式带来的缺点。初步的实验结果表明,把这个方法加入子集可满足性方法中可以减少变量和子句数量,并显著减少运行时间。

The problem of detailed FPGA routing using Boolean and sub-SAT formulation methods was addressed. In the context of FPGA routing resources are fixed, Boolean formulation methods can prove the unroutability of a given circuit, which is a clear advantage over classical one-net-at-a-time approaches. The sub-SAT methods transform a ＂strict＂ SAT problem with N constraints into a new, ＂relaxed＂ SAT problem which is satisfiable on a condition of unsatisfiable constraint numbers k〈〈N in the original problem. It improves SAT-based approach much, but introduces too many additional variables and clauses. To solve this problem, we employ the Pseu-do-Boolean satisfiability to offset the disadvantage of sub-SAT formulation. Preliminary experi- mental results show that this approach added to sub-SAT can reduce the numbers of variables and clauses, and reduce the runtime observably.