Welcome to my profile page. I am a Postdoctoral Research Associate at the School of Computer Science (SCS) at Carnegie Mellon University (CMU). My postdoc supervisor is associate professor Marijn Heule. My postdoc position at CMU is partially supported by an NSERC Postdoctoral Fellowship from Canada.
I completed my PhD and MSc from the computing science department of University of Alberta, Canada. I also have 5 years of software development experience from Canada.
My research interests lie in the area of automated reasoning (AR). AR studies computational frameworks that mimic reasoning aspects of human cognition. Currently, my focus is on boolean reasoning with Satisfiability (SAT) solving solving. SAT solving algorithms generate proofs for syntactically valid statements in propositional logic. In recent years, SAT solving has found numerous important practical applications in areas, such as formal verification, theorem proving, and AI.
The major theme of my work so far is to design, implement, and evaluate novel and effective algorithms for boolean reasoning. The solvers boosted with the techniques that I developed during my PhD study have improved state of the art of this area, and have won multiple awards in the recent international boolean satisfiability competitions.
My long-term research agendas are:
Informal Publications
I completed my PhD and MSc from the computing science department of University of Alberta, Canada. I also have 5 years of software development experience from Canada.
My research interests lie in the area of automated reasoning (AR). AR studies computational frameworks that mimic reasoning aspects of human cognition. Currently, my focus is on boolean reasoning with Satisfiability (SAT) solving solving. SAT solving algorithms generate proofs for syntactically valid statements in propositional logic. In recent years, SAT solving has found numerous important practical applications in areas, such as formal verification, theorem proving, and AI.
The major theme of my work so far is to design, implement, and evaluate novel and effective algorithms for boolean reasoning. The solvers boosted with the techniques that I developed during my PhD study have improved state of the art of this area, and have won multiple awards in the recent international boolean satisfiability competitions.
My long-term research agendas are:
- + Algorithmic Cooperation to boost solvers with algorithmic cooperation
- + Distributed Reasoning to develop solvers for a distributed environment
- + Machine Learning for Reasoning to improve performance of solvers using machine learning techniques
- + Explaining Solvers Performance Behavior to improve the understanding why problems which are understood to be hard in theory are easy to solve in practice
- + Impacting Other Reasoning Paradigms by transferring techniques developed for boolean reasoning to other related reasoning paradigms
Education
- + , 2016 - 2021, Department of Computing Science, University of Alberta, Edmonton, Canada.
Thesis: Empirical Insights Driven CDCL SAT Algorithms ()
Supervisors: Martin Mueller and Jia You - + , 2009 - 2011, Department of Computing Science, University of Alberta, Edmonton, Canada.
Thesis: SAT with Global Constraints
Supervisor: Jia You - + , 2004 - 2007, Department of Computer Science and Information Technology, Islamic Univ. of Technology, Bangladesh.
Thesis: Haplotype Inference by Pure Parsimony with SAT in Distributed Environment
Supervisor: Sardar Haque
Work Experience
- + , Feb, 2022 - Present, School of Computing Science, Carnegie Mellon University, Pittsburgh, PA, USA
- + , Jun 2021 - Sep 2021, Automated Reasoning@Amazon Research, Portland, OR, USA
- + , Sep 2016 - Dec 2021, Dept. of CS, University of Alberta, Edmonton, Canada
- + , Oct 2011 - Aug 2016, Technology North Corporation, Edmonton, Canada
- + , Nov 2007 - July 2009, Sylhet International University, Sylhet, Bangladesh
Publications
Referred Publications
-
+ Md Solimul Chowdhury, Cayden Codel, and Marijn J. H. Heule: A Linear Weight Transfer Rule for Local Search.
NASA Formal Methods-2023. [Paper] [Code]
- + Acceptance Rate: 38.66% (29/75)
-
+ Armin Biere, Md Solimul Chowdhury, Marijn J. H. Heule, Benjamin Kiesl, and Michael W. Whalen (2022).
Migrating Solver State.
SAT 2022:27:1--27:24 [Paper] [Code]
- + Acceptance Rate: 44.28 % (31/70)
- + Nominated for a Best Paper Award (3/70)
-
+ Md. Solimul Chowdhury, Martin Mueller, Jia-Huai You: Guiding CDCL SAT Search via Random Exploration amid Conflict Depression. AAAI 2020. [Paper] [Code]
- + Acceptance Rate: 20.6% (1591/7737)
- + Selected for Oral Presentation
- + Oral Acceptance Rate: 5.8% (454/7737)
-
+ Md. Solimul Chowdhury, Martin Mueller, Jia-Huai You: Exploiting Glue Clauses to Design Effective CDCL Branching Heuristics. CP 2019. [Paper] [Code]
- + Acceptance Rate: 36.36% (44/120)
-
+ Md. Solimul Chowdhury, Martin Mueller, Jia-Huai You: Preliminary Results on Exploration-Driven Satisfiability Solving. AAAI 2018. [Paper]
- + Student Abstract Finalist (Top 18% of the accepted abstracts)
-
+ Fangfang Liu, Yi Bi, Md. Solimul Chowdhury, Jia-Huai You, Zhiyong Feng:
Flexible Approximators for Approximating Fixpoint Theory. Canadian Conference on AI 2016. [Paper]
- + Acceptance Rate: 40.20% (39/97)
-
+ Md. Solimul Chowdhury, Fangfang Liu, Wu Chen, Arash Karimi, Jia-Huai You:
Polynomial Approximation to Well-Founded Semantics for Logic Programs with Generalized Atoms: Case Studies. LOPSTR 2014. [Paper]
- + Acceptance Rate: 52.95% (18/34)
-
+ Md. Solimul Chowdhury, Jia-Huai You:
SAT with Global Constraints. ICTAI 2012. [Paper]
- + Acceptance Rate: 55.00% (165/300)
- + Md. Solimul Chowdhury, Md Sakibul Hasan, Sardar Anisul Haque: Haplotype inference by pure parsimony by SAT solver in distributed environment. IJCSNS:VOL.8 No.8:2008. [Paper]
Under Preparation
- + Md Solimul Chowdhury , Martin Mueller, and Jia-Huai You: A Deep Dive into Conflict Generating Decisions. CoRR abs/2105.04595 (2021) [Paper]
Informal Publications
- + Md Solimul Chowdhury , Martin Mueller, and Jia-Huai You: Population Safety- A SAT Benchmark based on Elementary Cellular Automaton. In Proceedings of SAT Competition 2020: 75-76. [Paper]
- + Md. Solimul Chowdhury, Martin Mueller, Jia-Huai You: Four CDCL SAT Solvers based on Exploration and Glue Variable Bumping, Proceedings of SAT Race 2019:17-19. [Paper]
- + Md. Solimul Chowdhury, Martin Mueller, Jia-Huai You: Exploration via Random Walks in CDCL SAT Amid Conflict Depression. Proceedings of CP-2019 Doctoral Program. (informal) [Paper]
- + Md. Solimul Chowdhury, Martin Mueller, Jia-Huai You: Characterization of Glue Variables in CDCL SAT Solving. CoRR abs/1904.11106, 2019. [Paper]
- + Md. Solimul Chowdhury, Martin Mueller, Jia-Huai You: Description of expSAT Solvers, Proceedings of SAT Competition, 2018. [Paper]
- + Md. Solimul Chowdhury, Martin Mueller, Jia-Huai You: GrandTour^{obs} Puzzle as a SAT Benchmark, Proceedings of SAT Competition, 2018. [Paper]
- + Md. Solimul Chowdhury: Task and Energy Aware Node Placement in Wirelessly Rechargeable WSNs. CoRR abs/1805.07795, 2018. [Paper]
- + Md. Solimul Chowdhury, Victor Silva: Evolving Real-Time Heuristics Search Algorithms with Building Blocks. CoRR abs/1805.08256, 2018. [Paper]
Talks
Invited Talks
- + Extensions of CDCL Branching Heuristics by Exploration during Conflict Depression. At the workshop of Theoretical Foundations of SAT/SMT Solving, Simons Institute for the Theory of Computing, University of California, Berkeley, 28th April, 2021. [Talk]
Conference Talks
- + Guiding CDCL SAT Search via Random Exploration amid Conflict Depression. Technical Program at AAAI-2020, New York, USA [Talk]
- + Exploiting Glue Clauses to Design Effective CDCL Branching Heuristics, Main Technical Program at CP2019, Stamford, Connecticut, USA [Talk]
- + Flexible Approximators for Approximating Fixpoint Theory. Canadian Conference on AI 2016. [Talk]
Industry Talks
- + SAT with Memory. End of Internship Talk. Trusted Solver Group@Amazon Web Services (AWS). [Talk]
Academic Services
Juornal Reviewer
- + Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 2021
Program Committee Member
- + AAAI-2023, AAAI-2021, IJCAI-2020, ECAI-2020
External Reviewer
- + CADE-2023, SoCS-2018, IJCAI-2017 , ASPOCP-2017 , AAAI-2017 , Canadian AI-2017 , ICAPS-2017, ICLP-2016 , KR2016 , AAAI-2016 ASPOCP-2015 , LPNMR-2015 , ICLP-2015 KSEM-2014, ICLP-2013, Canadian AI-2011
Competition Medals
SAT Competition 2022
- + Bronze medal (3rd place out of 29 solvers) medal in the SAT subtrack of the Anniversary Sequential Track [Announcement] [Medal]
- + Bronze medal (3rd place out of 29 solvers) medal in the Anniversary Sequential Track [Announcement] [Medal]
- + Bronze medal (3rd place out of 52 solvers) medal in the MAIN track [Announcement] [Medal]
SAT Competition 2021
- + Bronze medal (ranked 3rd out of 48 solvers) medal in the SAT track [Announcement] [Medal]
- + Bronze medal (ranked 3rd out of 48 solvers) medal in the MAIN track [Announcement] [Medal]
SAT Race 2019
- + Silver medal (ranked 2nd out of 55 solvers) medal in the UNSAT track [Announcement]
Fellowships, Scholarships, and Grants
- + NSERC Postdoctoral Fellowship, Feb 2022 - Jan 2024
- + Alberta Excellence Graduate Scholarship, 2021
- + Ernst Mach Scholarship, 2021 (declined due to COVID-19)
- + AAAI Student Scholarship, 2020
- + Doctoral Program Travel Grant (CP 2019)
- + Alberta Innovates Graduate Student Scholarship, 2018
- + President’s Doctoral Prize of Distinction, 2018-2020
- + NSERC PGS Doctoral Scholarship, 2018-2020
- + GSA Travel Award, 2018
- + AAAI Student Scholarship, 2018
- + QE II Doctoral Scholarship, 2016
- + AITF R&D Award Industrial, 2012-2014
- + Swedish Trust Scholarship, 2010
- + Entrance Scholarship, Islamic Univ. of Tech, 2004-2006