Skip to content

Commit c7d00d0

Browse files
k-sidorovk-sidorov
authored
Uploaded Season 1 session descriptions
1 parent 50a0169 commit c7d00d0

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

49 files changed

+491
-0
lines changed

‎_sessions/2023-05-22-auditable-cp.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,5 @@ host_ref: https://ksidorov.nl
66
session_type: paper
77
related_papers: s20230522
88
---
9+
10+
The very first reading group session, in which I reviewed an approach for integrating constraint programming solving with VeriPB proof logging workflow.

‎_sessions/2023-05-30-general-constraints.md‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
---
2+
layout: session
3+
title: Learning general constraints in csp
4+
host: Maarten Flippo
5+
host_ref: https://maartenflippo.com
6+
session_type: paper
7+
related_papers: s20230530
8+
---
9+
10+
In this session, Maarten will tell us more about constraint learning in constraint programming that goes beyond clausal/PB constraints.

‎_sessions/2023-06-05-smt.md‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
---
2+
layout: session
3+
title: A tour of SMT proof logging
4+
host: Konstantin Sidorov
5+
host_ref: https://ksidorov.nl
6+
session_type: tour
7+
---
8+
9+
An overview of techniques for solving Satisfiability Modulo Theory problems and logging
10+
the solver decisions.

‎_sessions/2023-06-12-vrp-column-generation.md‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
---
2+
layout: session
3+
title: Column generation for real-time ride-sharing operations
4+
host: Elif Arslan
5+
session_type: paper
6+
related_papers: s20230612
7+
---
8+
9+
In this meeting, we discussed the column generation method in application to real-time ride-sharing operations.

‎_sessions/2023-06-20-vipr.md‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
---
2+
layout: session
3+
title: Optimality certificates, MIP style
4+
host: Konstantin Sidorov
5+
host_ref: https://ksidorov.nl
6+
session_type: paper
7+
related_papers: s20230620
8+
---
9+
10+
An overview of techniques for solving Satisfiability Modulo Theory problems and logging
11+
the solver decisions.
12+

‎_sessions/2023-08-21-unsat-proofs.md‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
---
2+
layout: session
3+
title: A tour of SAT proof logging
4+
host: Konstantin Sidorov
5+
host_ref: https://ksidorov.nl
6+
session_type: tour
7+
---
8+
9+
A follow-up of the SMT proof logging session; in this session, I motivate the proof logging on an example from [Schur Number Five](https://arxiv.org/abs/1711.08076) and introduced the basic ideas behind the clausal proofs.

‎_sessions/2023-08-28-gourd.md‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
---
2+
layout: session
3+
title: "Gourd-Test: testing Pumpkin and beyond"
4+
host: Jeff Smits
5+
host_ref: https://www.jeffsmits.net/
6+
session_type: research
7+
---
8+
9+
In this session I'll introduce the evaluation tool I've been developing for Pumpkin and other SAT-like solvers, with the idea that we might be able to generalise to other tools. I'll summarise the plans we've made, what I'm using for inspiration, the technology used, how far I've gotten, and finish with a little demo.

‎_sessions/2023-09-04-disjunctive.md‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
---
2+
layout: session
3+
title: Enhancing Hybrid CP-SAT Search for Disjunctive Scheduling
4+
host: Maarten Flippo
5+
host_ref: https://maartenflippo.com
6+
session_type: paper
7+
related_papers: s20230904
8+
---
9+
10+
Disjunctive scheduling problems such as the job shop and open shop are at the heart of many real world scheduling instances. In this paper, we frame such problems as disjunctive temporal networks associated with a makespan minimization objective. For those, we propose a hybrid approach between SAT/SMT and CP solvers. In particular, we keep from SMT solvers the aggregated constraint propagation in decision procedures as well as the explanations and clause learning mechanisms upon conflict. However, like all CP solvers, we maintain an explicit domain representation of integer variables, tightly integrated with clause learning. Automated search exploits explanations to derive activity-based heuristics combined with the more classical value-based heuristics of CP solvers. The resulting solver is shown to be competitive with state-of-the-art exhaustive search solvers on the classical benchmarks of job shop and open shop problems.

‎_sessions/2023-09-11-certified-tsp.md‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
---
2+
layout: session
3+
title: Certification of an optimal TSP tour through 85,900 cities
4+
host: Konstantin Sidorov
5+
host_ref: https://ksidorov.nl
6+
session_type: paper
7+
related_papers: s20230911
8+
---
9+
10+
In this session I will go over the integer-programming flow for solving traveling salesman problem instances (utilized, among others, by <i>Concorde</i> TSP solver) and introduce the approach by Applegate et al. for logging the solver steps that lead to the optimal tour. This approach is used to justify an optimal tour on `pla85900`, the largest instance from the TSPLIB collection.

‎_sessions/2023-09-18-cumulative.md‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
---
2+
layout: session
3+
title: A (not so) brief overview of propagation (and explanations) for the cumulative constraint
4+
host: Imko Marijnissen
5+
session_type: tour
6+
related_papers: s20230918
7+
---
8+
9+
In this session I will go over the different techniques which have been introduced for solving the cumulative constraint. More specifically, the presentation will aim to provide an intuitive understanding of the different techniques and the subsequent improvements thereon. If time permits, the generation of explanations for the different propagators will also be discussed.

0 commit comments

Comments
 (0)