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.

  • $\begingroup$ Can you provide a self-contained definition of a Dual Horn formula? $\endgroup$ – D.W. May 7 '18 at 18:44
  • $\begingroup$ 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. $\endgroup$ – D.W. May 8 '18 at 6:35

Since Horn and Dual Horn are analogous, yet opposite, your definition of minimal for Horn would be the negation of the Dual Horn definition. Said another way, if you negate the definition of minimal DualHorn, by your thinking, there is only 1 minimal solution.

Although, I'm not following the logic entirely.

There are papers on counting solutions to Horn or Dual Horn and it had been shown (proven?) to be NP.

  • 1
    $\begingroup$ I don't think see how this answers the question. Minimal solutions for a Dual Horn formula would correspond to maximal solutions for the corresponding Horn formula. I don't understand how "if you negate the definition of minimal DualHorn, there is only 1 minimal solution" is relevant or useful here. If you change the question, we can answer the changed question, but that doesn't answer the original question. $\endgroup$ – D.W. Aug 23 '18 at 7:24
  • $\begingroup$ I misinterpreted what I read. Thanks for the clarification $\endgroup$ – knightgambit Aug 24 '18 at 23:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.