Towards a theory of good SAT representations

Publications

• Generalising unit-refutation completeness and SLUR via nested input resolution - Arxiv report
• Towards a better understanding of hardness - CP 2011 (Doctoral Program) - Perugia [PDF]
• Towards a better understanding of SAT translations - LCC 2011 - Toronto [PDF]

Presentations

• Towards a Theory of Good SAT Representations - Computer Science Seminar - Computer Science Department of Leicester (May 2012) [slides]
• SAT Solving: Present and Future (in two vignettes) - Logical Approaches to Barriers in Complexity II - Isaac Newton Institute for Mathematical Sciences, Cambridge, UK [slides]
• Towards a better understanding of SAT translations (From Hardness to Softness) - BIRS 2011 - Banff [slides].
• Towards a better understanding of SAT-hardness: Constructing soft SAT-representations of boolean functions, with applications to AES+DES - CP 2011 (Doctoral Program) - Perugia [slides].
• Towards a better understanding of SAT translations - LCC 2011 - Toronto [slides]
• How to translate into SAT such that SAT solvers have a good time?! - Fourth Workshop on Formal and Automated Theorem Proving and Applications (Feb 2011) - Belgrade [slides]

Benchmarks

• AES Benchmarks II - SAT Challenge 2012 (benchmarks, documentation [PDF]).
• The AES Challenge - SAT Competition 2011 (benchmarks, documentation).
• Advanced Encryption Standard I Benchmarks - SAT Competition 2011 (benchmarks, documentation).
• Advanced Encryption Standard component benchmarks (MaxSAT) - Max-SAT 2011 (benchmarks, results, documentation).
• Advanced Encryption Standard component benchmarks (pseudo-boolean) - Pseudo-Boolean Competition 2011 (benchmarks, results, documentation).

Data

• Experimental data is available within the OKlibrary.
• Statistics for each experiment are available in a repository on GitHub.

Contacts

• Matthew Gwynne
• Oliver Kullmann