טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentMirron Rozanov
SubjectAn Approximation Scheme for Weighet and Non-Weighted
Model Counting
DepartmentDepartment of Industrial Engineering and Management
Supervisors Full Professor Strichman Ofer
Full Professor Domshlak Carmel
Full Thesis textFull thesis text - English Version


Abstract

Model-Counting (MC) is the problem of determining the number of solutions (models) for a given propositional formula. Weighted Model Counting

(WMC) is the problem of finding the total weight of the models of a propositional formula, where that weight is based on weights assigned to each of the literals. MC and WMC are #P problems (#P is the class of problems of finding the number of solutions for an NP hard problem). There are efficient methods for exact counting, but since the problem is hard both theoretically and in practice, it makes sense to find approximations. Indeed several approaches exist for MC and WMC approximations, and for approximating lower/upper bounds on the count/weighted count. Those methods are usually based on various sampling methodologies. Another approach tries to provide lower and upper bounds by adding constraints to the target formula that reduce the number of solutions in a predictable manner. In this thesis we describe a new approach to approximating MC and WMC. Our solution is based on a controlled reduction of the number of models or their weight by adding specially constructed constraints. We present several types of constraints and methods of using them in order to approximate the model count or the weight of a given propositional formula.

We show theoretically and experimentally that a single constraint, on average, removes the expected ratio of formula weight or solutions. Unfortunately, however, our experiments with real formulas show that the variance in the number of removed solutions (or formula weight) is too high to create a practical approximation scheme.