???global.info.a_carregar???
Mikoláš Janota. Concluiu o(a) Magister em Computer Science em 2005 pelo(a) Univerzita Karlova Matematicko-fyzikální fakulta. É Professor Auxiliar no(a) Universidade de Lisboa Instituto Superior Técnico. Publicou 12 artigos em revistas especializadas. Possui 21 livro(s). Nas suas atividades profissionais interagiu com 55 colaborador(es) em coautorias de trabalhos científicos.
Identificação

Identificação pessoal

Nome completo
Mikoláš Janota

Nomes de citação

  • Janota, Mikoláš

Identificadores de autor

Ciência ID
231F-5811-EDEA
ORCID iD
0000-0003-3487-784X

Idiomas

Idioma Conversação Leitura Escrita Compreensão Peer-review
Checo Utilizador proficiente (C2) Utilizador proficiente (C2) Utilizador proficiente (C2) Utilizador proficiente (C2)
Inglês Utilizador proficiente (C1) Utilizador proficiente (C1) Utilizador proficiente (C1) Utilizador proficiente (C1)
Português Utilizador proficiente (C1) Utilizador proficiente (C1) Utilizador independente (B1) Utilizador proficiente (C1)
Polaco Utilizador elementar (A1) Utilizador independente (B1) Utilizador elementar (A1) Utilizador elementar (A1)
Francês Utilizador elementar (A1) Utilizador independente (B1) Utilizador elementar (A1) Utilizador elementar (A1)
Formação
Grau Classificação
2006/01/10 - 2011/11/02
Concluído
 Computer Science (Doctor of Philosophy)
University College Dublin, Irlanda
"SAT Solving in Interactive Configuration" (TESE/DISSERTAÇÃO)
2005
Concluído
 Computer Science (Magister)
Univerzita Karlova Matematicko-fyzikální fakulta, República Checa
"Automated Theorem Proving and Program Verification " (TESE/DISSERTAÇÃO)
 N/A
Percurso profissional

Docência no Ensino Superior

Categoria Profissional
Instituição de acolhimento 		Empregador
2017/02/01 - Atual Professor Auxiliar (Docente Universitário) Universidade de Lisboa Instituto Superior Técnico, Portugal
2015/09/14 - 2017/02/12 Professor Auxiliar Convidado (Docente Universitário) Universidade de Lisboa Faculdade de Ciências, Portugal
Produções

Publicações

Artigo em conferência
  1. Hula, Jan; Mojzisek, David; Janota, Mikolas. "Graph Neural Networks for Scheduling of SMT Solvers". 2021.
    10.1109/ICTAI52525.2021.00072
  2. Janota, Mikolas. "On Unordered BDDs and Quantified Boolean Formulas". 2019.
    10.1007/978-3-030-30244-3_41
  3. Janota, Mikoláš. "Towards Smarter MACE-style Model Finders". 2018.
    10.29007/w42s
  4. Janota, M.. "Towards generalization in QBF solving via machine learning". 2018.
  5. Janota, M.; Grigore, R.; Manquinho, V.. "On the quest for an acyclic graph". 2017.
  6. Janota, M.; Marques-Silva, J.. "On Minimal corrections in ASP". 2017.
  7. Beyersdorff, O.; Chew, L.; Janota, M.. "Extension variables in QBF resolution". 2016.
  8. Janota, M.; Wintersteiger, C.M.. "On intervals and bounds in bit-vector arithmetic". 2016.
  9. Beyersdorff, O.; Chew, L.; Janota, M.. "Proof complexity of resolution-based QBF calculi". 2015.
    10.4230/LIPIcs.STACS.2015.76
  10. Marques-Silva, J.; Janota, M.; Ignatiev, A.; Morgado, A.. "Efficient model based diagnosis with maximum satisfiability". 2015.
  11. Janota, M.; Marques-Silva, J.. "Solving QBF by clause selection". 2015.
  12. Balabanov, V.; Jiang, J.-H.R.; Janota, M.; Widl, A.M.. "Efficient extraction of QBF (counter) models from long-distance resolution proofs". 2015.
  13. Ignatiev, A.; Janota, M.; Marques-Silva, J.. "Towards efficient optimization in package management systems". 2014.
    10.1145/2568225.2568306
  14. Janota, M.; Botterweck, G.; Marques-Silva, J.. "On lazy and eager interactive reconfiguration". 2014.
    10.1145/2556624.2556644
  15. Marques-Silva, J.; Heras, F.; Janota, M.; Previti, A.; Belov, A.. "On computing Minimal Correction Subsets". 2013.
  16. Chen, H.; Janota, M.; Marques-Silva, J.. "QBf-based Boolean function bi-decomposition". 2012.
  17. Bordeaux, L.; Janota, M.; Marques-Silva, J.; Marquis, P.. "On unit-refutation complete formulae with existentially quantified variables". 2012.
  18. Janota, Mikoláš. "Solving QBF with Counterexample Guided Refinement". 2012.
    10.1007/978-3-642-31612-8\_10
  19. Janota, M.; Grigore, R.; Moskal, M.. "Reachability analysis for annotated code". 2007.
    10.1145/1292316.1292319
  20. Janota, M.; Kiniry, J.. "Reasoning about feature models in higher-order logic". 2007.
    10.1109/SPLINE.2007.4339251
Artigo em revista
  1. Mohammad Rohaninejad; Mikoláš Janota; Zdenek Hanzálek. "Integrated lot-sizing and scheduling: Mitigation of uncertainty in demand and processing time by machine learning". Engineering Applications of Artificial Intelligence (2023): https://doi.org/10.1016/j.engappai.2022.105676.
    10.1016/j.engappai.2022.105676
  2. Araujo, Joao; Chow, Choiwah; Janota, Mikolas. "Boosting isomorphic model filtering with invariants". Constraints (2022): https://publons.com/wos-op/publon/53799722/.
    10.1007/S10601-022-09336-X
  3. Beyersdorff, Olaf; Chew, Leroy; Janota, Mikolas. "New Resolution-Based QBF Calculi and Their Proof Complexity". ACM Transactions on Computation Theory (2019): https://publons.com/publon/30340209/.
    10.1145/3352155
  4. Marques-Silva, J.; Janota, M.; Mencía, C.. "Minimal sets on propositional formulae. Problems and reductions". Artificial Intelligence 252 (2017): 22-50. http://www.scopus.com/inward/record.url?eid=2-s2.0-85028061913&partnerID=MN8TOARS.
    10.1016/j.artint.2017.07.005
  5. Mikoláš Janota; William Klieber; Joao Marques-Silva; Edmund Clarke. "Solving QBF with counterexample guided refinement". Artificial Intelligence 234 (2016): 1-25. https://doi.org/10.1016%2Fj.artint.2016.01.004.
    10.1016/j.artint.2016.01.004
  6. Mikoláš Janota; Joao Marques-Silva. "On the query complexity of selecting minimal sets for monotone predicates". Artificial Intelligence 233 (2016): 73-83. https://doi.org/10.1016%2Fj.artint.2016.01.002.
    10.1016/j.artint.2016.01.002
  7. Ignatiev, A.; Janota, M.; Marques-Silva, J.. "Quantified maximum satisfiability". Constraints 21 2 (2016): 277-302. http://www.scopus.com/inward/record.url?eid=2-s2.0-84959216203&partnerID=MN8TOARS.
    10.1007/s10601-015-9195-9
  8. Janota, Mikoláš. "Expansion-based QBF solving versus Q-resolution". Theoretical Computer Science (2015):
    10.1016/j.tcs.2015.01.048
  9. Janota, M.; Lynce, I.; Marques-Silva, J.. "Algorithms for computing backbones of propositional formulae". AI Communications 28 2 (2015): 161-177. http://www.scopus.com/inward/record.url?eid=2-s2.0-84922535838&partnerID=MN8TOARS.
    10.3233/AIC-140640
  10. Belov, A.; Janota, M.; Lynce, I.; Marques-Silva, J.. "Algorithms for computing minimal equivalent subformulas". Artificial Intelligence 216 (2014): 309-326. http://www.scopus.com/inward/record.url?eid=2-s2.0-84907340206&partnerID=MN8TOARS.
    10.1016/j.artint.2014.07.011
  11. Huan Chen; M. Janota; J. Marques-Silva. "QBF-Based Boolean Function Bi-Decomposition". DESIGN, AUTOMATION & TEST IN EUROPE (DATE) (2012): https://publons.com/publon/15301009/.
    10.1109/DATE.2012.6176606
  12. Delgrande, JP; Faber, W; Janota, Mikolas; Marques-Silva, Joao. "cmMUS: A Tool for Circumscription-Based MUS Membership Testing". Logic Programming and Nonmonotonic Reasoning 6645 (2011): 266-271.
  13. Coelho, H; Janota, Mikolas; Lynce, Ines; Marques-Silva, Joao; Studer, R; Wooldridge, M. "On Computing Backbones of Propositional Theories". Ecai 2010 - 19th European Conference on Artificial Intelligence 215 (2010): 15-20.
    10.3233/978-1-60750-606-5-15
  14. Janota, Mikolas; Kiniry, Joseph. "Reasoning about feature models in higher-order logic". SPLC 2007: 11TH INTERNATIONAL SOFTWARE PRODUCT LINE CONFERENCE, PROCEEDINGS (2007): https://publons.com/publon/7885204/.
    10.1109/SPLINE.2007.36
Capítulo de livro
  1. Nikolai Antonov; Premysl Šucha; Mikoláš Janota. "Data-driven Single Machine Scheduling Minimizing Weighted Number of Tardy Jobs". 2023.
    10.1007/978-3-031-49008-8_38
  2. Pedro Orvalho; Jelle Piepenbrock; Mikoláš Janota; Vasco Manquinho. "Graph Neural Networks for Mapping Variables Between Programs". 2023.
    10.3233/FAIA230468
  3. Jelle Piepenbrock; Tom Heskes; Mikoláš Janota; Josef Urban. "Guiding an Automated Theorem Prover with Neural Rewriting". 2022.
    10.1007/978-3-031-10769-6_35
  4. Mikoláš Janota; António Morgado. "SAT-Based Encodings for Optimal Decision Trees with Explicit Paths". 501-518. Springer International Publishing, 2020.
    10.1007/978-3-030-51825-7_35
Livro
  1. Janota, M.. Circuit-based search space pruning in QBF. 2018.
    10.1007/978-3-319-94144-8_12
  2. Janota, M.; Marques-Silva, J.. An Achilles’ Heel of term-resolution. 2017.
    10.1007/978-3-319-65340-2_55
  3. Si, X.; Zhang, X.; Manquinho, V.; Janota, M.; Ignatiev, A.; Naik, M.. On incremental core-guided MaxSAT solving. 2016.
    10.1007/978-3-319-44953-1_30
  4. Janota, M.. On Q-resolution and CDCL QBF solving. 2016.
    10.1007/978-3-319-40970-2_25
  5. Neves, M.; Martins, R.; Janota, M.; Lynce, I.; Manquinho, V.. Exploiting resolution-based representations for MaxSAT solving. 2015.
    10.1007/978-3-319-24318-4_20
  6. Beyersdorff, O.; Chew, L.; Janota, M.. On unification of QBF resolution-based calculi. 2014.
    10.1007/978-3-662-44465-8_8
  7. Klieber, W.; Janota, M.; Marques-Silva, J.; Clarke, E.. Solving QBF with free variables. 2013.
    10.1007/978-3-642-40627-0_33
  8. Ignatiev, A.; Janota, M.; Marques-Silva, J.. Quantified maximum satisfiability: A core-guided approach. 2013.
    10.1007/978-3-642-39071-5_19
  9. Janota, M.; Grigore, R.; Marques-Silva, J.. On QBF proofs and preprocessing. 2013.
    10.1007/978-3-642-45221-5_32
  10. Marques-Silva, J.; Janota, M.; Belov, A.. Minimal sets over monotone predicates in Boolean formulae. 2013.
    10.1007/978-3-642-39799-8_39
  11. Janota, M.; Marques-Silva, J.. On propositional QBF expansions and Q-resolution. 2013.
    10.1007/978-3-642-39071-5_7
  12. Belov, A.; Janota, M.; Lynce, I.; Marques-Silva, J.. On computing minimal equivalent subformulas. 2012.
    10.1007/978-3-642-33558-7_14
  13. Janota, M.; Klieber, W.; Marques-Silva, J.; Clarke, E.. Solving QBF with counterexample guided refinement. 2012.
    10.1007/978-3-642-31612-8_10
  14. Janota, M.; Marques-Silva, J.. On deciding MUS membership with QBF. 2011.
    10.1007/978-3-642-23786-7_32
  15. Janota, M.; Marques-Silva, J.. Abstraction-based algorithm for 2QBF. 2011.
    10.1007/978-3-642-21581-0_19
  16. Janota, M.; Marques-Silva, J.. CmMUS: A tool for circumscription-based MUS membership testing. 2011.
    10.1007/978-3-642-20895-9_30
  17. Janota, M.; Grigore, R.; Marques-Silva, J.. Counterexample guided abstraction refinement algorithm for propositional circumscription. 2010.
    10.1007/978-3-642-15675-5_18
  18. Janota, M.; Botterweck, G.; Grigore, R.; Marques-Silva, J.. How to complete an interactive configuration process? Configuring as shopping. 2010.
    10.1007/978-3-642-11266-9_44
  19. Janota, M.; Fairmichael, F.; Holub, V.; Grigore, R.; Charles, J.; Cochran, D.; Kiniry, J.R.. CLOPS: A DSL for command line options. 2009.
    10.1007/978-3-642-03034-5_10
  20. Janota, M.; Kuzina, V.; Wa¸sowski, A.. Model construction with external constraints: An interactive journey from semantics to syntax. 2008.
    10.1007/978-3-540-87875-9_31
  21. Janota, M.; Botterweck, G.. Formal approach to integrating feature and architecture models. 2008.
    10.1007/978-3-540-78743-3_3