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)
“Some hours seem not to be occasion for any deed, but for resolves to draw breath in. We do not directly go about the execution of the purpose that thrills us, but shut our doors behind us and ramble with prepared mind, as if the half were already done. Our resolution is taking root or hold on the earth then, as seeds first send a shoot downward which is fed by their own albumen, ere they send one upward to the light.”
—Henry David Thoreau (1817–1862)