Generating Models of a Matched Formula With a Polynomial Delay
(Extended Abstract)?
Abstract
A matched formula is a CNF formula whose incidence graph admits a matching which matches a
distinct variable to every clause. Such a formula
is always satisfiable. Matched formulas are used,
for example, in the area of parameterized complexity. We prove that the problem of counting the
number of the models (satisfying assignments) of
a matched formula is #P-complete. On the other
hand, we define a class of formulas generalizing
the matched formulas and prove that for a formula
in this class one can choose in polynomial time a
variable suitable for splitting the tree for the search
of the models of the formula. As a consequence,
the models of a formula from this class, in particular of any matched formula, can be generated sequentially with a delay polynomial in the size of the
input. On the other hand, we prove that this task
cannot be performed efficiently for linearly satisfi-
able formulas, which is a generalization of matched
formulas containing the class considered above