Method and system for performing propositional reasoning tasks by operating parallel processors

摘要

Propositional reasoning is performed on a massively-parallel processor, with sets of element value combinations being handled by separate processing units. A host processor operates as a problem-solver, generating requests for propositional reasoning, and also operates as an interface between the problem-solver and the parallel processor. In response to a request that includes a formula, the interface provides one or more formulae such as justifications and class restrictions. The interface provides instructions to the parallel processor based on each of these formulae. The instructions based on each formula are provided so that the set of element value combinations handled by each processing unit is not divided or forked into two subsets until necessary. If possible, forking is avoided by forcing the value of an element to the only value consistent with the current formula. Furthermore, if no additional processing unit is available for forking, the current formula is kept on a queue of formulas, and the corresponding instructions are subsequently repeated. In this manner, the host processor orders the formulas into a sequence that reduces the number of processing units required. When necessary, a selected assumption is forced to one value to free processing units; its other value is considered subsequently by backtracking. Each element value is assigned one or more bit positions in each processing unit, but when the values in all the processing units are the same for a given element, its bit position may be reclaimed, to reduce memory requirements. The interface also responds to a request for results by sending instructions that use circuitry in the parallel processor to obtain a combined result from the processing units.