Abstract is missing.
- Parameterized Compilation Lower Bounds for Restricted CNF-FormulasStefan Mengel. 3-12 [doi]
- Satisfiability via Smooth PicturesMateus de Oliveira Oliveira. 13-28 [doi]
- Solution-Graphs of Boolean Formulas and IsomorphismPatrick Scharpfenecker, Jacobo Torán. 29-44 [doi]
- Strong Backdoors for Default LogicJohannes Klaus Fichte, Arne Meier, Irina Schindler. 45-59 [doi]
- The Normalized Autocorrelation Length of Random Max r -Sat Converges in Probability to (1-1/2^r)/rDaniel Berend, Yochai Twitto. 60-76 [doi]
- Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole PrincipleVsevolod Oparin. 77-84 [doi]
- Extreme Cases in SAT ProblemsGilles Audemard, Laurent Simon. 87-103 [doi]
- Improved Static Symmetry Breaking for SATJo Devriendt, Bart Bogaerts 0001, Maurice Bruynooghe, Marc Denecker. 104-122 [doi]
- Learning Rate Based Branching Heuristic for SAT SolversJia Hui Liang, Vijay Ganesh, Pascal Poupart, Krzysztof Czarnecki. 123-140 [doi]
- On the Hardness of SAT with Community StructureNathan Mull, Daniel J. Fremont, Sanjit A. Seshia. 141-159 [doi]
- Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT SolversJan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard, Jakob Nordström, Marc Vinyals. 160-176 [doi]
- A SAT Approach to BranchwidthNeha Lodha, Sebastian Ordyniak, Stefan Szeider. 179-195 [doi]
- Computing Maximum Unavoidable Subgraphs Using SAT SolversC. K. Cuong, M. J. H. Heule. 196-211 [doi]
- Heuristic NPN Classification for Large Functions Using AIGs and LEXSATMathias Soeken, Alan Mishchenko, Ana Petkovska, Baruch Sterin, Paolo Ienne, Robert K. Brayton, Giovanni De Micheli. 212-227 [doi]
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-ConquerMarijn J. H. Heule, Oliver Kullmann, Victor W. Marek. 228-245 [doi]
- Deciding Bit-Vector Formulas with mcSATAleksandar Zeljic, Christoph M. Wintersteiger, Philipp Rümmer. 249-266 [doi]
- Solving Quantified Bit-Vector Formulas Using Binary Decision DiagramsMartin Jonás, Jan Strejcek. 267-283 [doi]
- Speeding up the Constraint-Based Method in Difference LogicLorenzo Candeago, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio. 284-301 [doi]
- Synthesis of Domain Specific CNF Encoders for Bit-Vector SolversJeevana Priya Inala, Rohit Singh 0002, Armando Solar-Lezama. 302-320 [doi]
- Finding Finite Models in Multi-sorted First-Order LogicGiles Reger, Martin Suda 0001, Andrei Voronkov. 323-341 [doi]
- MCS Extraction with Sublinear Oracle QueriesCarlos Mencía, Alexey Ignatiev, Alessandro Previti, Joao Marques-Silva. 342-360 [doi]
- Predicate Elimination for Preprocessing in First-Order Theorem ProvingZurab Khasidashvili, Konstantin Korovin. 361-372 [doi]
- Incremental DeterminizationMarkus N. Rabe, Sanjit A. Seshia. 375-392 [doi]
- Non-prenex QBF Solving Using AbstractionLeander Tentrup. 393-401 [doi]
- On Q-Resolution and CDCL QBF SolvingMikolás Janota. 402-418 [doi]
- On Stronger Calculi for QBFsUwe Egly. 419-434 [doi]
- Q-Resolution with Generalized AxiomsFlorian Lonsing, Uwe Egly, Martina Seidl. 435-452 [doi]
- 2QBF: Challenges and SolutionsValeriy Balabanov, Jie-Hong Roland Jiang, Christoph Scholl, Alan Mishchenko, Robert K. Brayton. 453-469 [doi]
- Dependency Schemes for DQBFRalf Wimmer, Christoph Scholl, Karina Wimmer, Bernd Becker. 473-489 [doi]
- Lifting QBF Resolution Calculi to DQBFOlaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda 0001. 490-499 [doi]
- Long Distance Q-Resolution with Dependency SchemesTomás Peitl, Friedrich Slivovsky, Stefan Szeider. 500-518 [doi]
- EL^+ OntologiesM. Fareed Arif, Carlos Mencía, Alexey Ignatiev, Norbert Manthey, Rafael Peñaloza, Joao Marques-Silva. 521-530 [doi]
- HordeQBF: A Modular and Massively Parallel QBF SolverTomas Balyo, Florian Lonsing. 531-538 [doi]
- LMHS: A SAT-IP Hybrid MaxSAT SolverPaul Saikko, Jeremias Berg, Matti Järvisalo. 539-546 [doi]
- OpenSMT2: An SMT Solver for Multi-core and Cloud ComputingAntti E. J. Hyvärinen, Matteo Marescotti, Leonardo Alt, Natasha Sharygina. 547-553 [doi]
- SpyBug: Automated Bug Detection in the Configuration Space of SAT SolversNorbert Manthey, Marius Lindauer. 554-561 [doi]