论文部分内容阅读
介绍了用布尔可满足性（SAT）和子集可满足性（sub-SAT）算法解决FPGA的详细布线问题。在布线资源固定的FPGA布线环境中，布尔公式可以证明所给电路的不可布通性，这一点要优于典型的one—net—at-a—time方法。子集可满足性方法把一个有Ⅳ个约束的“严格的”SAT问题转换成一个新的“松弛的”SAT问题，仅当在原始问题中变量的不可满足个数不超过阈值k（k〈〈N）时，这一问题是可满足的。它改进了布尔可满足性，但是却产生了很多额外的变量和子句。针对这一问题，提出了用伪布尔可满足性（PBS）来消除子集