Time: March 7th, 6:30pm onwards and March 8th, 2pm onwards
Venue: KR125
The students will read the papers published in SAT 2024 conference and give in-depth presentations. Students are expected to prepare a short presentation of 10-15 mins but be ready for a long discussion.
| Time | Roll No | Name | Task/Presentation Detail |
|---|---|---|---|
| 4th March TBD | 22b0980 | Ananya Rao | Models and Counter-Models of Quantified Boolean Formulas (Invited Talk) Authors: Martina Seidl |
| 7th March 6:30PM | 23b0974 | Krish Gupta | Clausal Congruence Closure |
| 7th March 6:50PM | 210050156 | Tanmay Arun Patil | eSLIM: Circuit Minimization with SAT Based Local Improvement |
| 7th March 7:10PM | 24d0379 | Sagar Kumar Verma | Lazy Reimplication in Chronological Backtracking |
| 7th March 7:30PM | 210050124 | Prerak Contractor | Parallel Clause Sharing Strategy Based on Graph Structure of SAT Problem |
| 7th March 7:50PM | 210050023 | Ashwin Abraham | SAT Encoding of Partial Ordering Models for Graph Coloring Problems |
| 7th March 8:10PM | 22b0982 | Tec Narayan Brahmachari | Cooking String-Integer Conversions with Noodles |
The students will study some specific aspects of certain solvers. Students are expected to prepare a short presentation of 10-15 mins along with the code walk describing the precise implementation details and be ready for a long discussion. Please provide pseudo codes to describe algorithms.
| Time | Roll No | Name | Task/Presentation Detail |
|---|---|---|---|
| March 8th, 2:00PM | 210050005 | Aditya Raj | Study the implementation of first UIP in Cadical |
| March 8th, 2:20PM | 22b1017 | Manchineni Yashwanth | Study the efficient implementation of blocked clause elimination in Cadical |
| March 8th, 2:40PM | 23b1048 | Sanchita Chaurasia | Study the new idea of SDCL and solver Sadical based on the idea. |
| March 8th, 3:00PM | 23b0912 | Sanapala Venkata Aditya | Study (non)-chronological backtracking in CaDiCaL or another SAT solver |
| March 8th, 3:20PM | 210050159 | Vaibhav Vishal | Study clause deletion strategy in Cadical |
| March 8th, 3:40PM | 22b1050 | J Tanvi Sree | Study clause deletion strategy in a top-ranked solver other than Cadical |
| Time | Roll No | Name | Task/Presentation Detail |
|---|---|---|---|
| March 8th, 5:00PM | 23b1033 | Chinthaparthi Babu Sujan Reddy | Study tactics layer in Z3 that optimizes the uses of the solver |
| March 8th, 5:20PM | 23b1060 | Madhav R Babu | Study model counting tool for pseudo boolean constraints PbCount |
| March 8th, 5:40PM | 24d0364 | Rahul Kapur | Study the handling of Xor constraints in Cryptominisat |
| March 8th, 6:00PM | 22b1054 | S.Shravan | Study Lovaz local lemma and modern SAT solver, can we observe the effect of the lemma in practice? |
| March 8th, 6:20PM | 24D0361 | Kalind Rajesh Karia | Study effect of software prefetching on watched list traversal |