GeneralisedUCP.hpp File Reference

Plans for Maxima-components regarding r_k-reductions. More...

Go to the source code of this file.

Detailed Description

Plans for Maxima-components regarding r_k-reductions.

Update names
  • All names need to be changed, reflecting their (main) argument types.

    todo 1519.

    • Instead of generalised_ucp(F,1) the more efficient ucp_0_cs (or ucp_cs_1 etc.) should be used where possible.
    • Except of the most basic implementations.
    • Perhaps we should allow alternative implementations of r_1 as additional parameters; or we should use a special variable (which can be dynamically altered).
    Strengthen the tests
    • We need more systematic coverage (with small clause-sets).
    • We should also employ some form of data-tables so that the tests mainly run through these tables.
    • And we should strengthen re-use of sub-tests between the various (rather similar) test-functions.
    Use oracles
    • Implement the generalisations of r_k using oracles S for satisfiability and U for unsatisfiability (see [Investigating a general hierarchy of polynomially decidable classes of {CNF}'s based on short tree-like resolution proofs; Kullmann, 1999, ECCC], and [Upper and Lower Bounds on the Complexity of Generalised Resolution and Generalised Constraint Satisfaction Problems; Kullmann, 2004, AMAI].
    • Perhaps two variations: Early detection of oracle-applicability, and late detection (at the leaves).
    • For additional oracle-examples see ComputerAlgebra/Satisfiability/Lisp/Backdoors/plans/general.hpp.
    • Likely the combination with autarky-search needs more thought.
    • 2-CNF for U and S can at most increase k by 2, but is easy to achieve.
    • Renamable Horn is only interesting for S.
    • An extension is given by linearly satisfiable clause-sets.
    • Another class contained in the class of linearly satisfiable clause-sets is given by matching satisfiable clause-sets.
    • All the above classes are stable under application of forced partial assignments, and likely we should only consider such classes. For d >= 1, the class of satisfiable clause-sets of maximal deficiency d (as well as the class of unsatisfiable clause-sets of maximal deficiency d) seems not to be stable (examples ???), and thus perhaps should be excluded from consideration.

Definition in file GeneralisedUCP.hpp.