Talk:Unit propagation

Is this actually correct?! By the very definition (and another definition I have here), the example is wrong because the {a} clause should have been deleted, giving:

{c}, {!c, d}

not

{c}, {!c, d}, {a}

Or is my understanding flawed? MikeHearn 22:09, 10 February 2006 (UTC)[reply]

According to the definition of the article, the elimination is to be done for all clauses containing a but a itself ("the other clauses are simplified..."). If you use unit propagation in a backtracking-based algorithm (more generally, if you have a partial current assignment), you may as well remove a, provided that a is added to the current partial evaluation. I have no idea of which definition is actually the most common in textbooks. You mention another definition you have: which one is that? - Liberatore(T) 11:30, 11 February 2006 (UTC)[reply]

The current page is just confusing. All other defintions I have seen would also remove the unit clause {a}. Why would you not keep a partial truth assignment?! There is no point in running unit propagation on a clause-set unless you keep a truth assignment, that's what unit propagation is designed for; constructing a truth assignment!

I made the edit yesterday, if you disagree then fair enough but all papers and textbooks that I've read would remove unit clause {a}. RogerWillis 14:54, 08 April 2006 (BST)

I added a section "Using a partial model" to explain when unit clauses can be removed. IMO, saying that clauses before=clauses after is simpler than saying partial model|=clause before=clauses after. - Liberatore(T) 10:52, 10 April 2006 (UTC)[reply]

Is the second rule correct? "in every clause that contains not{a} this literal is deleted." What happens if you have " not{a} ^ b"? If you delete the not{a} you are change the problem? Or am I mistaken? —Preceding unsigned comment added by 66.176.222.83 (talk) 02:33, 5 March 2011 (UTC)[reply]

The formula must be in CNF so clauses cannot contain conjunctions AntPraxis (talk) 16:59, 10 April 2020 (UTC)[reply]