Bidual Horn functions and extensions ?
Partially defined Boolean functions (pdBf) (T,F), where T,F?{0,1}n are disjoint sets of true and false vectors, generalize total Boolean functions by allowing that the function values on some input vectors are unknown. The main issue with pdBfs is the extension problem, which is deciding, given a pdBf, whether it is interpolated by a function f from a given class of total Boolean functions, and computing a formula for f. In this paper, we consider extensions of bidual Horn functions, which are the Boolean functions f such that both f and its dual function fd are Horn. They are intuitively appealing for considering extensions because they give a symmetric role to positive and negative information (i.e., true and false vectors) of a pdBf, which is not possible with arbitrary Horn functions. Bidual Horn functions turn out to constitute an intermediate class between positive and Horn functions which retains several benign properties of positive functions. Besides the extension problem, we study recognition of bidual Horn functions from Boolean formulas and properties of normal form expressions. We show that finding a bidual Horn extension and checking biduality of a Horn DNF is feasible in polynomial time, and that the latter is intractable from arbitrary formulas. We also give characterizations of shortest DNF expressions of a bidual Horn function f and show how to compute such an expression from a Horn DNF for f in polynomial time; for arbitrary Horn functions, this is NP-hard. Furthermore, we show that a polynomial total algorithm for dualizing a bidual Horn function exists if and only if there is such an algorithm for dualizing a positive function.
partially defined boolean functions boolean functions horn formulas satisfiability characteristic models polynomial algorithms