# Counting (enumerating) minimal solutions of a dual horn formula

Is there an efficient algorithm ("does not necessarily have to be a polynomial time algorithm") to compute all "minimal" solutions for a Dual Horn formula (conjunction of clauses where each clause contains at most one negated literal)? By "minimal" I mean, consider the following dual horn clause (formula)-: $x_1 \lor x_2$. While the solutions are $(1,0), (0,1), (1,1)$, we do not consider $(1,1)$ to be minimal since negating any bit in $(1,1)$ will also yield a feasible assignment. More generally, by a minimal solution I mean given a solution $S$, let $X$ be the subset of variables in $S$ that have been set to true, then if there exists a proper subset in $X$ which alone when set to true also satisfies the original dual horn formula, then $S$ is not minimal.

Further, it would be great if someone can point me to literature on the same.

Here are my thoughts on the problem, and admittedly not thoroughly thought true. I understand that since Horn SAT has a linear time algorithm for finding a feasible assignment, Dual Horn also must have such an algorithm analogously. However, Dual Horn can have more than 1 mimimal solution as shown in my example above whereas Horn has a single minimal solution.

On the problem of enumerating all minimal solutions, if in case the linear time algorithm is able to output at least one minimal solution, then an obvious way to enumerate other mimimal solutions would be to add another clause cutting off the previous solution. However this I suspect is likely to break the dual horn structure in the formula and also it is obviously inefficient to do so. Hence, I think there could be a better algorithm to enumerate them. An alternative algorithm may be to do a branch approach, where after a solution has been computed we branch on one of the variables and repeat the linear time algorithm, however now we may have preserved the dual structure in the formula.

As D.W pointed out below there can be exponential number of solutions. However I suspect there could be a way to enumerate all minimal solutions in the dual HORN formula based on some notion of the structure(relationship between variables and clauses). I am most interested in knowing if there exists an algorithm that exploits the structure in the problem for enumeration. By "EFFICIENT" this what I mean.

• Can you provide a self-contained definition of a Dual Horn formula? – D.W. May 7 '18 at 18:44
• I don't understand what you mean by "enumerate .. based on some notion of the structure". Are you perhaps looking for an implicit/compressed representation of the list of all minimal solutions? If so, what properties do you want that representation to have? What do you want to be able to do with it? Note that the formula is itself a compressed representation, but probably not one that is useful for your purposes -- so to find something more suitable, we'll need to know what your purposes are. – D.W. May 8 '18 at 6:35