Unit Propagation - Complexity

Complexity

The direct implementation of unit propagation takes time quadratic in the total size of the set to check, which is defined to be the sum of the size of all clauses, where the size of each clause is the number of literals it contains.

Unit propagation can however be done in linear time by storing, for each variable, the list of clauses in which each literal is contained. For example, the set above can be represented by numbering each clause as follows:

and then storing, for each variable, the list of clauses containing the variable or its negation:

This simple data structure can be built in time linear in the size of the set, and allows finding all clauses containing a variable very easily. Unit propagation of a literal can be performed efficiently by scanning only the list of clauses containing the variable of the literal. More precisely, the total running time for doing unit propagation for all unit clauses is linear in the size of the set of clauses.

Read more about this topic:  Unit Propagation

Famous quotes containing the word complexity:

    The price we pay for the complexity of life is too high. When you think of all the effort you have to put in—telephonic, technological and relational—to alter even the slightest bit of behaviour in this strange world we call social life, you are left pining for the straightforwardness of primitive peoples and their physical work.
    Jean Baudrillard (b. 1929)

    In times like ours, where the growing complexity of life leaves us barely the time to read the newspapers, where the map of Europe has endured profound rearrangements and is perhaps on the brink of enduring yet others, where so many threatening and new problems appear everywhere, you will admit it may be demanded of a writer that he be more than a fine wit who makes us forget in idle and byzantine discussions on the merits of pure form ...
    Marcel Proust (1871–1922)

    It is not only their own need to mother that takes some women by surprise; there is also the shock of discovering the complexity of alternative child-care arrangements that have been made to sound so simple. Those for whom the intended solution is equal parenting have found that some parents are more equal than others.
    Elaine Heffner (20th century)