Md Solimul Chowdhury

Postdoctoral Research Associate
School of Computer Science
Carnegie Mellon University


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:

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

  • + 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]
    • + 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

    • + 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

    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