OKlibrary  0.2.1.6
general.hpp File Reference

Plans for algorithms handling problems of bounded deficiency (or, better, for algorithms guided by the maximal-deficiency-parameter) More...

Go to the source code of this file.


Detailed Description

Plans for algorithms handling problems of bounded deficiency (or, better, for algorithms guided by the maximal-deficiency-parameter)

Todo:
Overview on fundamental tasks
  • Deciding SAT for (boolean and non-boolean) clause-sets via backtracking (bounded by deficiency) as given by [Szeider] and [Kullmann 2009].
  • Finding a maximal autarky for (boolean and non-boolean) clause-sets via search through partial assignments (bounded by deficiency) as given by [Kullmann 2009].
  • Using the matroid approach as in [Kullmann 2000].
  • Discuss the relations to module Satisfiability/Lisp/MinimalUnsatisfiability.
  • Discuss the relations to module Satisfiability/Lisp/Autarkies.
  • The deficiency for boolean clause-sets can be computed by max_deficiency_fcs in ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Hypergraphs.mac; we need also the computation for non-boolean clause-sets.

Definition in file general.hpp.