CDCL的能力来自证明系统，在理论也有这方面的讨论。特别在证明unsat的方面，CDCL频繁重启，不像以遍历搜索为目的去干的事情，而是积累学习子句（也就是归结式），然后在某个时刻，这些归结式就可以导出矛盾，得到unsat。不过，解sat和解unsat应该是需要不同的能力。这是未来SAT求解器可以作为的地方。
发布于 北京
蔡少伟
CDCL的能力来自证明系统，在理论也有这方面的讨论。特别在证明unsat的方面，CDCL频繁重启，不像以遍历搜索为目的去干的事情，而是积累学习子句（也就是归结式），然后在某个时刻，这些归结式就可以导出矛盾，得到unsat。不过，解sat和解unsat应该是需要不同的能力。这是未来SAT求解器可以作为的地方。