Using A Partial Model
The unit clauses that are present in a set of clauses or can be derived from it can be stored in form of a partial model (this partial model may also contain other literals, depending on the application). In this case, unit propagation is performed based on the literals of the partial model, and unit clauses are removed if their literal is in the model. In the example above, the unit clause would be added to the partial model; the simplification of the set of clause would then proceed as above with the difference that the unit clause is now removed from the set. The resulting set of clauses is equivalent to the original one under the assumption of validity of the literals in the partial model.
Read more about this topic: Unit Propagation
Famous quotes containing the words partial and/or model:
“There is no luck in literary reputation. They who make up the final verdict upon every book are not the partial and noisy readers of the hour when it appears; but a court as of angels, a public not to be bribed, not to be entreated, and not to be overawed, decides upon every man’s title to fame. Only those books come down which deserve to last.”
—Ralph Waldo Emerson (1803–1882)
“... if we look around us in social life and note down who are the faithful wives, the most patient and careful mothers, the most exemplary housekeepers, the model sisters, the wisest philanthropists, and the women of the most social influence, we will have to admit that most frequently they are women of cultivated minds, without which even warm hearts and good intentions are but partial influences.”
—Mrs. H. O. Ward (1824–1899)