ハスケル手順

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に送ってテストすることができます。同様に、Edwardは[(True,"B"), (True,"C"), (True,"A")]を掲載している。

一般的なやり方は、関数を簡単に書かれた小さな構成要素に分割し、最後にこれらの個々の要素をコードで結合して最終的な問題を解決する方法です。我々は一般式に作用するremoveTautologiesを数式中の句に作用する助手isTautologyに分解してからグルーコードを使ってremoveTautologiesを定義します。

私はこれがあなたの問題を始めるのに役立つことを願っています。まったく無関係に思えるかもしれませんが、より高度なバリエーションがモデルチェッキングアルゴリズムで使用されていることに注意してください.CPUが正しいこと、プロトコルが動作し、最近は自動リファクタリングでも使用されていることを確認します。http://coccinelle.lip6.fr/ 。だから、この問題は現実世界での真の適用性を学ぶ良い方法です！

---

コメントセクションで返信するのではなく、ここで編集します。あなたは書いています：

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

あなたが言及しているように、このアプローチにはいくつかの問題があります。まず、ゲームでは、あなたのrt関数が句で動作しているということです。

isRemovableClause :: Clause -> Bool 

あなたが撮影したパスがリストをソートする必要があります：指定された句がトートロジーであるならば、私が単におそらく上記の言及、またはタイプでisTautologyそれを呼び出す方が良いでしょうので、それは、削除する必要がありますたとえば、[P, P, not P, Q]の場合は何をすべきかを検討してください。別のアプローチは、検索を確立することである。我々は値(not tv, name)がrestに存在する場合、この句はトートロジーでなければならないこと

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

お知らせがあるとします。それ以外の場合は、(tv, name)を捨てて、同義語をrestで探してください。 removeTautologiesにフォーカスを移動する

が、関数がisRemovableClauseを使用して書き込むことができることは明らかである：式は句のリストであるので、我々は単に句リストの中を歩くと、真のすべての人のためのisRemovableClauseリターンを削除することができます。太字のソルバはこれを達成するために高階関数であるList.filterを使用します。

Answer 2

この質問はあまりにも広すぎます：あなたが助けが必要な特定の機能に焦点を当てるならば、それほど問題はないかもしれませんが、本当に効果的にするためには、コードが何をすべきかの仕様：それだけで、これはちょうど "私の宿題をする"問題です。言われていること

は、私は（私はあなたがCNFを使用していると仮定？）あなたの説明に掲載例を取って、自分の表現に変換をお勧めします次に、あなたは

(A v B v -A)^(B v C v A) 

の線に沿って何かを持っています

は

[[(True,"A"), (True,"B"), (False,"A")], 
[(True,"B"), (True,"C"), (True,"A")]] 

になり、その結果のデータ型がどのように見える、そしてどのように厳密に計算視点からそこに着くかもしれないものを考えます。パフォーマンスについて心配しないでください。