Decision versions of optimization problems: cardinality constraint (lower bound) as a CNF Horn formula for Maximum Matching

TL;DR

This paper introduces a polynomial-time satisfiability formula for the decision version of the maximum matching problem with a cardinality constraint, enabling new solution approaches for such optimization problems.

Contribution

It presents the first polynomially solvable satisfiability expression for the decision version of maximum matching with a cardinality constraint, opening new avenues for solving optimization problems.

Findings

Provides a CNF Horn formula for the lower bound in maximum matching

Enables polynomial-time solutions for the decision problem

Introduces a novel approach to optimization problems via satisfiability

Abstract

We provide a formula for the lower bound in the form of $|F| \ge K$, in such a way that the decision version of unweighted non-bipartite matching can be solved in polynomial time. ~The parameter $K$ can vary from instance to instance. We assume that the domains, the set of vertices and the set of edges, are ordered. To our knowledge, no polynomially solvable satisfiability expression has been developed for this problem so far, or for that matter, for any decision problem derived from optimization. Hence for such problems, this opens up a new approach to solving them.