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:
“Both the man of science and the man of art live always at the edge of mystery, surrounded by it. Both, as a measure of their creation, have always had to do with the harmonization of what is new with what is familiar, with the balance between novelty and synthesis, with the struggle to make partial order in total chaos.... This cannot be an easy life.”
—J. Robert Oppenheimer (1904–1967)
“Your home is regarded as a model home, your life as a model life. But all this splendor, and you along with it ... it’s just as though it were built upon a shifting quagmire. A moment may come, a word can be spoken, and both you and all this splendor will collapse.”
—Henrik Ibsen (1828–1906)