02/02/2021

Learning Branching Heuristics for Propositional Model Counting

Pashootan Vaezipoor, Gil Lederman, Yuhuai Wu, Chris Maddison, Roger B Grosse, Sanjit A. Seshia, Fahiem Bacchus

Keywords:

Abstract Paper Similar Papers

Abstract: Propositional model counting, or #SAT, is the problem of computing the number of satisfying assignments of a Boolean formula. Many problems from different application areas, including many discrete probabilistic inference problems, can be translated into model counting problems to be solved by #SAT solvers. Exact #SAT solvers, however, are often not scalable to industrial size instances. In this paper, we present Neuro#, an approach for learning branching heuristics to improve the performance of exact #SAT solvers on instances from a given family of problems. We experimentally show that our method reduces the step count on similarly distributed held-out instances and generalizes to much larger instances from the same problem family. It is able to achieve these results on a number of different problem families having very different structures. In addition to step count improvements, Neuro# can also achieve orders of magnitude wall-clock speedups over the vanilla solver on larger instances in some problem families, despite the runtime overhead of querying the model.

The video of this talk cannot be embedded. You can watch it here:
https://slideslive.com/38949270
(Link will open in new window)
 0
 0
 0
 0
  Share    
This is an embedded video. Talk and the respective paper are published at AAAI 2021 virtual conference. If you are one of the authors of the paper and want to manage your upload, see the question "My papertalk has been externally embedded..." in the FAQ section.

Comments

Post Comment
no comments yet
code of conduct: tbd Characters remaining: 140

Similar Papers

 0
 0
 0
 0
 26:16 
 0
 0
 0
 0
 9:41 
 0
 0
 0
 0
 7:27 
 0
 0
 0
 0
 2:54 
 0
 0
 0
 0
 15:23 
 0
 0
 0
 0
 24:38 
 0
 0
 0
 0
 4:50 
 0
 0
 0
 0
 14:26 
 0
 0
 0
 0
 5:25 
 0
 0
 0
 0
 3:04 
 0
 0
 0
 0
 17:45 
 0
 0
 0
 0
 15:28 
 0
 0
 0
 0
 7:41 
 0
 0
 0
 0
 3:22 
 0
 0
 0
 0
 3:02 
 0
 0
 0
 0
 14:47 
 0
 0
 0
 0
 16:25 
 0
 0
 0
 0
 4:25 
 0
 0
 0
 0
 3:16 
 0
 0
 0
 0
 5:03 
 0
 0
 0
 0
 5:48 
 0
 0
 0
 0
 13:13 
 0
 0
 0
 0
 5:08 
 0
 0
 0
 1
 3:28 
 0
 0
 0
 0
 16:38 
 0
 0
 0
 0
 4:51 
 0
 0
 0
 0
 3:12 
 0
 0
 0
 0
 17:29 
 0
 0
 0
 0
 3:13 
 0
 0
 0
 0
 15:48 
 0
 0
 0
 0
 14:54 
 0
 0
 0
 0
 15:33 
 0
 0
 0
 0
 7:27 
 0
 0
 0
 0
 12:48 
 0
 0
 0
 0
 8:38 
 0
 0
 0
 0
 5:25 
 0
 0
 0
 0
 14:26 
 0
 0
 0
 0
 15:07 
 0
 0
 0
 0
 3:18 
 0
 0
 0
 1
 5:14