One :Thank you Carsten Schultz,Daniel Fischer and all the other for your
help.
Two:After my last post I wrote some function that should help me in the
future,but I need some help with the followint as I'm tired and have to fit
in a schedule.I know it is long so I'll try and explain it as short and
consice as I can.
The DPLL procedure has two main stages: a simplification stage and a search
stage. In the simplification
stage, functions are applied to the formula to assign truth values to
certain propositional variables. The
simplifications are made because if there is a satisfying assignment for the
simplified formula then it is also
a satisfying assignment for the original formula. This reduces the need for
search which can take a long
time. The search stage is performed when no more simplifications can be
made. In this stage a literal is
chosen and is assigned true or false leading to two new branches in the
search space.
I wrote some function wich should be helpfull,but I have to fit in a
schedule and I'm getting tired I need some additional help if possible.
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 that I wrote:
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.
--Where do I need help:
removeTautologies :: Formula-Formula
This function should output a simplified formula if tautologies
can be found in one or more clauses in the input
Notes: If in a clause, a literal and its negation are found, it means that
the clause will be true, regardless of the value
finally assigned to that propositional variable. Consider the following
example:
(A v B v -A) ^ (B v C v A)
The first clause contains the literals A and -A. This means that the clause
will always be true, in which case
it can be simplify the whole set to simply (B v C v A) (the second clause
alone)
pureLiteralDeletion :: Formula-Formula
This function is suppose to implement a simplification step that assumes as
true any atom in a formula that appears exclusively in a positive or
negative form (not both). Consider the formula:
(P v Q v R) ^ (P v Q v -R) ^ (-Q v R)
Note that in this formula P is present but -P is not. Using Pure Literal
Deletion it can be assumed that the value of P will be True thus
simplifying the formula to (-Q v R). If the literal were false then the
literal would simply be deleted from the clauses it appears in. In that case
any satisfying model for the resulting formula would also be a satisfying
model for the formula when we assume that the literal is true. Hence this
simplification is sound in that if there is a solution to the simplified
formula then there is a solution to the original formula.
propagateUnits :: Formula-Formula
If a clause in a propositional formula contains only one literal, then that
literal must be true (so that the particular clause can be satisfied). When
this happens,we can remove the unit clauses (the ones that contain only one
literal), all the clauses where the literal appears and also, from the
remaining clauses, we can delete the negation of the literal (because if P
is true, -P will be false).For example, in the formula (P v Q v R) ^ (-P v Q
v -R) ^ (P) we have one unit clause (the third clause(P) ). Because this
