Fahiem's reading group

Choosing the next paper

Erin:

Explaining flow-based propagation. Nicholas Downing, Thibaut Feydy, and Peter J. Stuckey. CPAIOR'12

Propagation via Lazy Clause Generation. Olga Ohrimenko, Peter J. Stuckey, and Michael Codish. Constraints.

Ozan:

New Clause Learning Scheme for Efficient Unsatisfiability Proofs. AAAI '08

Lazy Explanations for Constraint Propagators. Ian P. Gent, Ian Miguel, Neil C.A. Moore. PADL'10

SDD: A New Canonical Representation of Propositional Knowledge Bases

Paper List

Sept 29:	Discussion led by Jessica, on the following paper: Ian P. Gent, Chris Jefferson, Ian Miguel, and Peter Nightingale, Generating Special-purpose Stateless Propagators for Arbitrary Constraints, CP 2010.
Oct 06:	Discussion led by Fahiem, on the following paper Blai Bonet and Malte Helmert, Strengthening Landmark Heuristics via Hitting Sets, ECAI 2010.
Oct 13:	Discussion led by Alexandra, on the following paper: Robinson, N., Gretton, C.; Pham, D. N.; and Sattar, A, Partial Weighted MaxSAT for Optimal Planning. To Appear: Proceedings of the 11th Pacific Rim International Conference on Artificial Intelligence, 2010.
Oct 20:	Discussion led by Ozan, on the following paper: Ruben Duarte Viegas, Marco Correia, Pedro Barahona and Francisco Azevedo Using Indexed Finite Set Variables for Set Bounds Propagation. Sixth Ibero-American Artificial Intelligence Conference (IBERAMIA.08), 2008.
Oct 27:	Discussion led by Christian, on the following paper: Knot Pipatsrisawat and Adnan Darwiche Top-Down Algorithms for Constructing Structured DNNF: Theoretical and Practical Implications. ECAI-10, Lisbon, Portugal
Nov 10:	Discussion led by Erin, on the following paper: Hubie Chen, A Rendezvous of Logic, Complexity, and Algebra, ACM Computing Surveys (CSUR) Volume 42 , Issue 1 (December 2009)
Nov 24:	Continuing discussion on the following paper: Hubie Chen, A Rendezvous of Logic, Complexity, and Algebra, ACM Computing Surveys (CSUR) Volume 42 , Issue 1 (December 2009)
Dec 8:	Discussion on the following paper: Niklas Eén and Niklas Sörensson, Translating Pseudo-Boolean Constraints into SAT Journal on Satisfiability, Boolean Modeling and Computation (2006) Christian presents Method 1: 5.3 Translation through BDDs Erin presents Method 2: 5.4 Translation through Adder Networks Eric presents Method 3: 5.5 Translation through Sorting Networks
Feb 09:	Discussion led by Fahiem, on the following paper: Peter Jeavons and Justyna Petke, Local consistency and SAT-solvers CP 2010. Vol. 6308 of Lecture Notes in Computer Science. Pages 398-413.
Feb 16:	Discussion led by Jessica, on the following paper: An Efficient Branch-and-Bound Algorithm Based on MaxSAT for the Maximum Clique Problem. Li, C., Quan, Z. AAAI 2010.
Feb 23:	Discussion led by Erin, on the following paper: Propagating Conjunctions of AllDifferent Constraints. Bessiere C., Katsirelos G., Narodytska N., Quimper C.G., and Walsh T. AAAI 2010
Mar 2:	Discussion led by Alexandra, on the following paper: Decompositions of All Different, Global Cardinality and Related Constraints. Bessiere C., Katsirelos G., Narodytska N., Quimper C.G., and Walsh T. IJCAI 2009
Mar 9:	Discussion led by Ozan, on the following paper: Symmetries of Symmetry Breaking Constraints. George Katsirelos and Toby Walsh. Proceedings of ECAI-2010, 2010.
Mar 16:	Discussion led by Jessica, on the following paper: Upper Bounds on the Number of Solutions of Binary Integer Programs. Jain, S., Kadioglu, S., Sellmann, M. CPAIOR 2010.
Mar 23:	Discussion led by Alexandra, on the following paper: Improved Local Search for Circuit Satisfiability. A. Belov and Z.Stachniak. Proceedings of SAT 2010
Mar 30:	Discussion led by Erin, on the following paper: A New Hybrid Tractable Class of Soft Constraint Problems. Martin C. Cooper and Stanislav Zivny. Proceedings of CP 2010
Apr 6:	Discussion led by Ozan, on the following paper: A Simplifier for Propositional Formulas with Many Binary Clauses. Ronen I. Brafman. IJCAI'01
Apr 13:	Discussion led by Erin, on the following paper: Automatically Exploiting Subproblem Equivalence in Constraint Programming. G. Chu, M. Garcia de la Banda, and P.J. Stuckey. CPAIOR 2010
Apr 20:	Discussion led by Alexandra, on the following paper: Learning in Local Search. Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, and Lakhdar Sais. ICTAI 2009
May 4:	Discussion led by Jessica, on the following paper: Automatically Configuring Algorithms for Portfolio-Based Selection by Lin Xu, Holger Hoos and Kevin Leyton-Brown, AAAI 2010.
May 25:	Discussion led by Ozan, on the following paper: Symmetry and Satisfiability: An Update. Hadi Katebi, Karem A. Sakallah, Igor L. Markov. SAT 2010
June 1:	Discussion led by Alexandra, on the following paper: Interpolation and SAT-based Model Checking. K. L. McMillan. CAV 2003.
June 8:	Discussion led by Erin, on the following paper: Maintaining State in Propagation Solvers. Raphael M. Reischuk, Christian Schulte, Peter J. Stuckey, Guido Tack. CP'09
June 22:	Discussion led by Jessica, on the following paper: Efficient CNF Simplification based on Binary Implication Graphs. Marijn Heule, Matti Jarvisalo, and Armin Biere. SAT'11
July 05:	SAT'2011 and ICAPS'2011 overviews
July 12:	Discussion led by Ozan, on the following paper: Heuristics for Planning with SAT and Expressive Action Definitions. Jussi Rintanen. ICAPS'11
July 27:	IJCAI'2011 overview
Aug 3:	Discussion led by Fahiem, on the following paper: Planning as Satisfiability with Relaxed ࢛-Step Plans. Martin Wehrle and Jussi Rintanen. AI'07

Sept 27:	CP'11 overview
Oct 4:	Discussion led by Fahiem, on the following paper: Circuit Complexity and Decompositions of Global Constraints. Christian Bessiere, George Katsirelos, Nina Narodytska, Toby Walsh. IJCAI'09
Oct 12:	Continuing discussion on the following paper: Circuit Complexity and Decompositions of Global Constraints. Christian Bessiere, George Katsirelos, Nina Narodytska, Toby Walsh. IJCAI'09
Oct 18:	Discussion led by Alexandra, on the following paper: Kangaroo: An Efficient Constraint-Based Local Search System Using Lazy Propagation. M.A.Hakim Newton, Duc-Nghia Pham, Abdul Sattar and Michael Maher. CP 2011
Oct 25:	Discussion led by Erin, on the following paper: Synthesis of Search Algorithms from High-level CP Models. Samir A. Mohamed Elsayed, Laurent Michel. CP 2011
Dec 6:	Discussion led by Jessica, on the following paper: Lifted Probabilistic Inference by First-Order Knowledge Compilation. Guy Van den Broeck, Nima Taghipour, Wannes Meert, Jesse Davis, Luc De Raedt. IJCAI 2011
Dec 13:	Discussion led by Ozan, on the following paper: Directed Search for Generalized Plans Using Classical Planners. Siddharth Srivastava, Neil Immerman, Shlomo Zilberstein, Tianjiao Zhang. ICAPS'11
Feb 14:	Discussion led by Erin, on the following paper: Automatic Generation of Constraints for Partial Symmetry Breaking. Christopher Jefferson and Karen E. Petrie. CP'11
Feb 21:	Discussion led by Lei, on the following paper: Planning with SAT, Admissible Heuristics and A*
Feb 28:	Discussion led by Ozan, on the following paper: A Lightweight Component Caching Scheme for Satisfiability Solvers (extended version). SAT '07
Mar 6:	Discussion led by Erin, on the following paper: Virtual Arc Consistency for Weighted CSP. AAAI '08
Mar 13:	Discussion led by Ozan, on the following paper: DPLL(T): Fast Decision Procedures. CAV 2004
Mar 20:	Discussion led by Jessica, on the following paper: Manipulating MDD Relaxations for Combinatorial Optimization. David Bergman, Willem-Jan van Hoeve, J. N. Hooker. CPAIOR 2011
Apr 3:	Discussion led by Lei, on the following paper: Computing Equivalent Transformations for Combinatorial Optimization by Branch-and-Bound Search. Eric I. Hsu and Sheila A. McIlraith. SoCS 2010
Apr 10:	Discussion led by Erin, on the following paper: Russian Doll Search with Tree Decomposition. Martí Sánchez, David Allouche, Simon de Givry. IJCAI 2009
Apr 17:	Discussion led by Ozan, on the following paper: DPLL(T) with Exhaustive Theory Propagation and its Application to Difference Logic. Robert Nieuwenhuis, Albert Oliveras. CAV'05
May 8:	Discussion led by Jessica, on the following paper: Using Hard Constraints for Representing Soft Constraints, Jean-Charles Regin, CPAIOR 2011
May 17:	Discussion led by Alexandra, on the following paper: Blocked Clause Elimination. M. Järvisalo, A. Biere, M. Heule. TACAS'10
May 31:	Discussion led by Lei, on the following paper: Monte-Carlo Style UCT Search for Boolean Satisfiability. Alessandro Previti, Raghuram Ramanujan, Marco Schaerf, Bart Selman. AI*IA 2012
Jun 7:	Discussion led by Ozan, on the following paper: Lazy Clause Generation Reengineered. Thibaut Feydy, Peter J. Stuckey. CP '09
June 26:	Discussion led by Alexandra, on the following paper: Solving QBF with Counterexample Guided Refinement. Mikolas Janota, William Klieber, Joao Marques-Silva, and Edmund Clarke. SAT'2012

Sep 19:	Simplified and improved resolution lower bounds. Paul Beame, Toniann Pitassi. FOCS '96
Sep 26:	Discussion led by Alexandra, on the following paper: The Complexity of Resolution Refinements. Joshua Buresh-Oppenheim, Toniann Pitassi. The Journal of Symbolic Logic 2007.
Oct 17:	Discussion led by Fahiem, on the following paper: The Intractability of Resolution. Armin Haken. Theoretical Computer Science, Volume 39, 1985, Pages 297--308
Oct 24:	CP 2012 OVerview
Oct 31:	Discussion led by Erin, on the following papers: Eigenvector Centrality in Industrial SAT Instances. George Katsirelos, Laurent Simon. CP 2012: 348-356. Refining Restarts Strategies for SAT and UNSAT. Gilles Audemard and Laurent Simon. CP 2012:118-126.
Nov 7:	Discussion led by Ozan, on the following paper: Relating Proof Complexity Measures and Practical Hardness of SAT. Matti Järvisalo, Arie Matsliah, Jakob Nordström and Stanislav Zivny. CP 2012
Nov 21:	Discussion led by Alexandra, on the following paper: Contributions to the Theory of Practical Quantified Boolean Formula Solving. Allen Van Gelder. CP 2012
Nov 28:	Discussion led by Erin, on the following paper: Conflict Directed Lazy Decomposition. Ignasi Abio, Peter J. Stuckey. CP 2012
Dec 5:	Discussion led by Fahiem, on the following paper: Accelerating MUS Extraction with Recursive Model Rotation. Anton Belov, Joao Marquez-Silva. FMCAD 2011

Jan 27:	Discussion led by Fahiem, on the following paper: SAT-based Preprocessing for MaxSAT. Anton Belov, Antonio Morgado, Joao Marquez-Silva. LPAR 2013
Feb 03:	Discussion led by Ozan, on the following paper: To Encode or to Propagate? The Best Choice for Each Constraint in SAT. Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Peter J. Stuckey. CP 2013.
Feb 10:	Discussion led by Fahiem, on the following paper: Inprocessing Rules. Matti Järvisalo, Marijn Heule, Armin Biere. IJCAR 2012.
Feb 24:	Discussion led by Ozan, on the following paper: Semantic Learning for Lazy Clause Generation. Thibaut Feydy, Andreas Schutt, Peter Stuckey. CP 2013.
Mar 3:	Discussion led by Nina, on the following paper: Automated Reencoding of Boolean Formulas. Norbert Manthey, Marijn Heule, Armin Biere. HVC2012.
Mar 17:	Discussion led by Nina, on the following paper: Preprocessing in Incremental SAT. Alexander Nadel, Vadim Ryvchin, Ofer Strichman. SAT 2012.
Mar 24:	Discussion led by Erin, on the following paper: Extended Resolution Proofs for Conjoining BDDs. Carsten Sinz and Armin Biere. CSR06.
Apr 7:	Discussion led by Fahiem, on the following paper: A Restriction of Extended Resolution for Clause Learning SAT Solvers. Gilles Audemard, George Katsirelos, Laurent Simon. AAAI 2010.
Apr 21:	Discussion led by Fahiem, on the following paper: Verifying Refutations with Extended Resolution. Marijn J. H. Heule, Warren A. Hunt Jr., Nathan Wetzler. CADE-24.
Apr 28:	Discussion led by Fahiem, on the following paper: DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt, Jr. SAT 2014.
May 05:	Discussion led by Nina, on the following paper: On Improving MUS Extraction Algorithms. Joao Marques-Silva and Ines Lynce. SAT 2011.
May 12:	Discussion led by Ozan, on the following paper: Structure Based Extended Resolution for Constraint Programming. Geoffrey Chu, Peter J. Stuckey.
May 26:	Discussion led by Fahiem, on the following paper: Minimum Satisfying Assignments for SMT. I. Dillig, T. Dillig, K. McMillan and A. Aiken. CAV 2012.
Jun 2:	Discussion led by Ozan, on the following paper: Lazy Annotation Revisited. Kenneth L. McMillan. Technical Report, 2014.
Jun 16:	Discussion led by Erın, on the following paper: Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask). Tomas Balyo, Andreas Frohlich, Marijn Heule and Armin Biere. SAT 2014.