team
contact
software
publications
teaching
jobs

Ringvorlesung Doktoratskolleg LogiCS

February 2021

News

Overview

This page mainly provides resources for our two hour lecture given in the Ringvorlesung of our Doktoratskolleg Logic in Computer Science (LogiCS).

The slides of the lecture: slides.pdf

Modified MiniSAT code with failed literal stubs for the exercise: minisat-failed-literal-exercise.zip

MiniSAT code on github: https://github.com/niklasso/minisat

Our SAT solvers: PicoSAT, Lingeling, Cleaneling. CaDiCaL.

Extended version SAT Solving of this lecture.

Tutorial
SAT-Solving
Satisfiability: Theory, Practice, and Beyond Boot Camp
Satisfiability: Theory, Practice, and Beyond Program
Simons Institute for the Theory of Computing
Cyberspace, February 2, 2021
[ pre-recorded intro on YouTube (4h22) | local copy of pre-recorded video (4h22) | live recording on YouTube (2h02) | code ]

Tutorial
SAT
5th Indian SAT + SMT Winter School
Cyberspace, December 11, 2020
[ slides | video 1 | video 2 | video 3 ]

Tutorial
SAT in Master Class
Recent Advances in Optimisation Paradigms and Solving Technology
17th Intl. Conf. on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR'20)
Cyberspace, September 21, 2020
[ slides | video ]

Tutorial
Conflict-Driven Clause Learning
Intl. Symp. on Automated Technology for Verification and Analysis (ATVA'19)
Taipei, Taiwan, Oct. 28, 2019

Tutorial on Modern SAT Solving
Logic Synthesis Software School
EPFL Lausanne, Switzerland, June 20, 2019.

Encoding into SAT
SAT/SMT/AR Summer School 2018
International Summer School on Satisfiability, Satisfiability Modulo Theories, and Automated Reasoning
Manchester, UK, July 2018.
[ satsmtar18satexercises.tar.gz | satsmtar18satsolutions.tar.gz ]
[ satsmtar18satexercises.zip | satsmtar18satsolutions.zip ]

Searching, Simplifying, Proving A Tutorial on Modern SAT Solving
European Joint Conferences on Theory and Practice of Software (ETAPS'18)
Thesaloniki, Greece, April 2018.

Conflict-Driven Clause Learning
SAT/SMT/AR Summer School 2019
Lisbon, Portugal, July 4, 2019.

Tutorial
Conflict-Driven Clause Learning
Intl. Symp. on Automated Technology for Verification and Analysis (ATVA'19)
Taipei, Taiwan, Oct. 28, 2019.

Invited
Tutorial on SAT
joint CP'17, ICLP'17, and SAT'17
Melbourne, Australia, August 2017.

Two related SAT talks at SAT'15 and POS'15:

Evaluating CDCL Variable Scoring Schemes.
18th Intl. Conf. on Theory and Applications of Satisfiability (SAT'15),
Austin, TX, USA,
Sept. 2015.

Evaluating CDCL Restart Schemes.
6th Workshop on Pragmatics of SAT (POS'15),
SAT 2015, Austin, TX, USA,
Sept. 2015.

Some recent tutorial talks on SAT:

Encoding into SAT
SAT/SMT/AR Summer School 2018
International Summer School on Satisfiability, Satisfiability Modulo Theories, and Automated Reasoning
Manchester, UK, July 2018.
[ satsmtar18satexercises.tar.gz | satsmtar18satsolutions.tar.gz ]
[ satsmtar18satexercises.zip | satsmtar18satsolutions.zip ]

Searching, Simplifying, Proving A Tutorial on Modern SAT Solving
European Joint Conferences on Theory and Practice of Software (ETAPS'18)
Thesaloniki, Greece, April 2018.

Invited
Tutorial on SAT
joint CP'17, ICLP'17, and SAT'17
Melbourne, Australia, August 2017.

Related talk at the SAT/SMT 2012 summer school in Trento:

Modern CDCL SAT Solvers,
Second Intl. SAT / SMT Summer School 2012,
Trento, Italy,
June 2012.

Related talk at the 2014 Banff Workshop in Canada:

Where does SAT not work? (video)
Workshop on Theoretical Foundations of Applied SAT Solving.
Banff International Research Station for Mathematical Innovation and Discovery.
related CACM editorial on this workshop,
Banff, Canada.
20 January 2014.