Research interests
- Satisfiability Modulo Theories (SMT)
- Boolean Satisfiability (SAT)
- Applications of SAT and SMT
- Interactive theorem proving
- Constraint Satisfaction Problems (CSP)
Publications
-
Milan Banković. Automation of Triangle Ruler-and-Compass Constructions Using Constraint Solver. ADG 2023. Belgrade, Serbia. September 20-22, 2023. ([pdf-draft])
-
Milan Banković, Ivan Drecun, Filip Marić. A proof system for graph (non)-isomorphism verification.
Logical Methods in Computer Science. 2023. ([pdf], [LMCS])
-
Milan Banković, David Šćepanović. Trail saving in SMT. Federated
Logic Conference 2022. (International Workshop on Satisfiability Modulo
Theories - SMT2022). Haifa, Israel, July 31 - August 12, 2022. ([pdf],[proceedings])
-
Milan Banković, Filip Marić. Faradžev Read-type enumeration of non-isomorphic CC systems. Computational Geometry. 2021. ([pdf],[elsevier])
-
Milan Banković. Automated solving of Sokoban puzzle using artificial intelligence. YU INFO 2021, Kopaonik, Serbia (in Serbian). 2021. ([pdf],[proceedings])
-
Milan Banković et al. Teaching graduate students how to review research
articles and respond to reviewer comments. Advances in Computers. 2020. ([elsevier])
-
Milan Banković. Improving SMT solvers using CSP
techniques and parallelization techniques. Doctoral
dissertation (in Serbian). 2016. ([pdf])
-
Milan Banković. Solving finite-domain linear constraints in presence of the alldifferent.
Logical Methods in Computer Science. 2016. ([pdf], [LMCS])
-
Milan Banković. Parallelizing simplex within SMT solvers.
Artificial Intelligence Review. 2016. ([pdf], [springer])
-
Milan Banković. Extending SMT solvers with support for finite domain alldifferent constraint.
Constraints. 2015. ([pdf], [springer])
-
Milan Banković. ArgoSMTe: an SMT-LIB 2.0 compliant expression library.
Pragmatics of SAT 2012. ([pdf])
-
Milan Banković. Filip Marić.
Alldifferent constraint solver in SMT.
Federated Logic Conference 2010. (International Workshop on Satisfiability Modulo Theories - SMT'10).
([pdf])
