Research Of The #SAT Approximate Solvers Based On Extension Rule

Artificial planning is a frontal research domain which has been developing rapidly from late 1950s.Up to the present,its research has come through more than half of century,and gained recently revolutionary development.The approach of compiling planning problem to SAT problem,then utilizing high efficient SAT solver to resolve it is one of the main approaches solving planning problem.Researches indicated that the indirect approach executed more rapidly than direct approach.#SAT problem is a more challenged problem caused by SAT problem.Many probabilistic inference problems,such as analysis of degree of belief,inference of Bayesian networks,probabilistic planning problem,all may be translated into #SAT problem,and resolved by #SAT solver.#SAT problem is the prototype of #P-complete problems.Therefore,almost all #P-complete problems can reduce to #SAT problem in polynomial time.Consequently,researching the resolved techniques of #SAT has important theory value and application significance to not only planning domain but also other domains.At present,many #SAT solvers are based on resolution principle.Extension rule is a SAT solving method which symmetrizes the resolution.Furthermore,it was extended to solve #SAT problem.However,the time complexity is exponential,so the efficiency is low.In this paper,we propose two approximate model counting algorithms based on extension rule:up-down bound approximation(Up-DownApprox)and sample approximation (SampleApprox).Up-DownApprox firstly counts the approximate number of no satisfactory assignments then counts the approximate number of models.Its main idea is as follow.If we view every consecutive add sum of the inclusion-exclusion principle as an item,then the sum of front odd items is an up bound,and the sum of front even items is a down bound.We analyse that under what condition the approximate dispersion of some up or down bound and the accurate number of no satisfactory assignments is in a range(e.g.≤0.01 or smaller),so the up or down bound may be viewed as the approximate number of no satisfactory assignments, then we can count the approximate number of models.SampleApprox combines the sample approach and the improved algorithm of exclusion rule MCIER to achieve the approximate number of models.Its main idea is following.At first,we choose several variables and assign value to them.Like this,we can restrict a subspace.Then use the sample approach to count the approximate multiplier of the total number of models and the number of models of the restricted subspace,and utilize MCIER to get the number of models of the restricted subspace. Furthermore,the result of multiplying the approximate multiplier with the number of models of the restricted subspace is the approximate number of models. We design two #SAT approximate solvers according to two algorithms above:UDApp and SamApp,and achieve the algorithm of accurate model counting MCER for comparing the two approximate solvers with accurate solver.Experiment results indicated that the two approximate solvers executed more rapidly than accurate solver MCER.Where,SamApp has multiple improvement on the running speed.In the accuracy,UDApp can gain the approximate number of models which is very near to the accurate value if the approximate dispersion is adequate small.And SamApp can gain the approximate number of models which is relatively close to the accurate value.