Decision Diagrams (exam 19. Feb 2020 question 1)

0 votes

since we didn't have such a question in our assignments during the semester, I am not familiar with this question and I don't know how to solve it. Could you please explain it to me?

edited

1 Answer

0 votes

Best answer

First step, you abbreviate all subformulas with new variable names:

•  x0 <-> c & d
•  x1 <-> !x0
•  x2 <-> b | x1
•  x3 <-> a -> b

The true meaning of this is that the given formula is equivalent to the following quantified formula

```    ∃x0 x1 x2 x3.
(x0 <-> c & d) &
(x1 <-> !x0) &
(x2 <-> b | x1) &
(x3 <-> a -> b)
```

So, when we are interested in the satisfiablily of the original formula, then it is satisfiable if and only if the above quantified formula is satisfiable, and that is the case if and only if the following is satisfiable:

```        (x0 <-> c & d) &
(x1 <-> !x0) &
(x2 <-> b | x1) &
(x3 <-> a -> b)
```

The next step is to replace these equivalences with their conjunctive normal forms. You can do that in that you compute the CNF for each one, but since there is one pattern for each operator, you may prepare that also on your notes. You will find those for negation, conjunction and disjunction on slide 113 of the propositional logic chapter.

That's all. Why doing that? Since modern SAT solvers work on conjuncitve normal forms, and the problem is that in general, a conjunctive normal form may have an exponential size in terms of the length of the given formula. The above equisatisfiable clause form is having a linear size, and is sufficient for SAT checking.

by (166k points)
selected by

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer