Plans for algorithms handling problems of bounded deficiency (or, better, for algorithms guided by the maximaldeficiencyparameter)
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 maximaldeficiencyparameter)
 Todo:
 Overview on fundamental tasks

Deciding SAT for (boolean and nonboolean) clausesets via backtracking (bounded by deficiency) as given by [Szeider] and [Kullmann 2009].

Finding a maximal autarky for (boolean and nonboolean) clausesets 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 clausesets can be computed by max_deficiency_fcs in ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Hypergraphs.mac; we need also the computation for nonboolean clausesets.
Definition in file general.hpp.