ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Mon 8 Apr 2019 12:00 - 12:30 at SUN I - SAT and SMT I Chair(s): Lijun Zhang

Given a set of constraints F and a user-defined weight function W on the assignment space, the problem of constrained sampling is to sample satisfying assignments of F conditioned on W. Constrained sampling is a fundamental problem with applications in probabilistic reasoning, synthesis, software and hardware testing. Consequently, the problem of sampling has been subject to intense theoretical and practical investigations over the years. Despite this, there still remains a gap between theory and practice. In particular, there has been significant progress in the development of sampling techniques when W is a uniform distribution but such techniques fail to handle general weight functions W. Furthermore, we are, often, interested in $Σ_1^1$ formulas, i.e. G(X) := ∃Y F (X, Y ) for some F; typically the set of variables Y are introduced as auxiliary variables during encoding of constraints to F. In this context, one wonders whether it is possible to design sampling techniques whose runtime performance is agnostic to the underlying weight distribution and can handle $Σ_1^1$ formulas? The primary contribution of this work is a novel technique, called WAPS, for sampling over arbitrary W. WAPS is based on our recently discov- ered connection between knowledge compilation and uniform sampling. WAPS proceeds by compiling F into a well studied compiled form, d-DNNF, which allows sampling operations to be conducted in linear time in the size of the compiled form. We demonstrate that WAPS is able to significantly outperform existing state-of-the-art weighted and projected sampler WeightGen, by up to 3 orders of magnitude in runtime while achieving a geometric speedup of 296× and solving 564 more instances out of 773. The distribution generated by WAPS is statistically indistin- guishable from that generated by an ideal weighted and projected sampler. Furthermore, WAPS is almost oblivious to the number of samples requested.

Mon 8 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30
SAT and SMT ITACAS at SUN I
Chair(s): Lijun Zhang Chinese Academy of Sciences
10:30
30m
Talk
Decomposing Farkas Interpolants
TACAS
Martin Blicha USI Lugano, Switzerland, Antti Hyvärinen , Jan Kofroň Charles University, Natasha Sharygina USI Lugano, Switzerland
Link to publication
11:00
30m
Talk
Parallel SAT Simplification on GPU Architectures
TACAS
Muhammad Osama Eindhoven University of Technology, Anton Wijs Eindhoven University of Technology
Link to publication
11:30
30m
Talk
Encoding Redundancy for Satisfaction-Driven Clause LearningBest paper nomination
TACAS
Marijn Heule The University of Texas at Austin, Benjamin Kiesl CISPA Helmholtz Center for Information Security, Armin Biere Johannes Kepler University Linz
Link to publication
12:00
30m
Talk
WAPS: Weighted and Projected Sampling
TACAS
Rahul Gupta , Shubham Sharma , Subhajit Roy IIT Kanpur, India, Kuldeep S. Meel National University of Singapore
Link to publication