Converting a 4cnf clause into one with not all equal literals

229 Views Asked by At

Given a 3cnf clause $$(a \lor b \lor c)$$ we can construct an equivalent conjunction $$(a\lor b\lor d) \land (\lnot d \lor c \lor \bot)$$ such that the second clause has a valid truth assignment if and only if the first clause has such an assignment, and, not all literals are set to true.

I am trying to extend this principle for a 4cnf clause. Unfortunately I am stuck and not sure how to proceed.

1

There are 1 best solutions below

0
On

For a 4-CNF clause there are two assignments that must be precluded, all literals false and all literals true, to satisfy the not-all-equal condition. All literals false is already precluded by CNF-SAT itself so you only need to block the all literals true assignment. The way to do this is to add a clause with all the literals in the original clause negated.

Example: To enforce the not-all-equal condition on the clause $$(\lnot a \lor \lnot b \lor c \lor d)$$ you would add $$(a \lor b \lor \lnot c \lor \lnot d)$$