Research And Implementation Of The #QBF Systems Based On Extension Rule

Intelligence planning is a sequence of sets of actions that will achieve the goals of a problem. The valid sequence of sets of actions is called planning solution. At present, all the planners can get just one solution, but not the number of all the solutions of the problem, such as the number of winning strategies at oppositional planning, the dual games and so on. These intelligence planning problems can be transformed into #QBF through the BlackBox, but it is a pity that there is no #QBF counter now.To be aimed at these problems, new approaches of #QBF counting which based on extension rule are proposed to deal with the corresponding intelligence planning problems. The basic idea of the approaches is to deduce the set of all the maximum terms for #QBF counting and to use the inclusion-exclusion principle to circumvent the problem of space complexity. Compared with the resolution approaches, the more complementary literal(s) the clauses contain, the greater efficiency the approaches are, so our approaches can be seen as a complementarity to the resolution approaches. Firstly, a basic approach that based on the extension rule is proposed whose basic idea is the same as the idea described above. Secondly, to improve the efficiency, another approach that based on Knowledge Compilation is proposed too. The basic idea is to compile the pending problem to EPCCL, then do the #QBF counting. Thirdly, the idea of components analysis inspired the last approach. The basic idea of this approach is to decompose the pending problem into components and to solve the individual components, then to multiply the models of the individual components to get the models of the QBF problem. This approach also has ability to deal with the single literals. Compared with the anterior approaches, the last one can deal with more universal and larger #QBF counting problems.Based on the algorithms proposed above, we have implemented three new #QBF counting systems: #ER﹑#KCER and #CSER. Experiment proved that the time complexity of #ER is exponential and the efficiency is low when solving the general problems. #KCER is better than the #ER in theory, however the scale of the clauses after compiled is exponential in the worst. So the effect of #KCER is dissatisfactory. Because #CSER has the ability of single literal processing and component analyzing, it is better than the former two systems. More over, as there is no ready model counting system based on the extension rule inland, so our systems, especially the #CSER will be significant both in research and practice.