Editors: Christoph M. Wintersteiger and Olaf Beyersdorff

Marijn HeuleComputable Short ProofsJul 11 11:00
Christoph Scholl and Ralf WimmerDependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications
Rahul SanthanamModelling SAT
Rüdiger Ehlers and Francisco Palau RomeroApproximately Propagation Complete and Conflict Propagating Constraint EncodingsJul 09 14:00
Tobias Paxian, Sven Reimer and Bernd BeckerDynamic Polynomial Watchdog Encoding for Solving Weighted MaxSATJul 09 14:30
Alexander NadelSolving MaxSAT with Bit-Vector OptimizationJul 09 15:00
Jan Elffers, Jesus Giráldez-Cru, Jakob Nordstrom and Marc VinyalsUsing Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean SolversJul 09 16:00
Jia Liang, Chanseok Oh, Minu Mathews, Ciza Thomas, Chunxiao Li and Vijay GaneshMachine Learning-based Restart Policy for CDCL SAT SolversJul 09 16:30
Vadim Ryvchin and Alexander NadelChronological BacktrackingJul 09 17:00
Sima Jamali and David MitchellCentrality-Based Improvements to CDCL HeuristicsJul 09 17:30
Dimitris Achlioptas, Zayd Hammoudeh and Panos TheodoropoulosFast Sampling of Perfectly Uniform Satisfying AssignmentsJul 10 09:00
Dimitris Achlioptas, Zayd Hammoudeh and Panos TheodoropoulosFast and Flexible Probabilistic Model CountingJul 10 09:30
Johannes K. Fichte, Markus Hecher, Michael Morak and Stefan WoltranExploiting Treewidth for Projected Model Counting and its LimitsJul 10 10:00
Mikolas JanotaCircuit-based Search Space Pruning in QBFJul 10 14:00
Manuel Kauers and Martina SeidlSymmetries for QBFJul 10 14:30
Martin Suda and Bernhard GleissLocal Soundness for QBF CalculiJul 10 15:00
Michael Lampis, Stefan Mengel and Valia MitsouQBF as an Alternative to Courcelle's TheoremJul 10 16:00
Tomáš Peitl, Friedrich Slivovsky and Stefan SzeiderPolynomial-Time Validation of QCDCL CertificatesJul 10 16:30
Tobias Friedrich and Ralf RothenbergerSharpness of the Satisfiability Threshold for Non-Uniform Random k-SATJul 11 09:00
Marc Vinyals, Jan Elffers, Jesús Giráldez-Crú, Stephan Gocht and Jakob NordstromIn Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT SolvingJul 11 09:30
Nicola Galesi, Navid Talebanfard and Jacobo ToranCops-Robber games and the resolution of Tseitin formulasJul 11 10:00
Hoda Abbasizanjani and Oliver KullmannMinimal unsatisfiability and minimal strongly connected digraphsJul 11 16:00
Ryan Berryhill, Alexander Ivrii and Andreas VenerisFinding all Minimal Safe Inductive SetsJul 11 16:30
Shubhani Gupta, Aseem Saxena, Anmol Mahajan and Sorav BansalEffective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query DecompositionJul 12 11:00
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri and Roberto SebastianiExperimenting on Solving Nonlinear Integer Arithmetic with Incremental LinearizationJul 12 11:30
Sean Weaver, Hannah Roberts and Michael SmithXORSAT Set Membership FiltersJul 12 12:00
Stepan Kochemazov and Oleg ZaikinALIAS: A Modular Tool for Finding Backdoors for SATJul 12 14:00
Alexey Ignatiev, Antonio Morgado and Joao Marques-SilvaPySAT: A Python Toolkit for Prototyping with SAT OraclesJul 12 14:30
Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj Bjorner and Mooly SagivConstrained Image Generation Using Binarized Neural Networks with Decision ProceduresJul 12 15:00