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

912 questions

1k answers

1.4k comments

441 users

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?

in * TF "Emb. Sys. and Rob." by (1.7k points)
edited by

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 (142k points)
selected by

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...