Polytime Simplification

There are many "preprocessing" techniques that run in low-order polytime and can be used to simplify a problem before it is given to a search engine. The most common of these is "unit resolution", in which the effects of simple facts are propagated and used to subsume clauses. For example, with the set of clauses

x 
not x or y
y or z

we know x and propagating x to the second clause we obtain that y is true, which we then find that it subsumes the last clause. In this case the theory is solved by the preprocessing alone.

A more advanced technique is to test for "failed literals". If setting x to true and propagating results in a contradiction then we know that x must be false in any model. Hence we can just add "not x" to the theory, and then propagate the results of this. Such techniques are called "probing" in the operations research literature.

CIRL

Many stages of a preprocessing can be speculative. For example, with the failed literal test if setting a value does not result in a contradiction then we not have achieved any simplification. In such cases the preprocessing might well take so long that it is not worthwhile in terms of overall solution time. We work on heuristics that will select the tests that are most likely to lead to some useful result: for example, heuristics for selecting probes that are most likely to give useful information.

Pointers

Parent areas:

Knowledge Compilation

Related areas:

Lifted WSAT

Back to the CIRL Overview Page.