2 哈斯克尔问题

Question

我有 2 个关于 2 个 haskell 函数的问题

1. flipSymbol :: Model -> Atom -> Model 这个函数必须取一个 Model 和一个 Atom 并翻转模型中原子的真值。现在我正在考虑这样写这个函数：...

   flipSymbol m a = map f m
     在哪里
     f (atom, value) = if a == atom then (atom, not value) else (atom, value)

   有没有更好的办法？

2. 第二个比较复杂，如果可能的话，我需要一些帮助。 为了检查给定模型中公式的可满足性，我们传播了将真值分配给公式中的原子的效果。假设我们将值 True 分配给一个原子。以下效果 可应用于公式：

   • 正字面值具有相同的 True 值，因此，包含它们的任何子句都将从公式中删除。这是为了表明可以满足这些条款，因此不再影响公式的可满足性。
   • 否定文字的值为 False，因此从它们所在的任何子句中删除。这表明这些子句仍然不满足，只能通过其他文字之一获得值来使之为真真。在将 False 分配给原子的情况下，正文字现在将是错误的，应该被删除 从他们的子句中删除，而否定文字将变为真，并从公式中删除他们的子句。
     例如，在公式 (P _ Q _ R) ^ (:P _ Q _ :R) ^ (P _ :Q) 中，假设我们将 True 分配给 P。那么包含 P 的子句，即。 (P _ Q _ R) 和 (P _ :Q) 从公式中删除，而 :P 从它所在的任何子句中删除，即。 （：P_Q_：R）。这导致公式（Q_：R）。另一方面，如果我们将 False 分配给 P，则我们从公式中删除 (:P _ Q _ :R) 并从其子句中删除 P，从而获得 (Q _ R) ^ (:Q)。
     如果可以将整个公式简化为空列表，则整个公式是可满足的，因为在这种情况下，所有子句都已满足。如果整个公式中有一个空列表，则表示不满足某个子句，因此导致该状态的分配不能满足公式。
   • assign :: (Atom,Bool) -> Formula -> Formula assign 函数应该采用 (Atom,Bool) 对和一个公式，并将给定真值分配给上述公式中的原子的效果。

代码（我也从这里获得了帮助）：

module Algorithm where

import System.Random
import Data.Maybe
import Data.List

type Atom = String
type Literal = (Bool,Atom)
type Clause = [Literal]
type Formula = [Clause]
type Model = [(Atom, Bool)]
type Node = (Formula, ([Atom], Model))

-- This function  takess a Clause and return the set of Atoms of that Clause.
atomsClause :: Clause -> [Atom]
atomsClause = undefined 

-- This function  takes a Formula returns the set of Atoms of a Formula
atoms :: Formula -> [Atom]
atoms = nub . map snd 

-- This function returns True if the given Literal can be found within
-- the Clause.
isLiteral :: Literal -> Clause -> Bool
isLiteral = isLiteral = any . (==)

-- this function takes a Model and an Atom and flip the truthvalue of
-- the atom in the model
flipSymbol :: Model -> Atom -> Model -- is this ok?
flipSymbol m a = map f m  where
    f (atom, value) = if a == atom
        then (atom, not value)
        else (atom, value) 

assign :: (Atom,Bool) -> Formula -> Formula
assign = undefined --any advice here?

Answer 1

乍一看，我看不出有什么方法可以改进您的第一个公式，也许您可​​以使用逻辑函数而不是if-then-else，它更快：

flipSymbol m a = map f m where
    f (atom, value) = (atom, value /= (a == atom))

注意：/= for Bool 基本上是异或。

最后一个问题： 基本思想是比较原子，合并布尔值并摆弄逻辑操作以获得结果。基本上，它看起来像这样：

assign :: (Atom,Bool) -> Formula -> Formula
assign (a,b) = map . (map f) where
  f (x,b) = (x,(x==a)&&b)