Equi-Satisfiable Linear-Size Clause Form

Question

VRS_PropLogic: pg 123

"if a subformula has only positive or only negative occurences, then implications are sufficient for abbreviating the new variables"

From what I understand, the linear clause form for a formula :

b ->  a &(b|c)

_______________________

x0 -> (b|c) : {!x0, b,c}

x1-> (a&c) : {!x1,a}, {!x1,x0}

x2 -> (b ->x1) : {!x2, !b, x1}

x2: {x2}

_________________________

Am I correct in deducing this would also be a valid linear-clause formula?

I only see the solution for "↔" in the exam solutions. Would the implication solution also be accepted?

Answer 1

Of course, you can use the optimization when we have only positive occurrences. Your computation is correct, and you can even eliminate the final x2:

    x0 -> (b|c)
    x1 -> a&x0
    b->x1