如何在 PDDL forall 中获取 break 的功能

Question

我正在尝试使用 PDDL 解决 Light Up 难题。为了实现将灯泡放置在单元格中的效果，我必须在 (x, y) 中放置一个灯泡，然后只要没有黑色单元格就点亮相同的行和列。在黑牢房之前，我无法点亮牢房。

例如，对于一个 5*5 的网格，如果我想在 (0,1) 处放置一个灯泡并且在 (3, 1) 处有黑色单元格，我只想点亮单元格 (0,1) ), (1,1), (2,1) 如果我只考虑列。但我不想在黑色单元格之后点亮单元格 (4,1)。

那么，如果我使用 forall 之类的东西，当它在一行/列中找到一个黑色单元格时，我将如何打破 for all 循环？

Answer 1

我认为看看 PDDL 中的公理和派生谓词是值得的。这使得构建传递闭包并从其他变量中获取信息成为可能。

其实你可以从网格结构（哪些细胞是黑色的）和灯泡的信息中推导出哪些细胞有光。所以你可以为每个单元定义一个派生谓词 lit((x,y)) 并用公理编写背景理论：

• 点亮((x,y))
• lit((x,y))

对于所有非黑色单元格，目标公式可能类似于：“lit((0,0)) and ... and ... lit((n,m))”。