Plans on special cases of DPresolution which lead to "reductions".
More...
Go to the source code of this file.
Detailed Description
Plans on special cases of DPresolution which lead to "reductions".
 Todo:
 Singular DPreduction

Transfer SingDPuncontracted, ISingDPuncontracted from Mupad/Orthogonal.mup.

This should be just the randomised version of sdp_reduction_cs (easily achieved by randomly choosing a singular variable).

Perhaps the input should better be a formal clauseset, and the reduction happens inplace.

Perhaps then we better create a newfunction.

Perhaps we have a general naming scheme for distinguishing between inplace operations and operations which leave their arguments intact?

The current implementation of nonsingular_csp could be used for testing purposes, and otherwise replaced by the obvious check for the existence of a singular variable.

We need more finegrained versions which check for the various conditions interesting here:

Degeneration (at least one clause gets lost).

Clauses are as full as possible.

Compare "Decision algorithms" in Satisfiability/Lisp/MinimalUnsatisfiability/plans/DeficiencyOne.hpp.
Definition in file DPReductions.hpp.