COSC1127/1125 Artificial Intelligence
School of Computing Technologies Semester 2, 2021
Prof. ̃a
Tutorial No. 4
KR&R I – Propositional Logic
The aim of this tutorial to familiarise you with logical propositions and how they are used to make inferences and represent knowledge about the state of the world. You are not expected to complete all problems in the tutorial session, and you can always catch up and complete unsolved problems later.
A propositional sentence or formula is:
• A propositional letter, often written as p or q. • ¬P where P is a sentence.
• P ∧ Q where P and Q are sentences.
• P ∨ Q where P and Q are sentences.
• P ⇒ Q where P and Q are sentences.
• P ⇔ Q where P and Q are sentences.
Sometimes we also define exclusive or as P ⊕ Q where P and Q are sentences.
We refer to ¬, ∧, ∨, ⇒, ⇔ and ⊕ as logical connectives. In some places, you will find → or ⊃ used instead of ⇒ for implication and ≡ instead of ⇔. In those cases, the symbol ⇔ is generally used for logical equivalence (i.e., two formulas that have exactly the same truth table).
An interpretation in propositional logic is a truth assignment (or valuation) mapping each atomic propositions to either true or false.
A truth table shows the truth value of formulas of interest per possible interpretation of the domain. The truth table showing the semantics (i.e., meaning) of each of the above logical connectives is as follows:
P Q ¬P P∧Q P∨Q P⇒Q P⇔Q P⊕Q TTFTTTTF TFFFTFFT FTTFTTFT FFTFFTTF
A propositional formula is:
• Satisfiable: if there is at least one truth assignment that makes it true.
• Valid or Tautology: if every truth assignment makes it true. A formula that is valid is also satisfiable.
• Unsatisfiable: if there is no truth assignment that makes it true (so that all truth assignments make it false).
Two formulas P and Q are logically equivalent (denoted P ≡ Q) iff P ⇒ Q and Q ⇒ P (and hence P ⇔ Q) are tautologies. It means their truth value coincide on every interpretation (i.e., they have the same truth table). For example P ∨ Q is logically equivalent to Q ∨ P and to ¬(¬P ∧ ¬Q).
1
COSC1127/1125 – AI Tutorial 4: KR&R I – Propositional Logic Page 2 of 15
PART1: BasicLogic……………………………………………………………………… (a) Use truth tables to show that the following are valid (i.e. that the equivalences hold).
P ∧(Q∨R)⇔(P ∧Q)∨(P ∧R) ¬(P ∧ Q) ⇔ (¬P ∨ ¬Q)
¬(P ∨ Q) ⇔ (¬P ∧ ¬Q)
(P ⇒ Q) ⇔ (¬Q ⇒ ¬P )
Distributionof∧ de Morgan’s Law de Morgan’s Law Contraposition
(P ⇒ Q) ⇔ (¬P ∨ Q)
Solution: These truth tables are very easy to find online.
(b) Foreachofthefollowingsentences,decidewhetheritisvalid,unsatisfiable,orsatisfiablebutnotvalid. Firstly, trying “guessing” the answer; then evaluate each properly (e.g. using truth tables). How did your guesses match up?
i. Smoke ⇒ Smoke
Solution:
Basically, just draw the truth table for each sentence – if the whole column for the sentence is T, then it is valud, if the whole column for the sentence is F, then it is unsatisfiable; neither otherwise. Eg.:
S S⇒S TT FT
Therefore, it is valid.
ii. Smoke ⇒ F ire
iii. (Smoke ⇒ F ire) ⇒ (¬Smoke ⇒ ¬F ire)
Solution:
SFS⇒F TTT TFF FTT FFT
Satisfiable but not valid.
Solution:
A : (S ⇒ F )
B : (¬S ⇒ ¬F)
S F ¬S ¬F A B A⇒B TTFFTTT TFFTFTT FTTFTFF FFTTTTT
Satisfiable but not valid.
iv. Smoke ∨ Fire ∨ ¬Fire Solution: Your turn!
v. ((Smoke ∧ Heat) ⇒ Fire) ⇔ ((Smoke ⇒ Fire) ∨ (Heat ⇒ Fire)) Solution: Your turn!
vi. (Smoke ⇒ Fire) ⇒ ((Smoke ∧ Heat) ⇒ Fire)
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise1continuesonthenextpage…
COSC1127/1125 – AI Tutorial 4: KR&R I – Propositional Logic Page 3 of 15
Solution:
S F H S⇒F S∧H S∧H⇒F (S⇒F)⇒(S∧H⇒F) TTTTTTT TTFTFTT TFTFTFT TFFFFTT FTTTFTT FTFTFTT FFTTFTT FFFTFTT
This it is a validity (or tautology) as it holds in every possible interpretation.
To see it from another angle, suppose we want to prove that the implication (S ⇒ F ) ⇒ (S ∧ H ⇒ F ) is true always, that is, it is a validity/tautology:
• Sinceitisanimplication,theonlypossiblewaythisistrueisif(S⇒F)istrue,but(S∧H⇒ F ) is false.
• Nowfor(S∧H⇒F)tobefalse,S∧HhastobetrueandFfalse.
• ButifS∧Histrue,thenSistrue.
• Because we already assumed in the first item that (S ⇒ F ), then together with S being true,
we know that F has to be true, which contradicts our second item.
• Hence, the whole implication cannot actually be made false, that is, it is a validity: always
true in every possible interpretation.
vii. Big ∨ Dumb ∨ (Big ⇒ Dumb)
Solution:
X : (B ∨ D) Y : (B ⇒ D)
BDXYX∨Y TTTTT TFTFT FTTTT FFFTT
Valid.
viii. (Big ∧ Dumb) ∨ ¬Dumb Solution: Your turn!
(c) Consider the natural language statement “If A then B else C” (in other words, if A is true then B is true, and otherwise C is true). Give two different formulas in propositional logic that capture that statement formally.
(d) Prove that ¬(P ⇒ Q) and ¬(¬Q ⇒ ¬P ) are all equivalent without using a truth-table
Hints:
The “if-then” conditional statement is represented by logical implication, so “If A then B” is just A ⇒ B, have a think about how you could represent “else”
Solution: (Note: this is a partial solution)
Of course the truth table would be:
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise1continuesonthenextpage…
COSC1127/1125 – AI Tutorial 4: KR&R I – Propositional Logic Page 4 of 15
P Q ¬P ¬Q ¬(P ⇒Q) P ∧¬Q ¬(¬Q⇒¬P) TTFFFFF TFFTTTT FTTFFFF FFTTFFF
Your turn! It is up to you to prove it without the truth table now.
We need to show first that if ¬(P ⇒ Q) is true in an interpretation I, then ¬(¬Q ⇒ ¬P) is true in I.
Then we need to show that if ¬(¬Q ⇒ ¬P ) is true in an interpretation I , then ¬(P ⇒ Q) is also true in I.
(e) Represent the following sentences in propositional logic. Can you prove that the unicorn is mythical? What about magical? Horned?
If the unicorn is mythical, then it is immortal, but if it is not mythical, then it is a mortal mammal. If the unicorn is either immortal or a mammal, then it is horned. The unicorn is magical if it is horned.
Solution: You can translate the sentences into the following propositional logic expressions: 1. mythical ⇒ ¬mortal
2. ¬mythical ⇒ mortal ∧ mammal 3. ¬mortal ∨ mammal ⇒ horned 4. horned ⇒ magical
From statements (a) and (b), we see that if it is mythical, then it is immortal; otherwise it is a mammal. So it must be either immortal or a mammal, and thus horned. That means it is also magical. However we cannot deduce anything about whether it is mythical.
PART2: Resolution………………………………………………………………………. First, let us go over an example in full. The resolution method can be used to prove that a CNF formula (a set of clauses) is unsatisfiable, by deriving the empty clause. Consider, for example, the following CNF formula:
φ = (¬T ∨ E) ∧ (T ∨ ¬E) ∧ (M ∨ ¬G) ∧ (¬E ∨ ¬C) ∧ (T ∨ ¬M) ∧ G ∧ C Here is a resolution proof for the empty clause:
1. (M∨¬G)
2. (T∨¬M)
3. (¬G∨T)
4. (¬T∨E)
5. (¬G∨E)
6. (¬E∨¬C)
7. (¬G ∨ ¬C)
8. G
9. C
10. (¬C )
11. ()
clause in φ clause in φ resolution 1,2 clause in φ resolution 3,4 clause in φ resolution 5,6 clause in φ clause in φ resolution 7,8 resolution 9,10
Note that clause (T ∨ ¬E) in φ was never used, so even if we drop such clause from φ, it still remains unsatisfiable. Also observe that, in many cases, there could be more than one (correct) resolution proof deriving the empty clause.
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise2continuesonthenextpage…
COSC1127/1125 – AI Tutorial 4: KR&R I – Propositional Logic Page 5 of 15
Another way of showing a resolution proof is using a graphical representation of the proof and using sets of literals to denote clauses:
{E,¬T} {¬C,¬E} {¬G,M} {¬M,T} {G} {C}
{¬T,¬C} {¬G,T}
{T}
∅
(Colours are added to show the order in which the resolutions occur: red ⇒ blue ⇒ green ⇒ magenta). OK, now, let’s do some exercises….
(a) Use propositional resolution to prove that the following sets of clauses are unsatisfiable. Observe how clauses are now represented via set notation!
i. {{p,q},{¬p,r},{¬p,¬r},{p,¬q}}.
{¬C }
Solution:
Here is a resolution proof for the
1. 2. 3. 4. 5. 6. 7. 8. 9.
empty clause (sets of clauses are unsatisfiable):
It can also solve using a resolution graph.
φ = (p∨q)∧(¬p∨r)∧(¬p∨¬r)∧(p∨¬q)
(p∨q) (p∨¬q) (p∨p) (¬p∨r) (¬p ∨ ¬r) (¬p ∨ ¬p) p
(¬p) ()
clause in φ clause in φ resolution 1,2 clause in φ clause in φ resolution 4,5 resolution 3 resolution 6 resolution 7,8
ii. {{p,q},{¬r,s},{¬p,r,s},{¬q,¬r},{p,¬s},{¬p,¬r},{r}}. Solution: Your turn!
(b) Show that the following statements are true by giving an appropriate resolution proof. You will need to convert formulas to CNF before doing a resolution proof.
i. p∧(p⇒q)|=q
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise2continuesonthenextpage…
COSC1127/1125 – AI Tutorial 4: KR&R I – Propositional Logic Page 6 of 15
Solution:
Remember that KB |= φ (i.e., KB entails φ: whenever KB is true in an interpretation, so is φ) is true if and only if KB ∧¬φ is unsatisfiable. To show that KB ∧¬φ is unsatisfiable, we convert KB and ¬φ into CNF, and do a resolution proof to achieve the empty clause (i.e., a contradiction).
Here, KB is p ∧ (p ⇒ q) and query is φ = q. So, we want to show that the following is unsatisfiable: KB ∧¬φ = p ∧ (p ⇒ q) ∧ ¬q
If we convert this to CNF, we are to prove that the following formula is unsatisfiable:
ψ = p ∧ (¬p ∨ q) ∧ ¬q Here is a resolution proof for the empty clause:
1. (¬p∨q)
2. p
3. q
4. (¬q)
clause in ψ clause in ψ resolution 1,2 clause in ψ resolution 3,4
5. ()
As we have shown that ψ = KB ∧¬φ is unsatisfiable, we know that φ must be true and KB |= q. ■
ii. p ∧ (p ⇒ q) ∧ (q ⇒ r) |= r
Solution: (Note: this is a partial solution)
Here, KB is p ∧ (p ⇒ q) ∧ (q ⇒ r) and query is φ = r. So, we want to show that the following is unsatisfiable:
(Your turn!)
If we convert this to CNF, we are to prove that the following formula is unsatisfiable:
(Your turn!) Here is a resolution proof for the empty clause:
(Your turn!)
As we have shown that ψ = KB ∧¬φ is unsatisfiable, we know that φ must be true and KB |= r. ■
iii. (p ⇒ (q ⇒ r)) ∧ (r ⇒ s) ∧ p |= ¬q ∨ s Solution: Your turn!
iv. (p∨r)∧(p⇒(q∨s))∧(r⇒t)|=q∨s∨t
Solution:
Here, KB is (p ∨ r) ∧ (p ⇒ (q ∨ s)) ∧ (r ⇒ t) and query is φ = q ∨ s ∨ t. So, we want to show that the following is unsatisfiable:
KB ∧¬φ = (p ∨ r) ∧ (p ⇒ (q ∨ s)) ∧ (r ⇒ t) ∧ ¬(q ∨ s ∨ t)
If we convert this to CNF, we are to prove that the following formula is unsatisfiable:
ψ = (p ∨ r) ∧ (¬p ∨ q ∨ s) ∧ (¬r ∨ t) ∧ ¬q ∧ ¬s ∧ ¬t Here is a resolution proof for the empty clause:
1. (p ∨ r) clause in ψ
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise2continuesonthenextpage…
COSC1127/1125 – AI Tutorial 4: KR&R I – Propositional Logic Page 7 of 15
2. (¬p∨q∨s)
3. (r∨q∨s)
4. (¬r∨t)
5. (q∨s∨t)
6. (¬q)
7. (s∨t)
8. (¬s)
9. t
10. (¬t)
11. ()
clause in ψ resolution 1,2 clause in ψ resolution 3,4 clause in ψ resolution 5,6 clause in ψ resolution 7,8 clause in ψ resolution 9,10
As we have shown that ψ = KB ∧¬φ is unsatisfiable, we know that φ must be true and KB |= q∨s∨t. ■
v. p∧r∧(p⇒q)∧((q∧r)⇒(s∨t))∧¬s|=t Solution: Your turn!
(c) Complete the truth table below. What does this tell you about resolution proofs?
P Q R ¬P ∨Q P ∨R (¬P ∨Q)∧(P ∨R) Q∨R ((¬P ∨Q)∧(P ∨R))⇒(Q∨R) TTTTTTTT TTFTTTTT TFTFTFTT TFFFTFFT FTTTTTTT FTFTFFTT FFTTTTTT FFFTFFFT
Solution: As the formula ((¬P ∨ Q) ∧ (P ∨ R)) ⇒ (Q ∨ R) is valid, this means that each resolution step is correct, and hence resolution proofs are correct.
RMIT AI 2021 (Semester 2) – ̃a
COSC1127/1125 – AI Tutorial 4: KR&R I – Propositional Logic Page 8 of 15
PART 3: Knowledge representation………………………………………………………… (a) For the following Wumpus world:
i. Develop a notation capturing the important propositions.
ii. How would you express in a propositional logic sentence:
α) Ifsquare[2,2]hasnosmellthentheWumpusisnotinthissquareoranyoftheadjacentsquares?
β) If there is stench in square [1, 2] there must be a Wumpus in this square or any of the adjacent squares?
iii. Giventhattheagentisstandinginsquare[1,1]andcansee(andsmell)alladjacentsquares,including diagonals; ; how can the agent deduce that the Wumpus is in square [1, 3] using the laws of inference in propositional logic and the formulas constructed in the previous question.
Solution:
Sxy, Wxy, Bxy, Gxy, Pxy, Yxy
The above denotes the sentence “there is a Stench/Wumpus/Breeze/Gold/Pit/You in square [x,y]”.
Solution:
Solution:
¬S22 ⇒ ¬W22 ∧¬W21 ∧¬W12 ∧¬W32 ∧¬W23 (1)
S12 ⇒W11 ∨W12 ∨W22 ∨W13 (2)
Solution:
We are told that ¬S22 ∧ S12
and And Elimination applied to the above Equation 1 gives:
¬W22 ∧ ¬W21 ∧ ¬W12 ∧ ¬W32 ∧ ¬W23, (3) applied to Equation 2 gives:
W11 ∨W12 ∨W22 ∨W13, (4)
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise3continuesonthenextpage…
COSC1127/1125 – AI Tutorial 4: KR&R I – Propositional Logic Page 9 of 15
Unit Resolution is applied to Equation 4 based on Equation 3, and also we know the agent has been to square [1, 1], hence ¬W11. Therefore, W13
iv. How many propositions are required to fully capture the world in a single formula? What about a general world of size n?
(b) Represent the following “blocks world” scene in propositional calculus.
(c) Consider the following information available in the domain of thing encountered at sea: 1. None of the unnoticed things are mermaids.
2. Anything entered into the log is sure to be worth remembering.
3. I have never seen anything worth remembering when on a voyage. 4. Anything that is noticed is sure to be recorded in the log.
Formalise the problem in propositional logic and use resolution to formally prove that I have never seen a mermaid at sea using the following atomic propositions:
L: entered into the log
M: is a mermaid
S: seen by me
N: noticed
W : worth remembering
Solution:
For a 4 × 4 world with 6 propositions, we need 4 × 4 × 6 = 96
¬S11 ∧¬W11 ∧¬B11 ∧¬G11 ∧¬P11 ∧Y11 ∧S12 ∧¬W12 ∧···∧P44 ∧¬Y44
Generally, we would need 6n2 propositions.
Solution: One example:
Aontable ∧ Bontable ∧ ConB ∧ Asquare ∧ Bsquare ∧ Ctriangle
Solution:
Assertion
1 2 3 4
Implication
¬N ⇒ ¬M L ⇒ W S ⇒ ¬W N ⇒ L
Clause in KB (N ∨ ¬M) (¬L ∨ W ) (¬S ∨ ¬W ) (¬N ∨ L)
“I have never seen a mermaid at sea” can be formally written as (S ⇒ ¬M ) or, in CNF (¬S ∨ ¬M ).
RMIT AI 2021 (Semester 2) – ̃a
COSC1127/1125 – AI Tutorial 4: KR&R I – Propositional Logic Page 10 of 15
Take KB to be the conjunction of all the CNF formulas in the table above. Then, we must prove that KB ∧¬(¬S ∨ ¬M ) is unsatisfiable (see, the query has been negated). This is equivalent to proving that KB ∧S ∧ M (we will call this formula φ), which is in CNF, is unsatisfiable.
Here is a resolution proof for the empty clause:
1. (¬S∨¬W)
2. (W∨¬L)
3. (¬S ∨ ¬L)
4. (L∨¬N)
5. (¬S∨¬N)
6. (N∨¬M)
7. (¬S∨¬M)
8. S
9. (¬M )
10. M
11. ()
As we have shown that KB ∧S ∧M is unsatisfiable, we ■
clause in φ clause in φ resolution 1,2 clause in φ resolution 3,4 clause in φ resolution 5,6 clause in φ resolution 7,8 clause in φ resolution 9,10
know that the query must be true and (S ⇒ ¬M ).
PART 4: Knowledge bases and resolution ………………………………………………….. (a) Consider a knowledge base built of just these three weird implications:
¬A ⇒ B B⇒A
A ⇒ (C ∧ D)
i. Prove formula A ∧ C ∧ D using only, or explain why this is not possible.
ii. Prove formula A ∧ C ∧ D using resolution.
Solution:
It is not possible using only: is not applicable to any pair of formulas in the knowledge base. An example of using is:
When it is cold, I always wear my jacket (C ⇒ J)
It is cold (C)
Therefore, I am wearing my jacket (J)
Solution:
Proof by refutation:
1. A ∨ B premise.
2. ¬B ∨ A premise.
3. ¬A ∨ C premise.
4. ¬A ∨ D premise.
5. ¬A ∨ ¬C ∨ ¬D negated thesis. 6. A resolution 1, 2.
7. C resolution 3, 6
8. D resolution 4, 6.
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise4continuesonthenextpage…
COSC1127/1125 – AI Tutorial 4: KR&R I – Propositional Logic Page 11 of 15
9. ¬C ∨ ¬D resolution 5, 6. 10. ¬D resolution 7, 9.
11. ⊥ resolution 8, 10
This can also be proved using a resolution tree:
{A, B} {¬B, A} {¬A, C}
{A}
{¬A, D}
{¬A, ¬C, ¬D}
{¬C, ¬D}
{C}
{D}
Here we use the clausal set notation where set {P, ¬Q} denotes clause (P ∨ ¬Q)
∅
{¬C }
(b) Given the following symbols and sentences: C to indicate that Gianni is a climber;
F to indicate that Gianni is fit; L to indicate that Gianni is lucky; E to indicate that Gianni climbs mount Everest.
i. Formalize the above sentences in propositional logic:
If Gianni is a climber and he is fit, he climbs mount Everest.
If Gianni is not lucky and he is not fit, he does not climb mount Everest. Gianni is fit.
ii. Tell if the KB buit in above is consistent, and tell if some of the following sets are models for the above sentences:
{}; {C, L}; {L, E}; {F, C, E}; {L, F, E}.
(Recall that for the binary variables A, B and C; the set S = {A, C} means A and C are true, and B is false. S is said to be a model of KB iff all statements in KB are true for that given assignment of the variables)
Solution:
(C ∧ F ) ⇒ E (¬L ∧ ¬F ) ⇒ ¬E F
Solution: (Note: this is a partial solution)
The KB is consistent: it has at least a model, as the following check shows. • {}isnotamodel(itmodels1and2butnot3).
• {C,L}Yourturn!
• {L,E}Yourturn!
• {F,C,E}isamodel. • {L,F,E}Yourturn!
(c) Prove the propositional formula [(A ⇒ C) ∨ (B ⇒ C)] ⇒ [(A ∧ B) ⇒ C] is valid using resolution.
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise4continuesonthenextpage…
COSC1127/1125 – AI Tutorial 4: KR&R I – Propositional Logic Page 12 of 15
Solution: (Note: this is a partial solution)
We can prove this with resolution in the following way:
In the over-all implication, we can take the antecedent to be (A ⇒ C) ∨ (B ⇒ C) and the consequent
to be (A ∧ B) ⇒ C.
Putting the antecedent into CNF gives the single clause (¬A ∨ C ∨ ¬B). Putting the consequent into CNF gives ¬(A ∧ B) ∨ C ≡ ¬A ∨ ¬B ∨ C. As we are trying to prove the consequent, it must be negated: A ∧ B ∧ ¬C
The formula can now be shown to be valid using resolution: Your turn!
(d) Let A, B, C be propositional symbols. Given KB = {A ⇒ C,B ⇒ C,A ∨ B}, tell whether C can be derived from KB or not. Use resolution.
Solution:
C can be derived with Resolution: 1. ¬A∨C.
2. ¬B∨C.
3. A∨B.
4. ¬C negated thesis 5. B∨Cfrom1and3. 6. C from2and5.
7. {} from 4 and 6.
This can also be proved using a resolution tree:
{¬A, C} {¬B, C}
{A, B} {¬C}
{A,C}
{C}
∅
(e) Heads, I win. Tails, you lose. Use propositional resolution to prove that I always win.
Solution: (Note: this is a partial solution)
We use H and T to signal heads or tails, resp. Also IW and IL to denote I win or lose, respectively, and YW and YL to denote you win or lose, resp. To formalize the problem we have:
1. IwiniffIdon’tlose:IW ⇔¬IL or(IW ⇒¬IL)∧(¬IL ⇒IW)or{{¬IW,¬IL},{IL,IW}}. 2. You win iff you don’t lose: …. .
3. Zero-sum game: …. .
4. Coin either tails or heads: …. .
5. “Heads,Iwin”:H⇒IW ≡{¬H,IW}.
RMIT AI 2021 (Semester 2) – ̃a
COSC1127/1125 – AI Tutorial 4: KR&R I – Propositional Logic Page 13 of 15
6. “Tails, you lose”: …. .
We need to prove that I always win, that is, that IW is entailed by the above formulas. We convert all the
abovetoclausalformandthendoresolutionwiththoseclausesplus¬IW andarrivetoemptyclause. {H,T}{¬H,IW}{¬T,YL}{¬YL,IW}{¬IW,YL}{¬IW,¬IL}{IL,IW}{¬YW,¬YL}{YL,YW}{¬IW}
{T,IW} {IW,YL}
{IW }
∅
Here, we can see that there is a lot of redundancy in the KB. Although we have not used all of the clauses, so long as we are able to derive a contradiction, the resolution is valid.
PART5: SATTechnology…………………………………………………………………. Satisfiability in propositional logic (named SAT) is a very active area of research and used in the industry, for constraint satisfaction, optimisation, planning, etc.
(a) Research and explain what is the DIMACS format used as a standard for specifying CNF formulas (and used by most SAT solvers). Check, for example this and this.
Solution:
• The CNF file format is an ASCII file format.
• The file may begin with comment lines. The first character of each comment line must be a lower
case letter ”c”. Comment lines typically occur in one section at the beginning of the file, but are
allowed to appear throughout the file.
• Thecommentlinesarefollowedbythe”problem”line.Thisbeginswithalowercase”p”followed
by a space, followed by the problem type, which for CNF files is ”cnf”, followed by the number
of variables followed by the number of clauses.
• The remainder of the file contains lines defining the clauses, one by one.
• A clause is defined by listing the index of each positive literal, and the negative index of each
negative literal. Indices are 1-based, and for obvious reasons the index 0 is not allowed.
• The definition of a clause may extend beyond a single line of text. The definition of a clause is
terminated by a final value of ”0”.
• The file terminates after the last clause is defined.
(b) Get a SAT solver (e.g., MiniSAT SAT; SAT4j, file sat4j.jar; or Microsoft Z3 Prover), and test it on some CNF files in DIMACS format from here.
Solution: The official MiniSAT solver can be found here. Binaries are available for Linux and Windows under Cywin.
The SAT4j solver is Java-based so it runs on any platform, Linux, Mac, or Windows. You just need, of coure, Java JRE installed.
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise5continuesonthenextpage…
COSC1127/1125 – AI Tutorial 4: KR&R I – Propositional Logic Page 14 of 15
What is more, you can even check it with an online version of the solver here. Just paste the content of your DIMACS file there and click Ready on the upper right corner!
(c) Finally, select TWO unsatisfiable task in this tutorial, build the corresponding DIMACS files, and use MiniSAT SAT on them to prove unsatisfiablity.
Solution:
Please check this video that explains this solution in more detail. For the sea domain problem (Part 3.(c)):
p cnf 5 6 1 -2 0
-3 4 0
-5 -4 0 -1 3 0 50
20
When ran on SAT4j, you get:
SAT]$ java -jar sat4j.jar MiniSAT sea-domain.cnf
c SAT4J: a SATisfiability library for Java (c) 2004 Berre
c version 1.0.290RC
c
c solving tute-07-sea-domain.cnf
c reading problem time 0.012
c #vars 5
c #clauses 4
s UNSATISFIABLE
c Total CPU time (ms) : 0.015
When ran in this online SAT solver, the output is (check the word UNSATISFIABLE):
c CryptoMiniSat version 5.6.8
c CryptoMiniSat SHA revision 0acd09613073840747161396ac47abf35ec29320 c — header says num vars: 3
c — header says num clauses: 5
c — clauses added: 6
c — xor clauses added: 0
c — vars added 5
s UNSATISFIABLE
c ——- FINAL TOTAL SEARCH STATS ———
c restarts :0
c blocked restarts :0
c decisions :0
c propagations :0
c decisions/conflicts : 0.00 c conflicts :0
c conf lits non-minim :0
c conf lits final : 0.00 c cache hit re-learnt cl :0
c red which0 :0
c props/decision : 0.00 c props/conflict : 0.00 c 0-depth assigns :5
(0.00 confls per restart)
(0.00 per normal restart)
(0.00 % random)
(0.00 lit/confl)
(0.00 % of confl)
(0.00 % of confl)
(100.00 % vars)
RMITAI2021(Semester2)-SebastianSardin ̃a Exercise5continuesonthenextpage…
COSC1127/1125 – AI Tutorial 4: KR&R I – Propositional Logic Page 15 of 15
c [occ-substr] long subBySub: 0 subByStr: 0 lits-rem-str: 0 c[scc]new:0BP0M T:0.00
c Conflicts in UIP : 0
c Mem used : 0.00 MB
RMIT AI 2021 (Semester 2) – ̃a
End of tutorial worksheet