Cost-Optimal Decision Diagrams for Stochastic Boolean Function Evaluation
January 01, 1970
Abstract
In many decision-making scenarios, acquiring information incurs different costs. We consider the problem of constructing a deterministic evaluation strategy that minimizes the expected cost of evaluating a propositional formula under variable costs and a probability distribution over truth assignments. We present a branch-and-bound algorithm with variable-selection heuristics, pruning, and caching. To the best of our knowledge, it is the first practical exact algorithm for this level of generality. Experiments on random instances demonstrate scalability and quantify the efficiency–quality trade-off of a greedy beam-search variant. We additionally evaluate a structured heart-disease diagnosis instance. Finally, we prove that the problem is \(\ComplexityFont{\#P}\)-hard and contained in \(\PSPACE\).
1 Introduction↩︎
Evaluating a Boolean formula becomes non-trivial when observing its variables incurs different costs, especially when the variables are statistically dependent. This scenario is typical in applications such as diagnosis, testing and classification [1]–[3]. This problem is known as the Stochastic Boolean Function Evaluation (SBFE) problem, and in the sequential testing literature [1] sequential testing of Boolean functions.
Exhaustive brute-force methods have been proposed for some classes of formulas [4], [5]. More recent works focus on worst-case complexity and approximation algorithms [6], sometimes in special cases such as symmetric functions [7], or using costs but no probabilities or assuming uniform probabilities for all variables [8], [9]. Polynomial-time cases with restricted Boolean functions such as \(k\)-out-of-\(n\) [10], [11] or disjunctions (analogously conjunctions) of atoms [12] have been considered for sequential testing.
The SBFE problem is related to various decision-tree problems [13]–[15]. Each node of a decision tree represents a test (possibly with an associated cost), the result of which determines which sub-tree to follow, and leaf nodes contain a value (such as a class or diagnosis) to which the sequence of test results from the root node is mapped.
Probabilities may be associated with the classes or the test outcomes in different ways. The tests and their relation to the diagnoses or the test results may be expressible as a mapping or a formula.
While there is a continuing interest in analytical works on tractable approximations and special cases, there has been little focus on scalable optimal methods for the SBFE problem in the most general setting with general Boolean functions and complex probability distributions on the variables. This is the gap our work helps to fill by proposing and evaluating a practical algorithm that incorporates heuristics and effective pruning methods to improve scalability.
We address the off-line SBFE problem, with the objective of constructing decision diagrams to evaluate Boolean formulas such that the expected cost of evaluation is minimal. The diagram represents a general procedure that can be used multiple times with different variable values, as long as the costs and the statistical dependencies between the variable values remain the same.
Concretely, we consider a general problem of optimal decision diagram construction, starting from an arbitrary propositional formula \(\phi\). The value of each variable in \(\phi\) can be observed, incurring a cost, and the conditional probability of a variable being true, given some subset of others, is known. We want to minimize the expected cost of determining the truth-value of \(\phi\). Additionally, in contrast to much of the earlier work that has imposed restrictions on cost functions or probability distributions, we permit arbitrary positive costs and general probability distributions that can, for example, be represented by Bayesian networks.
Our contributions are as follows. First, we propose a practical branch-and-bound algorithm for constructing optimal decision diagrams, including various variable ordering heuristics and efficient pruning and caching schemes. We present an implementation of our algorithm and evaluate its runtime performance. We empirically show the efficiency improvements from pruning, caching and variable ordering heuristics, and show performance variation across different clause-to-variable ratios, specifically a region around which instances are particularly hard. We also investigate the trade-off between runtime and quality when using a beam search instead of optimal search. Finally, we present novel complexity results for constructing optimal decision diagrams for arbitrary Boolean formulas, showing the problem to be \(\ComplexityFont{\#P}\)-hard. NP-hardness of various SBFE variants has been stated in the literature [16]–[18], but stricter lower bounds have not been reported for the SBFE problem or the equivalent sequential testing problem [2].
We review the related literature in more detail in Section 2. The problem is formally defined in Section 3, and its complexity is analyzed in Section 4. We present our algorithm in Section 5 and empirically evaluate its implementation in Section 6.
2 Related Work↩︎
A number of works in the literature consider the evaluation of a Boolean condition or a classifier, in some cases with a decision diagram or tree as a result.
2.0.0.1 Binary Decision Diagrams
Evaluation of Boolean functions can be described with different types of Binary Decision Diagrams, including Free BDDs (FBDD), which allow different variable orderings on different paths through the diagram. Methods for finding FBDDs of minimal size have been developed [19]. This is a restricted setting compared to ours: FBDD variables have no costs or probabilities for different value assignments, and the objective is to minimize size rather than the cost of using variables.
2.0.0.2 Object identification problems
The objective is to identify the class a given object belongs to, by performing a sequence of tests, each of which corresponds to a subset of objects, with the outcome being whether the object belongs to that subset [13], [14]. All possible test sequences are represented as a decision tree. Probabilities, if used at all, are assigned to classes only, not to tests. Hyafil and Rivest show that checking the existence of a decision tree of a given size is -complete. Later works are analytical and focus on approximation algorithms with logarithmic approximation ratios [20]–[22].
This problem is simpler than the one in our work due to the restricted probabilities and propositional language. The case with only two classes is a special case of our problem. The problem studied in our work can be generalized to multi-class classification, for example via vectors of Boolean formulas.
2.0.0.3 Binary classification with Boolean formulas
Using decision trees to determine the value of a Boolean formula, similarly to the present work, has been considered in the literature. Reinwald and Soland construct decision trees with the least expected cost for decision tables, which are essentially Boolean functions in disjunctive normal form, with a probability associated to each disjunct. Breitbart and Reiter present an algorithm for finding a decision tree with the minimum average number of observations to determine the value of a monotonic Boolean function, with unit costs for every observation, and uniform probability for every valuation. The treatment of probabilities here is far less general than in our work, and the algorithm for finding optimal decision trees is brute-force without heuristics or pruning methods. Many works on circuit complexity consider the depth of circuit diagrams for evaluating Boolean functions [23], without separately considering costs or associating probabilities with different value combinations. Approximation algorithms for the SBFE problem have been investigated [6], [7].
2.0.0.4 Decision trees in Machine Learning
Decision trees have been used for representing large datasets more compactly, to make the data more explainable, and to turn it into an effective classification procedure [15], [24]–[26]. Costs are sometimes considered, for example in algorithms that attempt to minimize the cost of misclassifying instances, sometimes together with the cost of reading the variable values [27], [28]. The machine learning problem is fundamentally different: learning (an approximation of) some decision function, in contrast to the SBFE problem which aims to devise a general strategy of most cheaply evaluating the decision according to a given decision function. This optimality in evaluation is not considered nor solved by learning a classification function.
3 Problem Statement↩︎
We briefly recall the basics of propositional logic. Let \(X = \{ x_1,\ldots,x_n\}\) be a set of propositional variables. Formulas are formed from variables in \(X\) and connectives \(\vee\), \(\wedge\) and \(\neg\). A valuation \(v : X\rightarrow\{0,1\}\) is a total function \(X\) to values 0 (false) and 1 (true), and it determines the truth of formulas \(\phi\), indicated by \(v\models\phi\), as follows. For atomic formulas \(x\in X\), \(v\models x\) if and only if \(v(x) = 1\). For compound formulas, \(v\models\phi_1\wedge\phi_2\) iff \(v\models\phi_1\) and \(v\models\phi_2\), \(v\models\phi_1\vee\phi_2\) iff \(v\models\phi_1\) or \(v\models\phi_2\), and \(v\models\neg\phi\) iff \(v\models\phi\) does not hold. A formula \(\phi\) is satisfiable if \(v\models\phi\) for at least one valuation \(v\). It is valid if \(v\models\phi\) for all valuations \(v\).
Consider a formula \(\phi\) with Boolean variables in \(X = \{ x_1,\ldots,x_n\}\), and the problem of determining whether \(\phi\) is true or false. Each variable \(x\in X\) can be observed at some positive rational cost \(c(x)\), \(c: X\rightarrow{\mathbb{Q}}\). Further, the probability model provides \(P(v(x)=b \mid B)\) for each variable \(x\in X\), value \(b\in\{0,1\}\), and partial valuation \(B\) over variables in \(X\backslash\{x\}\) reached during evaluation. These conditionals are induced by a joint distribution over \(X\).
Definition 1 (Problem instance). Our problem instance is \(I=(\phi,X,P,C)\), with
a Boolean formula \(\phi\) over a set of variables \(X\); a conditional probability distribution \(P\) on \(X\); and a cost function \(c: X\rightarrow{\mathbb{Q}}\) of observing variables.
The aim is to construct a minimal cost decision diagram that unambiguously determines the value of \(\phi\). Intuitively, given a Boolean formula \(\phi\) over variables \(X\), we say that \(G_{\phi}\) is a decision diagram for \(\phi\) if it is a decision diagram with non-leaf nodes labeled with variables in \(X\) and arcs with a value for the corresponding variable, and the following conditions hold. Each possible valuation is represented by exactly one path in the diagram.
Formally, we require the following.
Definition 2 (Decision diagram for a formula). Given an instance \(I=(\phi,X,P,C)\), a decision diagram for \(\phi\)* is a directed acyclic graph \(G = \langle N,A\rangle\) with \(N\) a finite set of nodes and \(A\subseteq N\times N\) a set of arcs, where*
\(O : N\rightarrow X\cup\{ \top, \bot\}\) assigns to each node a variable, the symbol \(\top\) (for true), or \(\bot\) (for false), with
\(O(n)\in\{\top,\bot\}\) only if \(n\) has no outgoing arcs,
\(O(n)\in X\) only if \(n\) has two outgoing arcs, and
\(V : A\rightarrow\{0,1\}\) indicates whether the arc is followed when the value of the observed variable is false* or true,*
for every node \(n\) such that \(O(n)\in X\), there is exactly one outgoing arc \(a\) labeled \(V(a)=0\) and exactly one outgoing arc \(a'\) labeled \(V(a')=1\),
there is a root node \(r\in N\) such that no arc ends in \(r\),
every node in \(N\backslash\{r\}\) has at least one incoming arc.
Consider a path starting from the root of \(G\), \(\mathit{s}=(a_1,\dots,a_m)\) where each \(a_i\in A\). Let \((n_1,\dots,n_m)\) be the sequence of nodes, not including \(\top\) or \(\bot\), appearing in the arcs of \(\mathit{s}\). We define \(\pi_{\mathit{s}}\), the valuation function corresponding to \(\mathit{s}\), as \(\pi_{\mathit{s}}(O(n_i))=V(a_i)\) for all \(1\leq i \leq m\).
\(G\) is a decision diagram for \(\phi\) (denoted \(G_{\phi}\)) if moreover 1) for all paths \(\mathit{s}\) of \(G_{\phi}\), if \(\mathit{s}\) ends in \(\top\), then \(\phi\) is valid under the valuation \(\pi_{\mathit{s}}\), and if \(\mathit{s}\) ends in \(\bot\), then \(\phi\) is unsatisfiable under \(\mathit{s}\); and 2) for each total valuation \(\pi\)over \(X\), there is a path \(\mathit{s}\) in \(G_{\phi}\) such that \(\pi_{\mathit{s}}\) can be extended to \(\pi\).
In words, a decision diagram for a formula \(\phi\) classifies any valuation as \(\top\) (\(\bot\)) iff \(\phi\) is true (false) under (all extensions to) that valuation. A decision tree is a special case of a decision diagram, where each node has at most one incoming arc.
We move on to defining the (evaluation) cost and thereby the optimality of decision diagrams for formulas. Let \(\mathcal{P}(G_{\phi})\) denote the collection of paths with non-zero length starting from the root in a decision diagram \(G_{\phi}\). For brevity, for path \(\mathit{s}\), let \(\pi_{\mathit{s}}^j\) denote \(\pi_{\mathit{s}}\) restricted to the first \(j\) valuations in the path, i.e. if the nodes corresponding to \(\mathit{s}\) are \((n_1^s,\dots,n_m^s)\), let \(N'=\{n_i^s\in N\mid 1\leq i\leq j\}\) and \(\pi_{\mathit{s}}^j=\pi_{\mathit{s}}|_{N'}\). Further, let \(\pi_{\mathit{s}}(j)\) denote the \(j\)th valuation in \(\mathit{s}\), i.e. \(O(n_i)=\pi_{\mathit{s}}(O(n_i))\).
Definition 3 (Optimal decision diagram for \(\phi\)). Given an instance \(I=(\phi,X,P,C)\)and a decision diagram for \(\phi\), \(G_{\phi}\), the expected (evaluation) cost of \(G_{\phi}\) is \[\begin{align} c(r)+ \sum_{\mathit{s}\in\mathcal{P}(G_{\phi})} \left( c(n^{\mathit{s}}_{|\mathit{s}|}) \cdot \prod_{j=1}^{|\mathit{s}|} P(\pi_{\mathit{s}}(j)\mid \pi_{\mathit{s}}^{j-1})\right). \end{align}\] The product of conditional probabilities is the probability, under the joint distribution, of reaching the corresponding path. A decision diagram for \(\phi\) is optimal if it has the minimal cost of all decision diagrams for \(\phi\).
In words, for each path with length greater than \(0\), the cost of observing the final variable in the path is multiplied by the probability of this particular valuation, and the cost of the whole tree is the cost of observing the root variable plus the sum of all paths. The cost is the expected cost of determining the truth value of \(\phi\) by a sequence of variable observations.
Example 1. Consider the instance \(I=(\phi,X,P,C)\) with \(\phi=(A\vee B\vee C)\wedge(\neg A\vee D)\), \(c(A)=c(B)=c(D)=1\) and \(c(C)=10\), and uniform probabilities, i.e. each variable is true with a probability of 0.5. Figure 1 shows two decision diagrams for \(I\) as trees; it is easy to see that they both correctly classify all valuations to \(\phi\).
The graph on the left has a cost of \(1 + 1\cdot 0.5 + 1\cdot 0.5 + 10\cdot 0.5^2 = 4.5\). The sum terms correspond to the costs of the variables \(A\), \(D\), \(B\), and \(C\) respectively, multiplied by the probability of the evaluation reaching their respective node. The graph on the right has a cost of \(1 + 1\cdot 0.5 + 10 \cdot 0.5 + 1 \cdot 0.5^2 = 6.75\),
reflecting the fact that the costly \(C\) is evaluated before \(B\) in the right-hand branch.
4 Complexity↩︎
Interestingly, the complexity of the SBFE problem and related problems has not been analyzed beyond showing NP-hardness.
With dependencies between the variables and the need to minimize the expected cost of formula evaluation, the complexity increases substantially beyond NP. We address this gap in the literature.
We show that constructing a decision diagram with minimal expected cost is -hard, i.e. as hard as many probabilistic inference problems and model-counting problems for propositional logic [29], [30]. This shows, for example, that a reduction to Mixed Integer-Linear Programming, an NP-complete problem, is not feasible (under common assumptions such as NP\(\subset\)).
Theorem 1. The problem of calculating the expected cost of the least expected cost decision diagram is -hard.
Proof. We reduce \(\#\)SAT to calculating the cost of the optimal decision diagram. Let \(\phi\) be any propositional formula, and let \(X\) be the set of atomic propositions in \(\phi\), with \(n = |X|\). We construct a formula \(\phi'\) and a distribution \(D\) so that \(\phi\) has \(N\) models if and only if the expected cost \(c\) of the optimal decision diagram for \(\phi'\) with data \(D\) satisfies \(N\leq c < N+1\).
Let \(\phi' = \phi\wedge z\), where \(z\not\in X\). Let \(c(z) = 2^n\) and \(c(x) = \frac{1}{2n}\) for all \(x\in X\). Let \(D\) be the uniform distribution, i.e., every valuation of \(X\) has probability \(2^{-n}\). Clearly, these distributions can be represented polynomially wrt \(|X|\) in many formalisms, including Bayesian networks.
In every root-to-leaf path of the decision diagram for \(\phi\wedge z\) and \(D\), some member of \(X\) is observed, and only after \(\phi\) has been determined to be true, the value of \(z\) is observed. Paths that correspond to valuations that make \(\phi\) false do not observe \(z\), and do not correspond to satisfying valuations of \(\phi\).
Consider a node in the decision diagram corresponding to a partial valuation that assigns truth values to variables \(x_1,\ldots,x_k\), and which observes \(z\). This node corresponds to \(2^{n-k}\) satisfying valuations of \(\phi\). The observation of \(z\) contributes expected value \(2^{-k}\cdot 2^n = 2^{n-k}\) to the expected cost of the optimal decision diagram. Thus the sum of the contributions of the observations of \(z\) in all nodes of the optimal decision diagram equals the number of satisfying valuations \(N\) of \(\phi\). Additionally, the graph contains at most \(2^n\) observations for variables in \(X\), with a total maximum cost of \(n\cdot \frac{1}{2n} = 0.5\) on any execution of the decision diagram. Hence, the expected cost \(c\) of the optimal decision diagram satisfies \(N\leq c \leq N+0.5\). ◻
Note that model counting is -hard even with monotone formulas [30], and as our proof preserves monotony, constructing optimal decision diagrams for monotone formulas is also -hard. While a -membership does not seem likely, we can show that computing the expected cost of the decision diagram is in , and determining whether the expected cost is within given bounds is in . is very close to , as \(\PH\subseteq \cP^{\ComplexityFont{\#P}}\subseteq \PSPACE\) [31], so only a small gap remains in the complexity results.
Theorem 2. The problem of calculating the expected cost of the optimal decision diagram is in , and the problem of deciding if there is a decision diagram with an expected cost bounded by some constant is in .
Proof. Consider our Algorithm [alg:main] in Section 5. The procedure call OptCost(\(\phi,\emptyset,0,\infty,1.0)\) returns the expected cost of the decision diagram with the lowest expected cost. At each recursive call to OptCost, the number of occurrences of variables in \(X\) in the formula \(\phi\) is decreased by at least one. Hence, the recursion depth of OptCost is linear in \(|X|\).
For the representations of the statistical data we consider, the computation of expected cost on lines [li:cost2] and [li:cost3] takes polynomial space, as the probabilistic inference problem for Bayesian networks is solvable in . Hence, the memory consumption at any point of the search graph is polynomial, ignoring caching (which is not needed for the correctness or completeness of the algorithm.) This shows the membership for the function problem as well as the membership for the decision problem. ◻
5 Algorithm for Optimal Decision Diagrams↩︎
We present Algorithm [alg:main] for finding a decision diagram of minimum expected cost for an instance \(I=(\phi,X,P,C)\). We employ a bounding method (lines [li:prune1], [li:prune2], and [li:prune3]) and caching of exact subproblem solutions (lines [li:cache95check] and [li:cache95add]). Both result in substantial pruning of the search tree. The advanced lower-bound cache is given in Appendix 9. The pseudocode computes only the optimal cost; simple book-keeping can be added to construct the optimal decision diagram.
The algorithm proceeds by iteratively choosing a variable \(x\) to observe, and then constructing sub-graphs for the simpler problems when the value of \(x\) has been respectively fixed to \(0\) and \(1\) (or false and true). The recursion ends when the formula is logically equivalent to either the constant \(\top\) or \(\bot\), producing a leaf node in the decision diagram. This can be checked by solving the propositional satisfiability problem.
A branch in the search graph can be pruned based on the cost of an optimal decision diagram for a subformula (so that this decision diagram was found earlier in the search in an alternative branch for the same subformula). We maintain a lower bound \(bound\) (initially \(\infty\)) and the cost of the thus-far constructed parts of the current decision diagram, in \(parentcost\). We prune those subgraphs of the current search node for which the sum of \(parentcost\)and the subdiagram cost exceeds \(bound\). The value of \(bound\) is the lowest expected cost partial decision diagram that can be compared to the current one under construction. Crucially, \(bound\)is only passed to further recursive calls and not returned, ensuring that we are essentially comparing the cost of a complete decision diagram for the subformula at the point in which \(bound\)is updated to the cost of an alternative decision diagram, still under construction, for the same subformula. Pruning is done only when the latter is higher than \(bound\).
The subprocedure assign(\(l,\phi\)), where \(l\) is a literal (\(x\) or \(\neg x\) for some \(x\in X\)), replaces occurrences of \(x\) by the constant \(\top\) (if \(l=x\)) or the constant \(\bot\) (if \(l=\neg x\)) and unit propagation-like simplifications are employed.1 We next provide an illustrative example.
\(p\cdot \text{Cache}[B]\)
\(0\)
\(childcost\gets \infty\)
\(C_x\gets p\cdot c(x)\)
continue
\(C_x\gets C_x+\) continue
\(C_x\gets C_x+\) continue
\(childcost\gets \min(childcost,C_x)\) \(bound\gets \min(bound, parentcost+childcost)\)
\(\text{Cache}[B] \gets childcost/p\) \(childcost\)
Example 2. Consider the formula \(F=(A\vee B\vee C)\wedge(\neg A\vee D)\), with a uniform distribution over valuations, and with cost 10 for observing \(C\) and cost 1 for other variables. Part of the search tree for finding a decision diagram for \(F\) is shown in Figure 2, including finding the first two decision diagrams. The search tree has variable nodes (with a diamond shape) with two subtrees corresponding to setting the variable true and false (with the false* subtree indicated by the dashed line), and formula nodes that indicate the formula simplified with the variable values on the path from the root to the node.*
From the search tree, each decision diagram can be obtained by starting from the root node, and for each formula node, eliminating the formula node and all of its subtrees except one, at the same time connecting the remaining subtree with the parent of the formula node. For example, the first decision diagram that would be found on a left-to-right traversal is the tree shown on the left in Figure 1, with expected cost 4.5.
In our tree-search algorithm, at the formula node \(B\vee C\) after traversing the subtree corresponding to \(B\) and before proceeding to the subtree corresponding to \(C\), we have the cost \(4.5\) as the bound to which we would be comparing any decision tree obtained by searching the subtree for \(C\). Now, when going down to the subtree for \(C\), the cost so far would be \(1 + 1\cdot 0.5 + 10 \cdot 0.5 = 6.5\), which exceeds the bound, indicating that any decision tree found by completing the search for the subtree \(C\) would have a cost of at least \(6.5\). Hence the search-tree can be pruned at that point, without having to go any deeper. Thus, 4.5 is the cost of the best decision tree found by observing the variable \(A\) first. The search proceeds from the root node by sequentially considering \(B,C\) and \(D\) as the first observation.
Note that line [li:prune3] might seem superfluous, as it does not actually prune the search tree. This is not the case. Its purpose is to prevent updating childcost and caching the value \(C_x\) for the current sub-graph when the lowest-cost evaluation of assign(\(x=\bot\),\(\phi\)) was never found due to pruning inside the preceding recursive call to OptCost (counterexample can be found in the Appendix).
Algorithm [alg:main] caches the normalized optimal cost of each solved subproblem (line [li:cache95add]), so that the cost can be rescaled by the path probability when the same valuation state is reached again (line [li:cache95check]). Appendix 9 gives the complete version with lower-bound caching for pruned searches.
The selection order of variables also impacts effectiveness. We would like to find the most promising, low-cost decision diagrams first, so that other branches can be pruned quickly. Similarly, we would like to first traverse the more promising branch, for true or false, instead of trying them in fixed order. We detail a number of ordering heuristics below.
Pruning could be further strengthened. Our algorithm only considers the parentcost, the cost of the current variable \(c(x)\), and the cost of the first sub-tree with \(x\) assigned true or false (lines [li:prune1], [li:prune2] and [li:prune3]). Lower bounds on the cost of the untraversed subtrees (corresponding to the formulas \(\mathit{assign}(x,\phi)\) and \(\mathit{assign}(\neg x,\phi)\)) could be used to strengthen the pruning. Doing this efficiently is not trivial, however. One could, e.g., append to \(bound\)a cost corresponding to the cheapest variable occurring in one of the truth value branches. However, this could overestimate the lower bound, since \(\mathit{assign}(x,\phi)\) could already be unsatisfiable or valid; a full satisfiability check on \(\mathit{assign}(x,\phi)\) might be required for a correct bound. We leave the investigation of stronger bounds to future work.
5.1 Heuristics for Search Order↩︎
We propose heuristics for choosing the order of evaluating variables (see line [li:variteration] of Algorithm [alg:main]).
It is preferable to first find lower cost subsolutions so that pruning is done earlier, reducing the amount of searching. To select the next variable for branching, the algorithm considers variables that appear in the current formula and scores them using a heuristic function \(\mathrm{\small Score}\). The evaluation is based on the cost of observing a given variable as well as properties of the subformulas resulting from assigning that variable either true or false.
We assume input formulas to be in CNF. Recall that \(c(x)\) gives the cost of observing variable \(x\in X\), while \(P(x)\) represents the prior probability that \(x\) evaluates to true. For each candidate variable \(x\), the score is computed as: \[\begin{align} \mathrm{\small Score}(x) & =\;\mathrm{\small VScore}(x) \\ & + P(x \mid B) \cdot \mathrm{\small BranchScore}(\phi_x, h) \\ & + P(\lnot x \mid B) \cdot \mathrm{\small BranchScore}(\phi_{\lnot x}, h) \end{align}\] Here, \(\phi_x\) and \(\phi_{\lnot x}\) denote the CNF formulas after simplifying \(\phi\) under valuations \(v(x) = \top\) and \(v(x) = \bot\) respectively, and \(B\) is the current partial valuation. The variable with the lowest score is selected. The score uses both the direct cost of observing a given variable (via VScore) and the estimated cost of the subsequent subproblems (via BranchScore).
We use \(c(x)\) for VScore, and propose three heuristics to compute \(\mathrm{\small BranchScore}(\phi, h)\). The definitions of each heuristic are given in Table 1.
Intuitively, h_cost selects the lowest cost variable regardless of the rest of the formula, h_varCount eliminates as many variables as possible from the formula, and h_totalCost balances the immediate, certain cost
of observing \(x\) with a (rough) estimate of the cost of observing the rest of the variables.
For h_totalCost, \(\mathrm{\small VScore}\) is multiplied by a user-provided constant \(m\); 0.5 in our experiments. This is to balance between \(\mathrm{\small VScore}\) and \(\mathrm{\small BranchScore}\). The multiplier should be between 0 and 1, with a lower value weighting the certain observation cost \(\mathrm{\small VScore}\) over future, uncertain costs.
We also consider base, a baseline heuristic with arbitrary variable ordering.
We use \(\mathrm{\small Score}\) to also select the truth branch to evaluate first. Specifically, if \(P(x \mid B) \cdot \mathrm{\small BranchScore}(\phi_x, h) < P(\lnot x \mid B) \cdot \mathrm{\small BranchScore}(\phi_{\lnot x}, h)\), then the lines [li:cost2]–[li:prune2] are evaluated before lines [li:cost3]–[li:prune3].
| Name | ||
|---|---|---|
| base | \(0\) | \(0\) |
| h_cost | \(\cost(x)\) | \(0\) |
| h_varCount | \(\cost(x)\) | \(N\) |
| h_totalCost | \(\cost(x)\) | \(\multiplier\cdot \sum_{v \in \phi} \cost(v)\) |
5.2 Correctness of the Algorithm↩︎
We show that Algorithm [alg:main] identifies the optimal cost.
Theorem 3 (Correctness). The least-cost decision diagram for \(\phi\) has expected cost that equals the value returned by OptCost\((\phi,\emptyset,0,\infty,1.0)\) (Algorithm [alg:main]).
Proof. Consider the algorithm without pruning and caching, i.e. remove lines [li:prune1], [li:prune2] and [li:prune3] as well as line [li:cache95check]. Then the algorithm simply exhaustively searches over all decision diagrams where each leaf corresponds to an valuation under which \(\phi\) is either valid or unsatisfiable. In each stage, the cost of observing the variables occurring in the current valuation (discounted by its probability) is stored in variable \(parentcost\). The cost of the minimum cost decision diagram for the working formula \(\phi\) is collected in the variable \(childcost\). In the base case, i.e. when \(\phi\) is valid or unsatisfiable, a cost of 0 is incurred. In other nodes, the total cost comprises the probability of visiting this node given the current search path, \(p\), times the cost of observing the considered variable \(x\) (line [li:cost1]), plus the costs of the subtrees where \(x\) is true and false, respectively (lines [li:cost2] and [li:cost3]). In the main loop, the cost of the optimal decision diagram for \(\phi\) for each unobserved variable is compared, and the lowest is selected as \(childcost\) (line [li:update95mincost]); the optimal cost of determining the truth value of the working formula \(\phi\) is returned at the end.
Pruning preserves correctness. To see this, consider that \(bound\) is only updated after both true/false branches are evaluated in a depth-first manner (line [li:update95bound]) and it is only passed down in further recursive calls, not returned. Consider a call to OptCost in which \(bound\) is updated and let the working formula at this point be \(\phi_b\), and the \(parentcost\) and \(childcost\) at this point be \(parentcost_b\) and \(childcost_b\), respectively. We claim that the return value for this call is the same whether pruning happens or not; this implies the overall claim, since \(bound\)is updated at least after the first variable at the root is evaluated. To see this, note that \(childcost_b=bound-parentcost_b\) is the cost of the lowest cost decision diagram found for \(\phi_b\) so far (divided by \(p\), which is the same for all variables on this search node). Assume that sometime after selecting another variable \(x\) in the same loop, we prune on line [li:prune1], i.e. \(parentcost+C_x\geq bound\). Thus the cost for any decision diagram for \(\phi_b\) that would be found in the pruned branch is at least \(parentcost+C_x-parentcost_b\). Since line [li:prune1] prunes only when \(parentcost+C_x\geqbound\), this cost is at least \(bound-parentcost_b=childcost_b\).
Thus, any decision diagram that would be found after the pruning happened would not contribute to lowering \(childcost_b\) (at the recursive call to OptCost where \(bound\) was found) and therefore also not to lowering the final \(childcost\) at the root. Similar reasoning holds for pruning at lines [li:prune2] and [li:prune3].
Finally, exact caching does not affect correctness. Exact cache entries store only optimal subsolutions (line [li:cache95add]), so retrieving an exact entry (line [li:cache95check]) returns the normalized optimal cost multiplied by the probability of the current path. Therefore, caching can only avoid repeated work and cannot change the optimal cost returned by the root call. The advanced lower-bound caching version in Appendix 9 uses lower-bound entries only to prune, never as exact costs. ◻
6 Empirical Evaluation↩︎
We evaluate our approach in four ways. First, we show runtime and memory performance on hard instances. Next, we investigate how the structure of the underlying propositional formula affects runtime. We then examine the effect of relaxing optimality on runtime and solution quality with a beam-search version of our algorithm. Finally, we evaluate a structured real-world instance.
Our implementation of Algorithm [alg:main] (Python 3.9, python-sat v1.8 [32], CaDiCaL 1.9.5 [33]) was used for all experiments. Experiments were conducted on 2.5 GHz Intel Xeon
E5-2680 v3 CPUs with a 120-minute time limit and a 16 GB memory limit per instance.
We are not aware of a suitable benchmark set for SBFE and thus generated a set of random 3-SAT formulas [34] along with costs and probabilities. Random 3-SAT is parameterized by the number of variables \(N\) and clauses \(M\).
We drew variable observation costs uniformly at random from the integers \(1\) to \(10\). For simplicity, we drew independent probabilities for truth values uniformly at random.
Figure 3 presents results with respect to runtime (left) and peak memory usage (right) on datasets with \(6\)–\(15\) variables and a fixed
clause-to-variable ratio of \(1.5\) which generates hard instances, averaged over 100 instances per size. We evaluate the proposed heuristics and four baseline variants: suffixes _cache and
_noPruning denote enabled caching and disabled pruning, respectively, while base is pruning without caching. Lines are truncated at the first occurrence of a timeout. As expected, both runtime and memory usage grow exponentially
with problem size. Both pruning and caching yield exponential improvements over the baselines. Only cached variants successfully scale to 15 variables. The best performing methods are h_varCount_cache and h_totalCost_cache, with
an average runtime of 152 and 182 seconds, respectively, on instances with 15 variables, compared to 275, 325 and 518 seconds for the three other caching-enabled variants.
In contrast to the significant memory use shown for the cached variants, without caching, memory usage is minimal, and thus in memory-constrained settings, forgoing caching might be sensible.
We proceed to the impact of the clause-to-variable ratio (\(r\)) on problem difficulty. We show in Figure 4 the performance of the algorithm on instances with varying ratios for two different problem sizes (\(N=10\) and \(N=14\)). For both instance sizes, the average solving time peaks around a ratio of \(1.2\) to \(1.5\), well before the SAT phase transition point (\(\approx\)4.27). This is likely because in highly constrained instances there are lots of logical consequences and thus smaller trees, while less constrained instances are easily satisfiable, so setting a few variables suffices.
Thus, \(r=1.5\) is a near-worst-case (see above) and \(r=3\) an easier scenario (below).
Figure 5: Runtime (left) and expected cost (right) for exact versus beam search (\(k \in \{1,2,3\}\)) on hard (\(r=1.5\), top) and relaxed (\(r=3.0\), bottom) instances. OOMs and timeouts are shown for the exact algorithm only..
Finally, we compare greedy beam search (branching into only the best \(k\) variables at each search node) to our exact algorithm (Figure 5). For this comparison, the exact baseline is the best
variant from Figure 3, i.e. h_varCount_cache. In the harder instances with \(r=1.5\) (top), the exact algorithm exceeded resource limits when \(n>16\), whereas beam search solved all instances. At \(n=16\), beam search is more than an order of magnitude faster.
In terms of cost, beam with \(k=3\) remains within \(\approx 30\%\) of the optimal. On instances with \(r=3\) (bottom), the exact algorithm scales further to \(n=19\), with runtime and cost behaviour similar to that of beam search.
Interestingly, with higher clause-to-variable ratio, the optimal algorithm mostly runs out of memory rather than time, while the opposite is true with a lower ratio.
6.0.0.1 Illustrative medical-diagnosis case study
To illustrate how a learned classifier can be converted into a structured SBFE instance, we transform a medical-diagnosis classification tree into a stochastic Boolean function evaluation problem. We trained a decision tree [35] on the Cleveland Heart Disease dataset [36] to capture the diagnostic rules. We turned the rules into a Boolean formula as implications from the conditions of each path to the class at the leaf. Continuous features were discretized via threshold encoding, where consistency was enforced by generating implication constraints (e.g., \(\neg(f \le t_1) \lor (f \le t_2)\) for thresholds \(t_1 < t_2\)) to prevent impossible values. Each threshold predicate inherits the cost of its underlying medical test from Turney . We set each predicate probability to its empirical marginal frequency and evaluate both policies under the resulting independent product model, which is the probability model used by our algorithm. This process yielded a Boolean formula with 16 variables and 22 clauses. Under this common model, evaluating the original decision tree costs $236.4, while our algorithm identified the global optimum of $137.4 in 819 seconds, a 41.9% reduction in expected predicate-acquisition cost.
7 Conclusion↩︎
We have considered a setting in which a Boolean formula represents a condition for a decision, where observing variables incurs different costs and valuations follow a joint probability distribution. We have presented a branch-and-bound algorithm for finding a decision diagram of minimum expected cost in this setting. We have introduced pruning, caching, and variable-selection heuristics, and empirically demonstrated their effectiveness. We have shown that a greedy beam-search variant offers a controllable efficiency–quality trade-off. Finally, we have analyzed the computational complexity of decision-diagram construction, showing that it is \(\ComplexityFont{\#P}\)-hard and contained in \(\PSPACE\).
8 Pruning in the Algorithm Pseudo-Code↩︎
In the pseudo-code of our algorithm given in the main paper, we have three code lines like this one. \[\label{codeline} \mathbf{if} \mathit{ parentcost} + C_x\geq \mathit{bound}\;\mathbf{then}\;\mathbf{continue}\tag{1}\] The first two code lines obviously prune parts of the search tree, but the third one obviously does not. The purpose of the third code line is instead to prevent caching of values that do not represent the expected cost of the best decision diagram for a given formula. The next example illustrates what would happen without this code line.
Example 3. Consider a decision diagram construction problem in which at some stage the current formula is \[(Z\rightarrow Y)\wedge(\neg Z\rightarrow(X\vee Y))\] and a part of the search tree looks as in Figure 6.
We show how the algorithm without the pruning condition (1 ) can cache a cost for the formula \(X\vee Y\) that is not the lowest possible cost for a decision diagram for \(X\vee Y\).
The core issue is that caching makes it possible to avoid some prunings that would otherwise take place, and in some cases for some formulas, a non-optimal diagram does not get pruned, but the optimal diagram for that same formula will get pruned, and the non-optimal value gets stored in the cache.
Let all the variables be statistically independent and \(P(X)=P(Y)=0.5\).
For the problematic behavior to be possible in this example, the decision diagram for \(X\vee Y\) with root \(Y\) must have a lower cost than the diagram for \(X\vee Y\) with root \(X\). This will be the case when \[c(Y)+0.5c(X) < c(X)+0.5c(Y).\]
For the pruning to not happen for the diagram with root \(X\) and for it to happen for the diagram with root \(Y\), it must be that \[c(X) < \mathit{bound} \;\mathrm{ and }\; c(Y)+0.5c(X)>\mathit{bound}.\]
These hold, for example, when the costs and the effective bound at the relevant spot in the search tree are as follows. \[\begin{array}{rcl} c(X) & = & 1.2 \\ c(Y) & = & 1 \\ \mathit{bound} & = & 1.4 \end{array}\]
What happens in this example is the following.
At the first (leftmost) \(Y\) node, the cost of the diagram for formula \(Y\) is cached.
At the second formula \(Y\) node (marked in boldface), the cost of the subtree is fetched from the cache. The bound of the \(X\vee Y\) node is violated, but the cached value is used as if there had been no bound violation. For \(X\vee Y\) the diagram with root \(X\) is now the best one so far.
The search for the best diagram for \(X\vee Y\) proceeds to the sibling with \(Y\) as the root. The illustration shows the full diagram below that node, but the second sub-tree with \(Y=0\) will not be developed beyond the node with formula \(X\) due to a violation of the bound.
The issue now is that this sub-tree, with \(Y\) in the root, has a lower cost than the sub-tree with \(X\) in the root. But this sub-tree was pruned. Hence the sub-optimal value for \(X\vee Y\), which was found first, gets cached.
Later in the search, if/when a node with \(X\vee Y\) is encountered again, this sub-optimal cost for \(X\vee Y\) will be retrieved from the cache, which can lead to the algorithm delivering a decision diagram that is not optimal.
To prevent sub-optimal values from being cached, we discard any cost computation that may have depended on pruning an optimal sub-solution. We have chosen to use the third code line (1 ). Another possibility would be to check the bound when retrieving a value from the cache.
9 Full Algorithm with Advanced Caching↩︎
Algorithm [alg:advanced95cache] presents the complete advanced-caching implementation of our approach. While the simplified version in the main text only caches optimal subsolutions, this version incorporates an advanced mechanism to handle cases where the search is pruned (i.e., when \(childcost= \infty\)). Note that the optimality still holds in this version.
9.0.0.1 Lower Bound Caching
When the search for a specific assignment \(B\) is cut off because the cost exceeds the global bound \(bound\), we cannot store an exact cost. However, we have derived valid information: the cost of this subtree is at least the difference between the bound and the parent cost. In line [adv:cache95lb95store], we store this lower bound (normalized by probability \(p\)) along with a flag \(\mathrm{\small LB}\).
9.0.0.2 Reusing Lower Bounds
When this state \(B\) is revisited later with a potentially looser bound, we retrieve the cached lower bound (line [adv:cache95check]). Even though it is not an exact value, it allows us to perform an immediate consistency check. If the cached lower bound, when scaled by \(p\) and added to the current \(parentcost\), still exceeds the new \(bound\) (line [adv:cache95lb95check]), we can immediately prune the search (returning \(\infty\)). This effectively prevents redundant explorations of expensive subtrees even when their exact costs are unknown.
\((\hat{v}, \textit{flag}) \gets \text{Cache}[B]\) \(\hat{v} \cdot p\) \(\infty\)
\(0\)
\(childcost\gets \infty\)
\(C_x\gets p\cdot c(x)\)
continue
\(C_x\gets C_x+\) continue
\(C_x\gets C_x+\) continue
\(childcost\gets \min(childcost,C_x)\) \(bound\gets \min(bound, parentcost+childcost)\)
\(\text{Cache}[B] \gets ((bound- parentcost)/p, \mathrm{\small LB})\) \(\infty\) \(\text{Cache}[B] \gets (childcost/p, \mathrm{\small Exact})\) \(childcost\)
Further Details on Empirical Evaluation↩︎
10 Dataset Generation Details↩︎
All reported random-instance results average over 100 independently generated 3-SAT formulas. For scalability, \(N\) ranges from 6 to 15 at a fixed clause-to-variable ratio of 1.5. For the ratio study, \(N\in\{10,14\}\) and \(M/N\) ranges from 0.5 to 4.5 in increments of 0.1. Beam search uses the same instances as the scalability study and \(k\in\{1,2,3\}\). Observation costs are drawn uniformly from the integers 1 to 10, and truth probabilities are independently sampled from \([0,1]\) and rounded to two decimal digits.
11 Illustrative Medical-Diagnosis Case Study↩︎
11.1 Data and Proxy Model↩︎
We use the Cleveland Heart Disease data from the UCI Heart Disease collection [36]. The target num is binarized as \(\texttt{num}>0\), and missing feature values are imputed with the feature median. We train DecisionTreeClassifier(max_depth=4, random_state=42) on the resulting data to obtain a deterministic CART proxy. The
proxy has 15 split predicates. We add one zero-cost target variable representing the binary output, yielding 16 Boolean variables in total.
11.2 CNF Construction↩︎
Each CART root-to-leaf path is converted into one clause encoding that the conjunction of its path conditions implies the label predicted at its leaf. The depth-4 proxy produces 16 such leaf-path clauses. To enforce consistency among predicates derived from the same physical feature, we add six threshold-consistency clauses of the form \(\neg(f\le t_1)\lor(f\le t_2)\) for \(t_1<t_2\). The resulting formula has 22 clauses.
11.3 Probability and Cost Modeling↩︎
For each split predicate \(f\le t\), its probability is its empirical frequency in the cleaned data, clipped to \([0.001,0.999]\). The solver uses the product prior formed from these marginal probabilities. Each predicate inherits the Turney cost of its underlying physical feature , while the target variable has zero observation cost. The model charges additively for threshold predicates, including multiple thresholds of the same feature. This is an explicit modeling choice of the Boolean encoding, rather than a direct simulation of a clinical workflow.
11.4 Like-for-Like Baseline and Scope↩︎
We evaluate the original CART proxy recursively under the same product prior and the same additive predicate-cost model as the optimized decision diagram. Thus, the comparison of $236.4 for the CART proxy with $137.4 for the optimized diagram is a cost-optimization result for the encoded SBFE model. It is not a clinical validation or a claim about real diagnostic workflow costs.
References↩︎
Our implementation represents the formula in conjunctive normal form (CNF), and assign is implemented by adding \(l\) to the clause set as a unit clause, exhaustively applying the unit resolution and unit subsumption rules, to eliminate any clause that is a strict superset of another clause, and finally removing the unit clause \(l\). This simplifies the clause set so that occurrences of \(l\) are correctly removed and any resulting unit clauses are used to simplify the formula further.↩︎