	A	B	C	D	E	G
1
2		Topic Name	Papers			Presenter
3
4	1	SAT & Proof Complexity	Narrow Proofs May Be Maximally Long	Albert Atserias, Massimo Lauria, Jakob Nordström	ACM Trans. Comput. Log. 17(3): 19 (2016)
5			On the interplay between proof complexity and SAT solving	Jakob Nordström	SIGLOG News 2(3): 19-44 (2015)
6
7	2	Proof Systems for QBF	Expansion-based QBF solving versus Q-resolution	Mikolás Janota, Joao Marques-Silva	Theor. Comput. Sci. 577: 25-42 (2015)
8			On Unification of QBF Resolution-Based Calculi	Olaf Beyersdorff, Leroy Chew, Mikolas Janota	MFCS (2) 2014: 81-93
9
10	3	Autarkies	Computing Maximal Autarkies with Few and Simple Oracle Queries	Oliver Kullmann, Joao Marques-Silva	SAT 2015: 138-155
11			Minimal Unsatisfiability and Autarkies	Hans Kleine Büning, Oliver Kullmann	Handbook of Satisfiability 2009: 339-401
12
13	4	Symbolic Execution	SAGE: whitebox fuzzing for security testing	Patrice Godefroid, Michael Y. Levin, David A. Molnar	Commun. ACM 55(3): 40-44 (2012)
14			KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs.	Cristian Cadar, Daniel Dunbar, Dawson R. Engler	OSDI 2008: 209-224
15
16	5	Hyper Binary Resolution	Enhancing Davis Putnam with Extended Binary Clause Reasoning	Fahiem Bacchus	AAAI/IAAI 2002: 613-619
17			Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas	Roman Gershman, Ofer Strichman	SAT 2005: 423-429
18			Revisiting Hyper Binary Resolution	Marijn Heule, Matti Järvisalo, Armin Biere	CPAIOR 2013: 77-93
19
20	6	Clause Removal Procedures	Clause Elimination for SAT and QSAT	Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, Armin Biere	J. Artif. Intell. Res. (JAIR) 53: 127-168 (2015)
21			Simulating Circuit-Level Simplifications on CNF	Matti Järvisalo, Armin Biere, Marijn Heule	J. Autom. Reasoning 49(4): 583-619 (2012)
22
23	7	Encoding	Applying Logic Synthesis for Speeding Up SAT	Niklas Eén, Alan Mishchenko, Niklas Sörensson
24			Efficient Circuit to CNF Conversion	Panagiotis Manolios, Daron Vroon	SAT 2007: 4-9
25
26	8	On-The-Fly Subsumption	On-the-Fly Clause Improvement	HyoJung Han, Fabio Somenzi	SAT 2009: 209-222
27			Learning for Dynamic Subsumption	Youssef Hamadi, Saïd Jabbour, Lakhdar Sais	International Journal on Artificial Intelligence Tools 19(4): 511-529 (2010)
28
29	9	Bit-Blasting	?
30
31	10	Bounded Variable Elimination + Addition	Automated Reencoding of Boolean Formulas	Norbert Manthey, Marijn Heule, Armin Biere	Haifa Verification Conference 2012: 102-117
32			Effective Preprocessing in SAT Through Variable and Clause Elimination	Niklas Eén, Armin Biere	SAT 2005: 61-75
33
34	11	Minimization	Recording and Minimizing Nogoods from Restarts	Christophe Lecoutre, Lakhdar Sais, Sébastien Tabary, Vincent Vidal	JSAT 1(3-4): 147-167 (2007)
35			Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces	Allen Van Gelder	SAT 2009: 141-146
36
37	12	Proofs	Proofs for Satisfiability Problems	Marijn Heule, Armin Biere
38
39	13	Symmetry Breaking	Improved Static Symmetry Breaking for SAT	Jo Devriendt, Bart Bogaerts, Maurice Bruynooghe, Marc Denecker	SAT 2016: 104-122
40			Expressing Symmetry Breaking in DRAT Proofs.	Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler	CADE 2015: 591-606
41
42	14	Watched Literals	Chaff: Engineering an Efficient SAT Solver.	Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik	DAC 2001
43			Implementing the Davis-Putnam Method	Hantao Zhang, Mark E. Stickel	J. Autom. Reasoning 24(1/2): 277-296 (2000)
44			Optimal Implementation of Watched Literals and More General Techniques.	Ian P. Gent	J. Artif. Intell. Res. (JAIR) 48: 231-251 (2013)
45
46	15	Portfolio Solving	A Concurrent Portfolio Approach to SMT Solving	Christoph M. Wintersteiger, Youssef Hamadi, Leonardo Mendonça de Moura	CAV 2009: 715-720
47			SATzilla: Portfolio-based Algorithm Selection for SAT	Lin Xu, Frank Hutter, Holger H. Hoos, Kevin Leyton-Brown	J. Artif. Intell. Res. (JAIR) 32: 565-606 (2008)
48					2007
49	16	Lookahead Solving	March_eq: Implementing Additional Reasoning into an Efficient Look-Ahead SAT Solver	Marijn Heule, Mark Dufour, Joris van Zwieten, Hans van Maaren	SAT 2004: 345-359
50			Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads	Marijn Heule, Oliver Kullmann, Siert Wieringa, Armin Biere	Haifa Verification Conference 2011: 50-65
51
52	17	Local Search	Choosing Probability Distributions for Stochastic Local Search and the Role of Make versus Break	Adrian Balint, Uwe Schöning	SAT 2012: 16-29
53			http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.21.2207&rep=rep1&type=pdf	Bart Selman, Henry A. Kautz, Bram Cohen	Cliques, Coloring, and Satisfiability 1993: 521-532