-
Atom：Atom是用于描述原子句或命题的数据类型 . 这些基本上表示为字符串 .
-
文字：文字对应原子的原子或否定 . 在此实现中，每个文字都表示为一对由布尔值组成，表示Atom的极性和实际的Atom . 因此，字面'P'表示为（True，"P"），而其否定'-P'表示为（False，"P"） . 2
-
条款：条款是文字的分离，例如PvQvRv-S . 在此实现中，它表示为文字列表 . 所以最后一个子句是[（True，"P"），（True，"Q"），（True，"R"），（False，"S"）] .
-
公式：公式是子句的结合，例如（P vQ）^（RvP v-Q）^（ - P v-R） . 这是命题公式的CNF形式 . 在此实现中，它表示为子句列表，因此它是文字列表的列表 . 我们上面的示例公式将是[[（True，"P"），（True，"Q"）]，[（True，"R"），（True，"P"），（False，"Q"）]，[（False，"P"），（False） ，"P"）]] .
-
模型：（部分）模型是（部分）将真值分配给公式中的原子 . 在此实现中，这是（Atom，Bool）对的列表，即 . 原子与他们的任务 . 所以在上面的类型为Formula的例子中，如果我们将Q赋值为true而将false赋给Q则那么我们的模型将是[（"P"，True），（"Q"，False）]
好的，我写了并更新了功能
update :: Node -> [Node]
它接收一个Node并返回一个节点列表，这些节点是在一种情况下将True分配给未分配的原子而在另一种情况下分配为False（即一个案例分割） . 返回的列表有两个节点作为元素 . 一个节点包含一个公式，其中一个原子分配为True，模型使用此赋值更新，另一个节点包含公式，其中原子指定为False，模型已更新以显示此情况 . 每个节点的未分配原子列表也相应更新 . 此功能使用assign函数进行分配 . 它还使用chooseAtom函数选择要分配的文字 .
update :: Node -> [Node]
update (formula, (atoms, model)) = [(assign (chooseAtom atoms, True) formula, (remove (chooseAtom atoms) atoms, ((chooseAtom atoms,True)) `insert` model)) , (assign (chooseAtom atoms, False) formula, (remove (chooseAtom atoms) atoms, ((chooseAtom atoms, False) `insert` model)) )]
现在我必须做同样的事情，但这次我必须实现一个变量选择启发式 . 这应该替换chooseAtom而我应该用它来编写一个函数update2
type Atom = String
type Literal = (Bool,Atom)
type Clause = [Literal]
type Formula = [Clause]
type Model = [(Atom, Bool)]
type Node = (Formula, ([Atom], Model))
update2 :: Node -> [Node]
update2 = undefined
所以我的问题是如何创建一个heurestic并将其实现到update2函数中，该函数与更新函数的行为相同？
1 回答
如果我正确理解了这个问题，那么您就会问如何在命题逻辑的解析系统中实现其他选择规则 . 据推测，你正在构建一个通过为文字指定真值而得到的公式树，直到（a）已经尝试了所有可能的文字赋值组合或（b）框（空子句）已经导出 .
假设函数chooseAtom实现了一个选择规则，你可以通过给update添加一个额外的参数并用update替换update中的chooseAtom的出现来参数化任意选择规则r上的函数更新 . 由于chooseAtom实现了一个选择规则，因此将该选择规则传递给参数r会得到所需的结果 . 如果您提供chooseAtom的实现以及要替换它的函数，则可以更轻松地验证您的实现是否正确 .
希望这很有帮助 . 然而，目前还不清楚究竟是在问什么 . 特别是，你要求的是一个“变量选择规则” . 但是，看起来你正在为命题逻辑实现一个解决方案系统 . 通常，选择规则和变量与谓词逻辑的分辨率相关联 .