haskell 程序

Question

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]


-- This function  takes a Formula returns the set of Atoms of a Formula
atoms :: Formula -> [Atom]


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


-- 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?

Additional functions :
remove :: (Eq a) )a ->[a] ->[a] 
-This function removes an item from a list.

 neg :: Literal->Literal
-This function flips a literal (ie. from P to :P and from :P to P).
falseClause :: Model -> Clause -> Bool 
-This function takes a Model and a Clause and returns True
if the clause is unsatisfied by the model or False otherwise.
falseClauses :: Formula -> Model -> [Clause]
-This function takes a Formula and a Model and returns the list of clauses of the  formula that are not satisfied.
 assignModel :: Model -> Formula -> Formula 
 -This function applies the assign function for all the assignments of a given model.
 checkFormula :: Formula -> Maybe Bool This function checks whether a formula can be  decided to be satisfiable or unsatisfiable based on the effects of the assign function.
 satisfies :: Model -> Formula -. Bool This function checks whether a model satisfies a formula. This is done with the combination of the assignModel and checkFormula functions.

Answer 1

从一个地方开始:看看

 removeTautologies :: Formula -> Formula

现在假设我们可以编写一个函数

 isTautology :: Clause -> Bool

然后我们可能有机会使用该函数来过滤一般公式。所以我会尝试忽略除了函数 isTautology 之外的所有内容。本质上，这里的问题是:什么是同义反复以及我们如何检测它？Edward Z. Yang 发表的一些想法绝对可以帮助您理解什么是同义反复正在进行中。在这种情况下，我们可以查看子句 [(True,"A"), (True,"B"), (False,"A")] 并尝试将其提供给 isTautology 用于测试它。与爱德华发布的其他子句类似，[(True,"B"), (True,"C"), (True,"A")]。

一般的技巧是弄清楚如何将函数分解为更小的易于编写的组成部分，然后将这些单独的部分与代码粘合在一起以解决最终问题。我们正在将适用于一般公式的 removeTautologies 分解为可适用于公式中子句的帮助器 isTautology，然后我们寻求定义 removeTautologies通过一些过滤粘合代码来实现。

我希望这可以帮助您开始解决您的问题。它可能看起来完全无关紧要，但请注意，模型检查算法中使用了更高级的变体，这些算法验证您的 CPU 是否正确、协议(protocol)行为，并且最近也已用于自动重构，请参阅 http://coccinelle.lip6.fr/供使用。所以这个问题是学习现实世界中一些严肃的适用性的好方法!

<小时/>

我会在这里编辑它以帮助您，而不是在评论部分回复。您写道:

rt ((x, x') : (y, y') : rest) | x' == y' = rt rest
                              | otherwise = (x, x') : rt ((y, y') : rest)

正如您提到的，这种方法存在一些问题。首先，游戏是您的 rt 函数正在处理子句。如果给定的子句是重言式，则应将其删除，因此最好使用我上面提到的类型将其称为 isTautology，或者简单地:

isRemovableClause :: Clause -> Bool

您所采取的路径要求您按字典顺序对子句中的列表进行排序，然后考虑在有 [P, P, not P, Q] 的情况下该怎么做。另一种方法是建立搜索。假设我们有

isRemovableClause ((tv, name) : rest) = ...

请注意，如果 rest 中存在值(not tv, name)，则此子句必须是同义反复。否则，我们可以丢弃(tv, name)并在rest中寻找同义反复。

将焦点移至 removeTautologies，很明显可以使用 isRemovableClause 来编写该函数:公式是子句列表，因此我们可以简单地遍历子句列表并删除所有 isRemovableClause 返回 true 的子句。粗体求解器将使用 List.filter(一个高阶函数)来实现此目的。