Thu 19 Nov 2020 23:40 - 00:00 at SPLASH-I - R-3 Chair(s): Pranav Kant, Xiangzhe Xu
Modern SAT solvers are extremely efficient at solving boolean satisfiability problems, enabling a wide spectrum of techniques for checking, verifying, and validating real-world programs. What remains challenging, though, is how to encode a domain problem (e.g., model checking) into a SAT formula because the same problem can have multiple distinct encodings, which can yield performance results that are orders-of-magnitude apart, regardless of the underlying solvers used. We develop Satune, a tool that can automatically synthesize SAT encoders for different problem domains. Satune employs a DSL that allows developers to express domain problems at a high level and a search algorithm that can effectively find efficient solutions. The search process is guided by observations made over example encodings and their performance for the domain and hence Satune can quickly synthesize a high-performance encoder by incorporating patterns from examples that yield good performance. A thorough evaluation with JMCR, SyPet, Dirk, Hexiom, Sudoku, and KillerSudoku demonstrates that Satune can easily synthesize high-performance encoders for different domains including model checking, synthesis, and games. These encoders generate constraint problems that are often several orders of magnitude faster to solve than the original encodings used by the tools.
Thu 19 Nov Times are displayed in time zone: Central Time (US & Canada) change
11:00 - 12:20: R-3OOPSLA at SPLASH-I +12h Chair(s): Marieke HuismanUniversity of Twente, Michael CoblenzUniversity of Maryland at College Park | |||
11:00 - 11:20 Talk | Compiling Symbolic Execution with Staging and Algebraic Effects OOPSLA Guannan WeiPurdue University, Oliver BračevacPurdue University, Shangyin TanPurdue University, Tiark RompfPurdue University Link to publication DOI Pre-print Media Attached | ||
11:20 - 11:40 Talk | Projection-Based Runtime Assertions for Testing and Debugging Quantum Programs OOPSLA Gushu LiUniversity of California at Santa Barbara, Li ZhouMax Planck Institute for Security and Privacy, Nengkun YuUniversity of Technology Sydney, Yufei DingUniversity of California at Santa Barbara, Mingsheng YingUniversity of Technology Sydney / Institute of Software at Chinese Academy of Sciences / Tsinghua University, Yuan XieUniversity of California at Santa Barbara Link to publication DOI Pre-print Media Attached | ||
11:40 - 12:00 Talk | Satune: Synthesizing Efficient SAT Encoders OOPSLA Hamed GorjiaraUniversity of California at Irvine, Guoqing Harry XuUniversity of California at Los Angeles, Brian DemskyUniversity of California at Irvine Link to publication DOI Media Attached | ||
12:00 - 12:20 Talk | The Anchor Verifier for Blocking and Non-blocking Concurrent Software OOPSLA Link to publication DOI Media Attached |
23:00 - 00:20: R-3OOPSLA at SPLASH-I Chair(s): Pranav KantUniversity of Utah, Xiangzhe XuNanjing University | |||
23:00 - 23:20 Talk | Compiling Symbolic Execution with Staging and Algebraic Effects OOPSLA Guannan WeiPurdue University, Oliver BračevacPurdue University, Shangyin TanPurdue University, Tiark RompfPurdue University Link to publication DOI Pre-print Media Attached | ||
23:20 - 23:40 Talk | Projection-Based Runtime Assertions for Testing and Debugging Quantum Programs OOPSLA Gushu LiUniversity of California at Santa Barbara, Li ZhouMax Planck Institute for Security and Privacy, Nengkun YuUniversity of Technology Sydney, Yufei DingUniversity of California at Santa Barbara, Mingsheng YingUniversity of Technology Sydney / Institute of Software at Chinese Academy of Sciences / Tsinghua University, Yuan XieUniversity of California at Santa Barbara Link to publication DOI Pre-print Media Attached | ||
23:40 - 00:00 Talk | Satune: Synthesizing Efficient SAT Encoders OOPSLA Hamed GorjiaraUniversity of California at Irvine, Guoqing Harry XuUniversity of California at Los Angeles, Brian DemskyUniversity of California at Irvine Link to publication DOI Media Attached | ||
00:00 - 00:20 Talk | The Anchor Verifier for Blocking and Non-blocking Concurrent Software OOPSLA Link to publication DOI Media Attached |