我正在尝试将摩天大楼的拉丁方问题简化为SAT。
[skyscrapper问题与Latin-sqaure相同，但此外，摩天大楼难题还要求玩家将高度不同且独特的建筑物放置在网格上，以便满足网格边缘上的提示。这些“边缘线索”告诉玩家，从给定线索沿木板边缘的位置看，可以看到多少座建筑物。 （full explanation）
因此，为了使用SAT解算器解决此问题，我尝试了类似的方法来使用SAT解决suduko（我已经做过）。因此，首先我定义了所有n ^ 3个二进制变量X_i，j，k，这表明在i，j单元格中值k为真（因此在i，j单元格中我们有一个高度为k的摩天大楼） >
我以CNF的形式添加了以下缺点：
现在，我很难确定应该为线索和高度添加哪些约束。首先，我考虑了为给定的每个线索添加每种可能的顺序的选项，例如，如果从左边我可以看到3个摩天大楼（n = 4），那么可能性是：[[2，3，4，1]，[1,3,4,2]]但我认为总共是O（n！）...
我使用ILP实现了Suduko求解器，因此我读到了有关使用ILP（整数线性编程）解决此问题的信息。我发现this link描述了如何执行此操作。但是我仍然找不到他们在ILP情况下添加的高度约束的等效项，以适合SAT求解器。
非常感谢！
我正在尝试将摩天大楼的拉丁方问题简化为SAT。摩天大楼问题与拉丁方相同，但此外，摩天大楼难题还要求玩家......>
可能有很多方法，但是想到的可能如下。
对于每个线索C_i，您引入新的帮助程序变量：