Minisat 是一个约束编程/满足工具，有一个版本的 Minisat 可以在浏览器中运行http://www.msoos.org/2013/09/minisat-in-your-browser/
如何用 Minisat 表达调度问题？是否有更高级别的语言可以编译为 Minisat 让我表达它？
我的意思是解决考试时间表等问题。http://docs.jboss.org/drools/release/6.1.0.Final/optaplanner-docs/html_single/#examination
另一种高级建模语言是 Picat ( http://picat-lang.org/ )，当使用 sat 模块时，它可以选择 solve/2 转换为 CNF，例如“solve([dump], Vars)”。使用 sat 模块以及 cp 和 mip 模块时的语法类似于标准 CLP 语法。
有关一些 Picat 示例，请参阅我的 Picat 页面：http ://hakank.org/picat/ 。
像Minisat或Cryptominisat这样的SAT 求解器通常会读取合取范式 (CNF)中的一组逻辑OR表达式。将您的问题转换为这种 CNF 格式需要一个编码步骤。
电路 SAT 求解器处理嵌套的布尔表达式，而不是CNF. 但现在看来，这类求解器的表现要优于求解CNF SAT器。
Minizinc等约束编程求解器使用更易于编写和理解的高级语言。根据所使用的功能，Minizinc可以将其输入语言翻译成CNF/DIMACS适合 SAT 求解器的格式。
Peter Stuckey 的论文“没有 CNF 问题”解释了这个想法。他的幻灯片还包含一些关于日程安排的见解。
查看由Hakan Kjellerstrand编写的用于调度的Minizinc 示例。
Emmanuel Hebrard 的日程安排和 SAT是对该主题的广泛处理。
几个月前我参与了这个项目。
这真的很有趣。
要使用 miniSAT（或任何其他 SAT 求解器），您必须将调度问题简化为 SAT 问题。
我可以向您推荐我分三部分提出的这个问题。
你基本上会一步一步地看到如何将调度问题转换为 MiniSAT 可以阅读和解决的 SAT 问题:)。
再次感谢@amit，他在这个项目中提供了很大的帮助。
有了这个答案，您将能够与 T 老师一起解决 N 个房间，他们正在向 G 不同组的学生教授 S 科目:) 我认为这足以解决 99% 的调度问题。