Biblio

Both SAT and #SAT can represent difficult problems in seemingly dissimilar areas such as planning, verification,  and probabilistic  inference. Here, we examine an expressive new language, #∃SAT, that generalizes both of these languages.   #∃SAT problems require counting the number of satisfiable formulas in a concisely-describable  set of existentially quantified, propositional formulas. We characterize the expressiveness and worst-case difficulty of #∃SAT by proving it is complete for the complexity  class #P NP [1], and re- lating this class to more familiar complexity  classes. We also experiment with three new

general-purpose #∃SAT solvers on a battery  of problem distributions  including  a simple logistics domain. Our experiments show that, despite the formidable worst-case complex-

ity of #P NP [1], many of the instances can be solved efficiently  by noticing and exploiting a particular type of frequent structure.

Complementary problems play a central role in equilibrium finding, physical sim- ulation, and optimization.  As a consequence, we are interested in understanding how to solve these problems quickly, and this often involves approximation.  In this paper we present a method for approximately solving strictly monotone linear complementarity problems with a Galerkin approximation.  We also give bounds for the approximate error, and prove novel bounds on perturbation error. These perturbation  bounds suggest that a Galerkin approximation  may be much less sen- sitive to noise than the original LCP.