BACKGROUND 10001] Technological advances in hardware such as processors, memory, and storage continue to serve as a catalyst for creating larger and more complex software applications that provide a richer user experience by handling many different types of data types of media (e.g., voice, text and video), development programs, and so on. [0002] The hardware support counted on by these vendors in single-processor systems may be distant because historical circuit speedups associated with Moore's law no longer appear to be readily obtainable. The principle aspect of Moore's law is that approximately every eighteen months the number of transistors on a chip will double due, generally, to technological advances in device fabrication. Historically, when this was accomplished, the processor clock speed could also be increased. However, the heat density now associated with the more tightly packed transistors is so high that increasing the clock speed means heat cannot be efficiently and effectively dissipated. Thus, smaller devices no longer directly translate into faster and cooler running machines. [0003] One alternative being exploited is to simply employ more of the devices. In other words, in the realm of processors, for example, design parallel or multi-processor systems to accommodate the software demands. However, parallel processing systems require sophisticated coordination techniques for handling algorithms or computational thread processing. Constraint solving is useful in testing these coordination techniques. Traditional sequential algorithms, however, are notoriously difficult to reconstruct in ways that make effective use of all available shared-memory parallel processors. [0004] Constraint satisfaction problem (CSP) solvers - such as Boolean satisfiability (SAT) solvers - are in no way exceptions to the previous observation. Typically, sequential CSP solvers have a current state that includes a partial solution (an assignment to some of the constraint variables) from which the solver attempts to move to a new state with an augmented solution created by assigning one or more currently unassigned variables. The new assignmentation may engender other assignments through the propagation of constraints. Propagation of constraints, in turn, can lead to the detection of a conflict among the current assignments which (in order to relieve the conflict) must be partially undone, changed to new assignments, and re-propagated. [0005] In parallel processing systems, a parallel implementation of this problem solving regime per force has several parallel computations propagating constraints in the fashion just described. A problem is to merge several conflict-free solver states (post propagation) into a single conflict-free solver state. SUMMARY [0006] The following presents a simplified summary in order to provide a basic understanding of some aspects of the disclosed innovation. This summary is not an extensive overview, and it is not intended to identify key/critical elements or to delineate the scope thereof. Its sole purpose is to present some concepts in a simplified form as a prelude to the more detailed description that is presented later. [0007] The disclosed architecture provides support for parallel processing in generic constraint satisfaction problem (CSP) solvers. The state of a computational thread of the solvers is represented as a set of support graphs. Sets of support graphs are a recognized mechanism in the efficient implementation of truth maintenance systems (TMS), which are frequently an important component of generic CSP solvers. As described herein, the support graphs are used in a new way by merging the graphs in a pairwise fashion, yielding a new conflict-free graph. This allows construction of a CSP solver by mapping parallel propagation of constraints over multiple new assignments and reducing to a new problem solver state (with more variables assigned) by merging the states resulting from the multiple propagations. The architecture can be applied, generally, in any CSP solver having certain formal properties. For example, in one implementation, the architecture can be applied specifically in the context of a Boolean satisfiability (SAT) solver. [0008] The architecture disclosed and claimed herein comprises a computer-implemented system that facilitates solver processing. The system includes a bookkeeping component for representing input solver state of a computational thread as a set of graphs. A merge component performs pairwise merging of at least two input graphs of the set of graphs into a merged graph that represents final state of the computational thread. [0009] To the accomplishment of the foregoing and related ends, certain illustrative aspects of the disclosed innovation are described herein in connection with the following description and the annexed drawings. These aspects are indicative, however, of but a few of the various ways in which the principles disclosed herein can be employed and is intended to include all such aspects and their equivalents. Other advantages and novel features will become apparent from the following detailed description when considered in conjunction with the drawings. BRIEF DESCRIPTION OF THE DRAWINGS [0010] FIG. 1 illustrates a system that facilitates solver processing in accordance with a parallel implementation. [0011] FIG. 2 illustrates a methodology of processing solver state in accordance with the innovation. [0012] FIG. 3 illustrates an alternative parallel solver system that employs learning and reasoning to infer guesses for answer assignments. [0013] FIG. 4 illustrates an (L,K-deduction graph derived from an exemplary constraint propagation process. [0014] FIG. 5 illustrates a new graph for processing the conflicting constraint output from the support graph of FIG. 4. [0015] FIG. 6 illustrates a method of preparing and merging two support graphs. [0016] FIG. 7 illustrates a method of paring down two input support graphs for a pairwise merging process. [0017] FIG. 8 illustrates a method of processing conflicts of a merged graph. [0018] FIG. 9 illustrates a method of paring and merging support graphs into a final merged conflict-free graph for a sequential SAT solver. [0019] FIG. 10 illustrates a method of paring and merging support graphs into a final merged conflict-free graph for a parallel SAT solver. [0020] FIG. 11 illustrates a diagram of a system that applies solver state processing of the subject innovation to a multi-core processing system. [0021] FIG. 12 illustrates a diagram of a system that applies solver state processing in accordance with the subject innovation to multi-core multi-processor systems. [0022] FIG. 13 illustrates a diagram of a system that applies solver state processing in accordance with the subject innovation to solver state processing across separate computing systems. [0023] FIG. 14 illustrates is a diagram of a CSP solver system that employs a truth maintenance system and an inference engine for application as a problem solver in a large search space. [0024] FIG. 15 illustrates a block diagram of a computing system operable to employ the disclosed parallelized solver state architecture. [0025] FIG. 16 illustrates a schematic block diagram of an exemplary computing environment that can exploit parallelized solver processing according to the disclosed innovation. DETAILED DESCRIPTION [0026] The disclosed architecture provides a solution for shared-memory parallel processor systems that, conventionally, have notoriously been difficult to address even as a sequential problem. The innovation provides lock-free state merging in parallel constraint satisfaction problem (CSP) solvers. The state of a computational thread of the solvers is represented as a set of support graphs. (In the interest of simplicity, the phrase "support graph" will be used rather than "set of support graphs", when no coniusion will ensue.) These support graphs are used in a new way by merging the graphs in a pairwise fashion describing a process that is lock-free and which yields a new conflict-free support graph. The architecture can be applied, generally, in any CSP solver where the underlying problem is reducible to Boolean satisfiability, and in one specific implementation, the architecture can be applied specifically in the context of a Boolean satisfiability (SAT) solver. [0027] In the specific implementation of SAT solvers, the SAT solver problem begins with a set of Boolean formulae that engender the problem in one of two ways. It is desired to know whether the formula is always true. Put another way, it is desired to determine if the formula is a theorem. An equivalent question, by taking the complement (or negation) of any formula, is to determine if the formula is satisfiable. That is to ask, is there an assignment of variables that makes the formula true? For purposes of mechanization, this can be a way the problem is approached. It is attacked as a satisfiability problem and not a theorem proving problem. [0028] In the space of digital design, it is desired to know whether a Boolean formula is a theorem or not. Rather than proving the formula to be shown is a theorem, show that the negation is not satisfiable. The Boolean formula is presented in a canonical form such as a disjunctive normal form, for example. The disjunctive normal form is a representation where the set of formulae is finite, and there are only two logical connectives that occur in any one of the formulae-a negation sign (logical NOT) and the disjunction (or logical OR). Accordingly, in order for the original problem, now in canonical form, to be satisfiable, there is an assignment of variables that ensures these disjunctive formulae are true. Each of the formulae in the canonical form is called a clause. As used herein, the term "clause" can also refer to a constraint. [0029] Oftentimes in such complex domains such as CSP solvers, there is no analytic method by which even a partial solution may be derived. One must assume an answer -essentially a guess. Consequently, initial assumptions once deemed true by a program can change over time and later be discovered to be false. Accordingly, the program has the problem of undoing inferences it might have made, based on assumptions later found to be false. To be efficient, the process attempts to undo as little as possible. [0030] A SAT confronts the problem just described because in order to demonstrate satisfiability, a partial assignment of answers is guessed. The guess causes other Boolean variable answers to be assigned because of the logical consequences of the new guess. The result of such a guess is that either a successful set of guesses is eventually made which cause all the variables to become assigned, or the last guess made leads to a logical inconsistency, at which point one of the guesses is given up. [0031| Conventionally, chronological backtracking can be employed to move backward, choosing values for one variable at a time. This backtracking may continue until a variable has no legal values left to assign. [0032] The disclosed innovation employs "non-chronological" backtracking by providing the capability to undo the most relevant assumptions, for example, change only that one assumption, and change nothing to the intermediate assumptions. In other words, the algorithm can go back in the arbitrary path, pick one assumption, and change only that assumption, in contrast to conventional systems where backing up changes all nodes between the current position and some earlier position. [0033] The innovation is now described with reference to the drawings, wherein like reference numerals are used to refer to like elements throughout. In the following description, for purposes of explanation, numerous specific details are set forth in order to provide a thorough understanding thereof It may be evident, however, that the innovation can be practiced without these specific details. In other instances, well-known structures and devices are shown in block diagram form in order to facilitate a description thereof [0034] Referring initially to the drawings, FIG. 1 illustrates a system 100 that facilitates solver processing in accordance with a parallel implementation. The system 100 includes a bookkeeping component 102 for representing solver state 104 (denoted SOLVER STATEj, SOLVER STATE2,...,SOLVER STATEN, where N is a positive integer) associated with processing of a computational thread parallel solvers as a set of support graphs. The solver state 104 can be received from different systems in a parallel fashion for processing by the bookkeeping component 102. The bookkeeping component 102 processes the solver state 104 into support graphs for subsequent merging. The system 100 can also include a merge component 106 for pairwise merging of at least two input support graphs of the set of support graphs into a merged graph that represents the final state of the computation thread. [0035] Manipulation of the support graphs by the bookkeeping and merge components (102 and 106) can be simultaneous. In other words, solver state from one of the solvers is received and processed during the processing of solver state from another solver. [0036] In one implementation, the bookkeeping component 102 receives the input solver state 104 from parallel CSP solvers operating on the computation thread. As described in more detail infra, a CSP solver is defined according to a lattice of valuations A and a set of values Z), where D and A are the same set. In a more specific alternative implementation, the bookkeeping component 102 receives the input solver state 104 from parallel Boolean SAT solvers operating on the computation thread. [0037] Where the input solver state 104 is from two parallel SAT solvers operating on the computational thread, the merge component 102 facilitates adding n new and distinct literals to each of n copies of an L-complete, K-consistent deduction graph, where n is a positive integer. This will also be described further hereinbelow. [0038] The merge component 106 merges the input solver state into the merged graph in a lock-free manner, without cycles, and eliminates conflicts in the merged graph, thereby outputting a conflict-free graph 108. [0039] With respect to lock-free processing, one way of achieving parallelism is to have the capability of handling parallel thread processing. In other words, there exist a number of parallel threads which eventually require results finalization. [0040] One conventional way of performing parallel thread handling is that a first thread simply locks the other threads out of some shared data structure until the first thread has reached a result. It then becomes incumbent upon the other threads obtain results that are consistent with previous thread results. [0041] The subject innovation avoids conventional locking by processing one-step ahead, in parallel, and then combining the results. Accordingly, this method is lock-free, in that, since there are m independent agents, where m is a positive integer, each agent has taken a step ahead, and in order to get the overall answer, the agents must combine the results. At the heart of the process, results are combined two at a time. [0042] When merging support graphs, there are several undesirable things that can happen. First, a conflict occurs between the two graphs. In other words, a variable x has been assigned a true value in a first graph and the same variable x in the other graph has the assignment false. Solving, the two graphs are merged and a set of assumptions is found that leads to this conflict. Once found, the associated assumption or one of the assumptions, is withdrawn. [0043] A second problem can occur when as assignment in one graph is an assumption and the same assignment in another graph is derived by unit resolution. If graph merger is now attempted, the resulting graph would exhibit a cycle. To resolve, assumptions are given up in a very economical way using a greedy method. This is described in greater detail infra. [ 0044] FIG. 2 illustrates a methodology of processing solver state in accordance with the innovation. While, for purposes of simplicity of explanation, the one or more methodologies shown herein, for example, in the form of a flow chart or flow diagram, are shown and described as a series of acts, it is to be understood and appreciated that the subject innovation is not limited by the order of acts, as some acts may, in accordance therewith, occur in a different order and/or concurrently with other acts from that shown and described herein. For example, those skilled in the art will understand and appreciate that a methodology could alternatively be represented as a series of interrelated states or events, such as in a state diagram. Moreover, not all illustrated acts may be required to implement a methodology in accordance with the innovation. [0045] At 200, support graphs are generated from the solver states of parallel solvers. At 202, the support graphs of solver state are received, the solver state associated with processing of a computational thread. At 204, the support graphs from each solver are pared down simultaneously for merging of nodes having the same literals. At 206, the support graphs are pairwise merged into a merged support graph that represents the final state of the computational thread. At 208, constraint propagation is initiated to achieve completeness of the merged graph. At 210, non-chronological backtracking is utilized during constraint propagation to change previous assumptions and resolve conflicts. At 212, conflicting literals are eliminated to output a conflict-free merged graph. [0046] Referring now to FIG. 3, there is illustrated an alternative parallel solver system 300 that employs learning and reasoning to infer guesses for assignment of answers. The system 300 includes multiple systems (e.g., two sequential solver systems) 302 that generate solver state. For example, a first system 304 (denoted SYSTEMA), a first sequential CSP solver, for example, generates solver state 306 (denoted SOLVER STATEAI,.--,SOLVER STATEAS, where S is a positive integer), and a second system 308 (denoted SYSTEMB), a second sequential CSP solver, for example, generates solver state 308 (denoted SOLVER STATEB 1,.. - ,SOLVER STATEBT, where T is a positive integer). [0047] The bookkeeping component 102 receives the solver state (306 and 310) from the corresponding first and second systems (304 and 308) and creates graphs (e.g., support graphs) of the solver state for parallel thread processing and that accounts for system constraints. The graphs are passed to the merge component 106 for merging into a merged graph having conflict-free state 108. However, the merged graph may not be complete. Accordingly, constraint propagation facilitated by a propagation component 312 is utilized to ensure completeness in the merged graph. This is described in greater detail hereinbelow. The propagation component 312 also facilitates non-chronological backtracking as part of the constraint propagation to directly change an earlier assumption without changing an intermediate assumption. [0048] The system 300 can also employ a learning and reasoning component 314 (also referred to herein as an inference engine) that facilitates making inferences about variable assignments based on guesses during constraint propagation. (0049] The system 300 can operate in applications where not all of the answers are known. Accordingly, assumptions are made about what is going in the world. For example, as a server program is exposed to more data, it can occur that earlier assumptions that the program made will be discovered to be false. The program then has the problem of undoing inferences that might have made based on false premises. [0050] In the satisfiability problem, a similar problem can exist because in order to demonstrate satisfiability, an assignment of answers may have to be guessed. In other words, in the sequential case when a new guess is made, this causes other Boolean variable answers to be assigned because of the logical consequences of the new guess. Moreover, one of two things eventually happens. Either a successful set of guesses is made, which cause all the variables to become assigned, or the last guess made leads to a logical inconsistency, at which point one of the guesses is given up. [0051] In the most classical version of Boolean satisfiability, the sign of the last guess is changed so if previously the Boolean variable was assigned false, the assignment is changed to true and the process proceeds again. It is possible that a logical inconsistency occurs when an assignment can be neither true nor false, which means that some earlier assignment made must have been wrong. [0052] Rather than backing up and moving forward repeatedly, as necessary, the actual set of assumptions that lead to the observed conflict is identified. Once a conflict has been observed, it is desired to diagnose exactly what leads to the conflict, which may or may not be the last assimiption made. Such a diagnosis can be precisely made and consequently a set of incompatible assumptions identified. [0053] The subject architecture (e.g., in connection with selection) can employ various learning and reasoning based schemes for carrying out various aspects thereof. For example. a process for determining which assignment to toggle (e.g., from true to false or from false to true) can be facilitated via an automatic classifier system and process. [0054] A classifier is a function that maps an input attribute vector, x = (xl, x2, x3, x4, xn), to a class label class(x). The classifier can also output a confidence that the input belongs to a class, that is, f(x) = confldence(class{x)). Such classification can employ a probabilistic and/or other statistical analysis (e.g., one factoring into the analysis utilities and costs to maximize the expected value to one or more people) to prognose or infer an action that a user desires to be automatically performed. [0055] As used herein, terms "to infer" and "inference" refer generally to the process of reasoning about or inferring states of the system, environment, and/or user from a set of observations as captured via events and/or data. Inference can be employed to identify a specific context or action, or can generate a probability distribution over states, for example. The inference can be probabilistic-that is, the computation of a probability distribution over states of interest based on a consideration of data and events. Inference can also refer to techniques employed for composing higher-level events from a set of events and/or data. Such inference results in the construction of new events or actions from a set of observed events and/or stored event data, whether or not the events are correlated in close temporal proximity, and whether the events and data come from one or several event and data sources. [0056] A support vector machine (SVM) is an example of a classifier that can be employed. The SVM operates by finding a hypersurface in the space of possible inputs that splits the triggering input events from the non-triggering events in an optimal way. Intuitively, this makes the classification correct for testing data that is near, but not identical to training data. Other directed and undirected model classification approaches include, for example, various forms of statistical regression, naive Bayes, Bayesian networks, decision trees, neural networks, fuzzy logic models, and other statistical classification models representing different patterns of independence can be employed. Classification as used herein also is inclusive of methods used to assign rank and/or priority. [0057] As will be readily appreciated from the subject specification, the subject architecture can employ classifiers that are explicitly trained (e.g., via a generic training data) as well as implicitly trained (e.g., via observing user behavior, receiving extrinsic information). For example, SVM's are configured via a learning or training phase within a classifier constructor and feature selection module. Thus, the classifier(s) can be employed to automatically learn and perform a number of functions according to predetermined criteria. [0058] In other words, the learning and reasoning component 314 can apply learned constraints for conflict processing. One example, as described below, one learned constraint can be added to a sequential SAT solver for conflict resolution. Similarly, in a parallel SAT solver, several learned constraints can be added during constraint propagation processing. [0059] Prior to looking at a constraint propagation example, preliminary information is provided for a better understanding. A constraint satisfaction problem (CSP) is typically described as follows: given a finite set of variables K, a (typically finite) set of values D, a (possibly infinite) lattice of valuations and a finite set of functions (constraints) D —> A, find a tuple in E^^ such that the lattice meet among that tuple's images in all the constraints is maximal in A. Following is a description where D and A are both the lattice of Booleans, specifically describing the invention in the context of a SAT solver. This restriction notwithstanding, the invention is generalizable to any CSP where D and A are the same set. [0060] Variables are denoted Xi,X2,...,Xn, where n is a positive integer. Literals are "signed" variables: Xi,"'Xi,X2,~'X2,... . L is the set of literals with / ranging over L. A clause is a finite set of literals including the empty clause, denoted n. A clause {Xi,*iX2, X3,"'X4} is often written instead as Xi v -'X2 v X3 v -'X4 (the logical OR (v) of its elements). Any finite set of propositional formulae can be rendered as a logically equivalent finite set of clauses. [0061] A variable can be unassigned, or assigned a value of True (e.g., Xi) or False (e.g., ""Xi). An assignment of the value True to the variable x is conflated with the literal x. An assignment of the value False to the variable x is conflated with the literal ""X. Valuations are attributed to clauses as a result of lifting assignments from variables to clauses. A clause with an assignment of True is satisfied, and a clause with an assignment of False is violated. Satisfiability is the question of whether there is an assignment of logical variables that satisfies a set of clauses. Tautology is the question of whether a set of clauses is satisfied by every assignment. Satisfiability and tautology are dual concepts in that a formula is a tautology if and only if its negation is unsatisfiable. [0062] Let Abe a set of clauses over the literals in L. An (ij/Q-'eduction graph is a directed graph whose nodes are labeled with individual literals paired with subsets of L and whose edges are labeled with members of ^. When there is no confusion about which L and K are meant, the graph is referred to simply as a deduction graph. A node is a ^-antecedent to another just in case there is a directed edge from the first to the second where the edge is labeled with the clause k. [0063] An {L,K) deduction graph is well-labeled just in case the label on a node is the union of the labels on its antecedent nodes, if the node / has no incoming arcs then it is labeled with {/}, all incoming edges to the node for literal / are labeled with a clause of the form all outgoing edges from the node for the literal / are labeled with a clause of the form Whenever there is an edge labeled incident upon the / node, there are m-1 other edges labeled that are also incident upon the / node. [0064] A node / in an (Z,,Ar)-deduction graph labeled with a singleton set consisting of itself (e.g., is called an assumption literal. A well-labeled (L,/Q-deduction graph is uniquely justified if the incoming arcs incident upon a node are labeled with exactly one clause. A well-labeled (L,K-deduction graph is K-consistent just in case it does not contain both the nodes / and -l. A well-labeled (L,,K-deduction graph is K-complete just in case for every k in K of the form , whenever are in the graph, / is in the graph with input incident edges labeled with k. An acyclic well-labeled (L,.K-deduction graph, G, is L-complete if there is no larger (in terms of nodes) well-labeled graph, G'. [0065] FIG. 4 and FIG. 5 illustrate a parallelized solver example that employs support graphs for conflict processing. FIG. 4 illustrates an (L,K)-deduction graph 400 derived from an exemplary constraint propagation process. To illustrate application of the above definitions, consider an example of a satisfiability problem and an attempted partial solution. Begin with an initial set of constraints C that include, and a current stack of assumptions. In the deduction graph 400, assumptions are modeled as assumption nodes, which nodes have no input arc. Accordingly, the assumptions for the graph 400 include The graph 400 includes four assumption nodes: a first assumption node 402 where Xi has been assigned true (e.g., Xt); a second assumption node 404 where X9 has been assigned false (e.g., ""Xg); a third assumption node 406 where Xio has been assigned false (e.g., ""Xio); and, a fourth assumption node 408 where Xn has been assigned false (e.g., ""Xii). [0066] Looking at a snapshot in time, the graph 400 indicates that assumption node 402 has an assignment of true to Xi (e.g., Xi), and assumption node 404 has an assignment of false to X9 (e.g., "^Xg). Now consider the edges labeled C02, the constraint clause ©2 = (""Xi v X3 v X9), as listed above; in other words, it can be read as "not Xi or X3 or X9." However, notice that in the constraint C02, Xi appears negatively as ~^X\, which means that the assignment as true in the graph 400 makes the disjunct false, and X9 as being assigned negatively, also makes X9 disjunct false. But the overall constraint CO2 has to be made true, and the only remaining way that can get constraint clause C02 to be true is when X3 is assigned to be true (e.g., X3). This is exactly what the graph 400 indicates at node 410, by assigning X\ as true. Thus, based on the assumptions at the input nodes 402 and 404, and the associated constraint t02, the only way to satisfy the constraint C02 is to assign X3 as true. This is an application of unit resolution. [0067] Continuing with the other nodes, the edge to a node 412 uses the constraint coi = ("Xi y X2). However, Xi at the node 402 is assigned true, leaving the only remaining possibility in satisfying the constraint coi is. to assign X2 at node 412 as true. Looking at the edges labeled C03, the constraint clause ©3 = (-'X2 v ~'X3 v X4) can only be satisfied by^ assigning true to X4 at node 414. In other words, the input nodes to 414 are 410 and 412, which assign true to X3 and X2, respectively, leaving the only remaining possible way to satisfy C03 is to assign true to X4. [0068] Looking at the edges labeled with C04, the constraint clause ©4 = ("'X4 v X5 v Xio) can only be satisfied by assigning true to X5 at node 416, since the input Xio is assigned false and the input X4 is assigned true. The edges labeled C05 use the constraint clause C05 = (~'X4 v Xe V Xii), which can only be satisfied by assigning true to Xe at node 418, since the inputs xl 1 is assigned false and the input X4 is assigned true. Finally, the edges labeled coe use the constraint clause co6 = (""Xs v "'Xg), which constraint fails based on the existing assignments of X5 true and Xe true at the corresponding nodes 416 and 418. [0069] Constraint propagation leads to the (i,iO-deduction graph 400 and, when reaching a last node 420, outputs a newly-derived constraint (written in a different form), O)C(K(C06)) = ""(Xl A --Xg A ''Xio A "-Xn), where K (kappa) represents "conflict" and the constraint is a report of what went wrong. Here, the output (OC(K(CO6)) indicates that it cannot be that simultaneously, Xi is true, X9 is false, Xio is false, and Xn is false, one of which has to be given up for further processing. This is equivalent to not which is in correct form. FIG. 5 illustrates a new graph 500 for processing the conflicting constraint output from the support graph of FIG. 4. Selecting assumptions for three of four of the above yields the new graph 500 and yet another newly-derived output constraint [0070] More specifically, the graph 500 is created by making assumptions (dropping one of the early assumptions), using assumption nodes 502, 504, and 506 as respectively. Beginning with these assumptions and applying the newly-derived constraint to the edges yields an assignment of false to Xi at node 508 to satisfy the constraint [0071] Looking at the edges labeled C07, another assumption node 510 (assigned Xi2@{Xi2}) is introduced, and the constraint clause can only be satisfied by assigning true to x? at node 512, since the input X1 is assigned false and the input X12 is assigned true. [0072] Looking at the edge labeled cog, the constraint clause can only be satisfied by assigning true to Xg at node 514, since the input X1 is assigned false. Now considering the edges labeled cog, the constraint clause cannot be satisfied using the current inputs (node 512, node 514, and an assumption node 516). Thus, the newly-derived constraint output at node 518, is a report of what went wrong with the deduction graph 500. The constraint derivation process continues until no conflict states exist. [0073] Described in a more general way, once support graphs are obtained for the solver states of each parallel solver thread, merging can be commenced. Although the description focuses on pairwise merging, it is within contemplation that merging can be accomplished using more than two graphs. State merging is lock-free. In other words, one conventional way of achieving parallelism involves threads processing. For example, where a multiplicity of parallel threads is processing data, eventually it is desired to merge the results of the threads. One way of doing this is by a first thread simply locking the other threads out from some shared data structure until the first thread completes its process. Accordingly, it is incumbent upon the other locked-out threads to write results that are consistent with those that have already been written. This conventional architecture is at least inefficient. The disclosed architecture avoids such explicit locking mechanism. [0074] As described supra, the algorithm(s) perform processing one step ahead in parallel and then the results are combined. In other words, in order to arrive at the overall result, each agent processes ahead one step and the separate interim results are combined, and this continues until reaching the overall answer. Additionally, conflict processing is resolved and the merge process is cycle free. [0075] As before, in deconflict processing, one or more assumptions may be given up in one or the other of the graphs. Moreover, it is desirable to be very economical about what assumptions to give up. By defining all of the sets of information (e.g., assumptions, deductions, graphs,...) used by the disclosed architecture, a reduction algorithm (also referred to herein as redux) makes choices in a way that it gives up as little as possible between the two graphs being merged. Recall that in a single graph case, the point of identifying these conflicts is to identify an assumption that has as little a consequence as possible if it were to be given up, rather than having to backup over several previous assumptions, which a point for the set of support graphs. [0076] Now applying the same technique(s) to a pair of graphs, the graphs are merged in a cycle-free fashion such that if an assumption is given up, as little as possible is affected or lost. This can be addressed by utilizing a "greedy" method or algorithm. In other words, the method finds a cheap way of minimizing what is being given up by making the choice that seems to be the best at the particular point in time. More intensive algorithms can be employed that utilize much more analysis; however, in one implementation, the greedy method is sufficient. [0077] FIG. 6 illustrates a method of preparing and merging two support graphs. At 600, two support graphs are received for processing. At 602, the graphs are pared (or reduced) down for merging nodes that correspond to the same literals to reduce or eliminate cycling using a greedy method. At 604, merge the support graphs into a merged graph. At 606, process the merged graph for completeness by propagating constraints, if needed. At 608, process merged graph for conflicts, if needed. At 610, the final merged graph is output that represents conflict-free solver state. [0078] In preparation for a more detailed description of how two (/,,Ar)-deduction graphs can be merged, the following definitions are presented. If G, G' are acyclic, i-complete {L,K)- deduction graphs, then CG,G' is the set of assumptions in common to the graphs G and GAc is the set of assumptions of G. Do is the set of deductions of G. AG,G ■ is the set of assumptions of G that are deductions of G'. BG,G ■ is the set of assumptions of G that are not mentioned in G' AG = CG,G'^AG,G''^ BG,G' AG=CG,G'^AG',G^ BG;G /G'. AG -^ 2^'^G-fG being a function that produces the dependents of an assumption in G. he: L-AG —* 2'^'^- he being a function that produces the antecedents of a deduction in G. [0079] FIG. 7 illustrates a method of paring down two input support graphs for a pairwise merging process. At 700, in this particular implementation, this process is initiated according to a function called redux. The function redux (G.G') produces a pair of graphs (Gi,G2) defined as follows. At 702, a first definition is provided: Let / s AG,G' be a node such that J/G'(/)| (the size of the set of dependents) is at least as large as the choice of any other assumption node in AG,G- At 704, a second definition is provided: Let /' G AG',G be a node such that 1/G{/ ')| is at least as large as the choice of any other assumption node in AG;G- At 706, if |/b