MatchingAutarkies.hpp File Reference

Plans for Maxima-components regarding matching autarkies. More...

Go to the source code of this file.

Detailed Description

Plans for Maxima-components regarding matching autarkies.

Connections to other modules
Matching satisfiability
  • Deciding matching satisfiability of F likely happens most efficiently by the criterion delta^*(F) = 0.
  • A matching satisfying assignment can then be simple read off a maximum matching in the clause-variable graph.
Deciding matching leanness
  • Using the definition (no matching autarky exists).
  • Using the surplus.
    Using the criterion, that every strict subset has a smaller deficiency.
Finding matching autarkies
  • DONE Simple enumeration.
Computing the matching-lean kernel
  • DONE Implement brute-force search.
  • Apply the general procedure (see "Lean kernel via oracle for leanness-decision" in ComputerAlgebra/Satisfiability/Lisp/Autarkies/plans/LeanKernel.hpp), based on deciding matching leanness.
  • Can the characterisation of the matching-lean kernel as the smallest tight sub-clause-set be exploited (using matching techniques)?
Computing a quasi-maximal matching autarky
  • This is a matching autarky yielding the matching-lean kernel.
  • It can be obtained by iteratively computing some non-trivial matching autarky until none exists anymore, and then taking the composition.
  • Alternatively one first computes the matching-lean kernel, crosses the variables in it out and removes the arising empty clause, and computes a matching-satisfying assignment for the resulting clause-set.
  • Compute the surplus.
  • Implement the related strengthening of matching autarkies (see [Kullmann, CSR 12-2007], Lemma 4.32).
  • Implement the reduction r from Corollary 4.31 in [Kullmann, CSR 12-2007].
  • Implement the reduction S from Lemma 4.33 in [Kullmann, CSR 12-2007].

Definition in file MatchingAutarkies.hpp.