相关疑难解决方法(0)

我有一些理论/实际问题,我现在还没有关于如何管理的线索,这里是:

我创建了一个SAT求解器,能够在存在模型时找到模型,并且当使用遗传算法在C中出现CNF问题时,不能证明矛盾.

SAT问题看起来基本上就像这样的问题: 我的目标是使用此求解器在许多不同的NP完成问题中找到解决方案 .基本上,我将不同的问题转换为SAT,用我的求解器解决SAT,然后将解决方案转换为原始问题可接受的解决方案.

我已经成功完成了N*N Sudoku以及N-queens问题,但这是我的新目标:将类调度问题减少到SAT,但我不知道如何形成类调度问题以便轻松转换它在SAT之后.

显然,在几个月内,我们的目标就是制作一张如下图所示的时间表:

我发现这个源代码能够解决类调度但不幸的是没有减少SAT:/

我还发现了一些关于规划的文章(例如http://www.cs.rochester.edu/users/faculty/kautz/papers/kautz-satplan06.pdf).

但是,本文中使用的规划域定义语言似乎对我来说过于笼统,以表示类调度问题.:/

是否有人知道如何有效地形成类调度以便将其减少到SAT以及之后,将SAT解决方案(如果它存在^^)转换为类调度？

我基本上对任何建议持开放态度,我现在不知道如何表示,如何减少问题,如何将SAT解决方案转换为计划......

跟进问题:类调度到布尔可满足性[多项式时间减少]第2部分