DP-Reductions.hpp File Reference

Plans on special cases of DP-resolution which lead to "reductions". More...

Go to the source code of this file.

Detailed Description

Plans on special cases of DP-resolution which lead to "reductions".

Singular DP-reduction
  • 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 clause-set, and the reduction happens in-place.
    1. Perhaps then we better create a new-function.
    2. Perhaps we have a general naming scheme for distinguishing between in-place 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 fine-grained versions which check for the various conditions interesting here:
    1. Degeneration (at least one clause gets lost).
    2. Clauses are as full as possible.
  • Compare "Decision algorithms" in Satisfiability/Lisp/MinimalUnsatisfiability/plans/DeficiencyOne.hpp.

Definition in file DP-Reductions.hpp.