 |
| Constraint and Consequence |
|
|
 | |
| Craig Holman Research Jabberwocky Quotations Contact | |
Home >
Jabberwocky 
Previous
Next
|
|
| |
Jabberwocky for June 5, 2008 |
|
The Constraint Calculus This work is derived from my doctoral dissertation and was written in 2001.
When you have eliminated the impossible, whatever remains, however
improbable, must be the truth. - Sir Arthur Conan Doyle, as Sherlock Holmes When searching for a model for a Boolean expression, it seems reasonable to assume that the expression evaluates to True and then to study the consequences that proceed from this assumption. These consequences will take the form of a system of constraints upon variables. If, within this system, we are able to construct a consistent set of constraints, then any interpretation that conforms to this set is a model of the expression. In this work, we present such a constraint calculus and show that is both sound and complete. Terminology Let E be a Boolean expression and let V denote the vocabulary of E. A constraint is any element (v, b) of the Cartesian product V x {True, False} and is a constraint of v to b. For convenience, (x, True) will be denoted by +x and (x, False) by -x. A set of constraints is inconsistent if it contains +x and -x for some variable x; otherwise, it is consistent. An interpretation of E is a consistent set of constraints that contains one constraint on each variable in V. A model of E is any interpretation of E under which E evaluates to True. A partial interpretation of E is a subset of an interpretation and is said to generate those interpretations of E that contain it as a subset. The empty set generates all interpretations of E. An interpretation is said to conform to a set of constraints if it contains that set of constraints as a subset. Constraints may be associated with nodes that are in trees or graphs. A binary constraint tree is a binary tree which has a Root node as its root, And and Or nodes as internal nodes, and Literal nodes, each possessing one constraint, as terminal nodes. A constraint tree is a general tree which has an And node as its root, And and Or nodes as internal nodes, and And nodes as terminal nodes. Each And node in a constraint tree is associated with a set of constraints, known as a guard set, which may be empty. Nodes in constraint trees are layers so that And nodes are at even distances, and Or nodes at odd distances, from the root node. A constraint graph is a directed acyclic graph in which the sole source is a Start node, the sole sink is a Stop node, and all other nodes are And nodes or Or nodes. Each And node in a constraint graph possesses a guard set. Nodes in constraint graphs are layered so that And nodes are at odd distances, and Or nodes at even distances, from the Start node. A selection of a binary constraint tree, constraint tree, or constraint graph is a set of nodes S such that 1. The root of the tree (graph) is in S. 2. If D is an And node and is in S, each child of D is in S. 3. If D is an Or node and is in S, exactly one child of X is in S. Each selection is associated with a selection set of constraints. For binary constraint trees, a selection set is the union of the constraints attached to the Literal nodes in a selection. For constraint trees and constraint graphs, a selection set is the union of the guard sets of the And nodes in a selection. Definition of the Constraint Calculus The Constraint Calculus is a method of constructing a set of all of the models of a Boolean expression. This calculus consists of the sequential application of five algorithms and is defined as follows: The Constraint Calculus 1. Apply the Build Tree algorithm to the Boolean expression E, yielding the binary expression tree T1. 2. Apply the Propagate Truth Value algorithm with the target truth-value of True to the binary expression tree T1, yielding the binary constraint tree T2. 3. Apply the Gather Junctors algorithm to the binary constraint tree T2, yielding the constraint tree T3. 4. Apply the Transform Tree To Graph algorithm to the constraint tree T3, yielding the constraint graph G. 5. Apply the Traverse Graph algorithm to the constraint graph G, yielding a set C of consistent selection sets that are partial interpretations of E. 6. For each partial interpretation P in C, add the interpretations of E that conform to P to the set of models M. Given a well-formed Boolean expression E, the Build Tree algorithm scans the expression and constructs a binary expression tree T1 that represents E. T1 is similar to a parse tree of the expression except that parentheses are implicit in the structure of the tree rather than being represented explicitly. This algorithm requires linear time and linear space. The application of the algorithm to the expression (Ø ( ( a Ú ( Ø b Ù a ) ) Ú c ) Ù b ) will yield the following binary expression tree:
The Propagate Truth Value Algorithm The binary expression tree T1 is transformed recursively by this algorithm into the binary constraint tree T2. The expression is assumed to evaluate to a target truth-value that is assigned to the root of the tree. This truth-value is then propagated throughout the tree, being inverted by and consuming Not nodes and inverting junctor nodes when appropriate. When a truth-value reaches a Literal node, its value is recorded there and the node is regarded as a constraint of the node's variable to that truth-value. This algorithm requires linear time and linear space. For example,
The binary constraint tree T2 is transformed recursively by this algorithm into a constraint tree T3. First, Root and Literal nodes are retyped as And nodes. Clusters of adjacent nodes of the same type are identified and collapsed into a single node of that type. When a cluster of And nodes is collapsed, the constraints which are carried by nodes in the cluster are added to a guard set of constraints which is associated with the surviving And node. When any cluster is collapsed, the children of nodes in the cluster that are not themselves in the cluster are formed into a list of children and attached to the surviving node. This algorithm requires linear time and linear. For example,
The Transform Tree Into Graph Algorithm A constraint tree T3 is transformed recursively by this algorithm into a directed acyclic constraint graph G which contains one source node of type Start, one sink node of type Stop, and all of the nodes from the constraint tree T3. Each And node in G has an outvalence of 1, which will facilitate recursive depth-first searching of the graph. Each subtree in T3 which has an Or node as a root is treated as a block. If an And node in T3 has more than one block as a child, then those blocks will be stacked up beneath the And node in G by having the And node point to a linked stack of child blocks. Each path from Start to Stop in the constraint graph corresponds to one selection of the constraint tree. This algorithm requires linear time and linear space. For example,
The application of this algorithm to the Start node of a constraint graph will result in a set of selection sets that can generate all of the models of the original expression. This algorithm performs a recursive, depth-first traversal of the constraint graph, searching for a path from the Start node to the Stop node that does not contain any conflicting constraints, and backtracking when a constraint conflict is encountered. While traveling along a path, the constraints contained in the guard sets of the And nodes along the path are collected. When a Stop node is visited, the current set of collected constraints is saved as a selection set. This algorithm may require exponential time and linear space. For example, an application of the algorithm to the constraint graph on the left produces the selection sets on the right in the order that they're listed:
Proof that the Constraint Calculus is Sound and Complete The proof of the soundness of the Constraint Calculus is the reverse of the proof of its completeness. The following definitions and lemmas will be used in these proofs. Let the primary constraint tree of an expression E be the binary constraint tree that is the result of the application of steps 1 and 2 of the constraint calculus to E. Lemma 1 Let E be a Boolean expression and let T2 be the primary binary constraint tree of E. An interpretation I is a model of E iff I conforms to a consistent selection set of T2. Proof Let D be the DNF-equivalent of E produced by distributing all disjunctors over conjunctors. Let U2 be the primary binary constraint tree of D and note that U2 could have been produced by distributing all Or nodes over the And nodes in T2. Distributing an And node over an Or node in a binary constraint tree changes neither the selections nor the selection sets of the tree. Thus, the selection sets of T2 and U2 are the same. There is a one-to-one correspondence between the clauses of D and the selection sets of U2 such that, if C is a clause of D and S is the selection set of U2 which corresponds to C, variable x occurs in a positive (negative) literal of C iff the constraint +x (-x) is in S. Thus, any interpretation that satisfies C must conform to S. This interpretation contains one constraint on every variable in the vocabulary of the expression and is necessarily consistent. Therefore, an interpretation I is a model of D iff I satisfies some clause of D iff I conforms to some consistent selection set of U2 iff I conforms to some consistent selection set of T2. However, since D and E are equivalent, I is a model of D iff I is a model of E. Thus, I is a model of E iff I conforms to some consistent selection set of T2. Q.E.D. Lemma 2 The Gather Junctors algorithm preserves selection sets. Proof The Gather Junctors algorithm first transforms Root and Literal nodes into And nodes. The algorithm then identifies clusters of adjacent nodes of the same type and collapses them into a single node of that type, transferring all constraints in an And cluster to the surviving node. The algorithm thus deletes unnecessary And nodes from and And cluster in a selection while leaving that selection's selection set unchanged. The algorithm also deletes unnecessary Or nodes from each selection. Neither nodes nor constraints are added to any selection. Thus, while each selection may lose some nodes, the selection set associated with that selection remains unchanged. Q.E.D. Lemma 3 The Transform Tree To Graph algorithm preserves selection sets. Proof The Transform Tree To Graph algorithm adds two nodes, one of type Start and the other of type Stop, to each selection of a constraint tree, but no nodes are removed from a selection and no guard sets are modified. Since Start and Stop nodes have no guard sets, no constraints are added to a selection set. Since no nodes are removed from a selection and no guard sets are modified, no constraints are removed from a selection set. Therefore, the algorithm preserves selection sets. Q.E.D. Lemma 4 The Traverse Graph algorithm produces precisely the consistent selection sets of a constraint graph. Proof Each directed path from the Start node to the Stop node of the constraint graph consists of precisely those nodes that are a selection of the graph. By collecting the constraints in the guard sets of the And nodes which lie on a path of the graph, the algorithm constructs a selection set. The Traverse Graph algorithm will backtrack and abandon a path only when the selection set being constructed becomes inconsistent. Thus, whenever the algorithm visits the Stop node, a consistent selection set has been constructed. Q.E.D. Theorem 1 Soundness of the Constraint Calculus - Apply the Constraint Calculus to an expression E, yielding a set of interpretations M. Every interpretation in M is a model of E. Proof Let T be the primary constraint tree of an expression E. Each interpretation in M conforms to a selection set produced by the Traverse Graph algorithm. Since the Traverse Graph algorithm produces precisely the consistent selection sets of a constraint graph, each interpretation in M conforms to a consistent selection set of the constraint graph (by Lemma 4). Since the Transform Tree To Graph and Gather Junctors algorithms preserve selection sets (by Lemmas 3 and 2), each interpretation in M conforms to a consistent selection set in the primary binary constraint tree. Since an interpretation I conforms to a consistent selection set of T iff I is a model of E (by Lemma 1), each interpretation in M is a model of E. Q.E.D. Theorem 2 Completeness of the Constraint Calculus - Apply the constraint calculus to an expression E, yielding a set of interpretations M. Every model of E is in M. Proof Let T be the primary binary constraint tree of E. For every interpretation I that is a model of E, there exists a consistent selection set of T that is a subset of I (by Lemma 1). Since the Gather Junctors and Transform Tree To Graph algorithms preserve selection sets (by Lemmas 2 and 3), for every interpretation I that is a model of E, there exists a consistent selection set of the constraint graph for E that is a subset of I. Since the Traverse Graph algorithm produces precisely the consistent selection sets of the constraint graph, for every interpretation I that is a model of E (by Lemma 4), the Traverse Graph algorithm produces a consistent set that is a subset of I. Since every model of E conforms to some selection set produced by the Traverse Graph algorithm and since every interpretation that conforms to a selection set produced by the Traverse Graph algorithm is added to the set M, every model of E is in M. Q.E.D. The Satisfiability-Determination Algorithm The Constraint Calculus is far too expensive to use for satisfiability testing without modification. Only one model needs to be constructed in order to demonstrate that an expression is satisfiable. The Satisfiability Determination algorithm is a modification of the Constraint Calculus. The first four steps of the algorithm are taken directly from the Constraint Calculus. The fifth step of the Constraint Calculus, the application of the Traverse Graph algorithm, is modified so that it terminates as soon as the first selection set has been constructed. If the Stop node is visited, the expression is satisfiable; otherwise, it is not. The Falsifiability-Determination Algorithm I cannot comprehend how any man can want anything but the truth. Marcus Aurelius Antoninus
It is only by lying to the limit that you can come at the truth. Sherwood Anderson We may determine the falsifiability of an expression E by determining the satisfiability of the complement of E. The Falsifiability Determination algorithm differs from the Satisfiability Determination algorithm only in that the target truth-value that is initially propagated during step 2 of the Satisfiability Determination algorithm is False rather than True. Any selection set produced during step 5 of this algorithm is a non-model generator for E. If the Stop node is visited, the expression is falsifiable; otherwise, it is not. |
| |
| Home >
Jabberwocky
Previous
Next
|
|
| Craig Holman Research Jabberwocky Quotations Contact | |
| |
| Patterncraft™ and Constraint and Consequence™ are trademarks of Craig Stewart Holman Copyright © 2008 Craig Stewart Holman All Rights Reserved. |
|
| | |
|
|
