Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

917 questions

1k answers

1.4k comments

441 users

+4 votes

I've tried to solve Task 3 e on the first exercise sheet in VRS and always get rejected.

I've verified my solution through multiple online tools and calculated it multiples times by myself (this task is very trivial and can be done in 3 steps).

The automatic check still says "incorrect solution". So i was wondering if there might be a mistake in the solution or the question itself.

The task was to convert x <-> (y1 ^ y2) into its CNF

(¬X ∨ Y1) ∧ (¬X ∨ Y2) ∧ (¬Y1 ∨ ¬Y2 ∨ X)  (is my and the online tools solution)

Thanks for the help

closed with the note: Question was answered
in * TF "Emb. Sys. and Rob." by (230 points)
closed by

1 Answer

+3 votes

Thank you for your question! I'm really glad to see that this exercise is already being worked on!

It looks to me that you are entering the solution for x ↔ (y1 ∧ y2) or x <-> (y1 & y2). Please note that the circonflexe ^ is XOR or ⊕.

Out of curiosity: Which online tools did you use to verify your solution and how did you do so? I used the Embedded Systems Group's teaching tools on propositional logic. As an output, I used the truth table, and as an input used entered the variables x,y1,y2 and the formulas

(¬x ∨ y1) ∧ (¬x ∨ y2) ∧ (¬y1 ∨ ¬y2 ∨ x);
x <-> (y1 ^ y2)

The result was this truth table:

xy1y2(!x|y1)&(!x|y2)&(!y1|!y2|x)x<->!(y1<->y2)
00011
00110
01010
01101
10000
10101
11001
11110

You can see that only for two assignments the formulas evaluate to the same result. Another way of telling these formulas apart would have been connecting the two formulas with ↔ and checking it for tautology. The following sequent calculus proof tree is generated for an XOR between the two formulas. (Note that XOR is precisely the negation of ↔.)

The sequent calculus proof tree telling the formulas apart. Note that there are green leaves much mans it is satisfiable. Hence, the formulas do differ.

From the green leaves, you can tell that the new xor-formula is satisfiable which means that its operands differ.

Here is another trick on reading the resulting cnf: A → B is the same as (¬A ∨ B), hence your formula can be read as
(X → Y1) ∧ (X → Y2) ∧ (¬X → (¬Y1 ∨ ¬Y2))
This means that there three if-statements:

  • if Y is satisfied, Y1 is satisfied too
  • if Y is satisfied, Y2 is satisfied too
  • if Y is not satisfied, at least one of Y1, Y2 is not satisfied
One can easily tell that this this the conjunction ∧.
by (25.6k points)
edited by
ahhh i thought it was the "AND" symbol. That explains alot.
Thank you very much :)
I just updated the answer. Which online tools did you use and how?
Imprint | Privacy Policy
...