Unit Propagation and Resolution
The second rule of unit propagation can be seen as a restricted form of resolution, in which one of the two resolvents must always be a unit clause. As for resolution, unit propagation is a correct inference rule, in that it never produces a new clause that was not entailed by the old ones. The difference between unit propagation and resolution are:
- resolution is a complete refutation procedure while unit propagation is not; in other words, even if a set of clause is contradictory, unit propagation may not generate an inconsistency;
- the two clauses that are resolved cannot in general be removed after the generated clause is added to the set; on the contrary, the non-unit clause involved in a unit propagation can be removed when its simplification is added to the set;
- resolution does not in general include the first rule used in unit propagation.
Resolution calculi that include subsumption can model rule one by subsumption and rule two by a unit resolution step, followed by subsumption.
Unit propagation, applied repeatedly as new unit clauses are generated, is a complete satisfiability algorithm for sets of propositional Horn clauses; it also generates a minimal model for the set if satisfiable: see Horn-satisfiability.
Read more about this topic: Unit Propagation
Famous quotes containing the words unit and/or resolution:
“During the Suffragette revolt of 1913 I ... [urged] that what was needed was not the vote, but a constitutional amendment enacting that all representative bodies shall consist of women and men in equal numbers, whether elected or nominated or coopted or registered or picked up in the street like a coroner’s jury. In the case of elected bodies the only way of effecting this is by the Coupled Vote. The representative unit must not be a man or a woman but a man and a woman.”
—George Bernard Shaw (1856–1950)
“The changes in our life must come from the impossibility to live otherwise than according to the demands of our conscience ... not from our mental resolution to try a new form of life.”
—Leo Tolstoy (1828–1910)