Mikolas Janota
AuthID: R-004-VTA
41
TITLE: Solving QBF with counterexample guided refinement
AUTHORS: Mikolás Janota; William Klieber; Joao Marques Silva ; Edmund M. Clarke;
PUBLISHED: 2016, SOURCE: Artif. Intell., VOLUME: 234
AUTHORS: Mikolás Janota; William Klieber; Joao Marques Silva ; Edmund M. Clarke;
PUBLISHED: 2016, SOURCE: Artif. Intell., VOLUME: 234
INDEXED IN: 
DBLP
DBLP42
TITLE: On intervals and bounds in bit-vector arithmetic
AUTHORS: Mikoláš Janota; Christoph M Wintersteiger;
PUBLISHED: 2016, SOURCE: CEUR Workshop Proceedings, VOLUME: 1617
AUTHORS: Mikoláš Janota; Christoph M Wintersteiger;
PUBLISHED: 2016, SOURCE: CEUR Workshop Proceedings, VOLUME: 1617
INDEXED IN: 
Scopus
Scopus IN MY: 
ORCID
ORCID43
TITLE: On Q-Resolution and CDCL QBF Solving
AUTHORS: Janota, M;
PUBLISHED: 2016, SOURCE: THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2016, VOLUME: 9710
AUTHORS: Janota, M;
PUBLISHED: 2016, SOURCE: THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2016, VOLUME: 9710
44
TITLE: Extension variables in QBF resolution
AUTHORS: Olaf Beyersdorff; Leroy Chew; Mikoláš Janota;
PUBLISHED: 2016, SOURCE: AAAI Workshop - Technical Report, VOLUME: WS-16-01 - WS-16-15
AUTHORS: Olaf Beyersdorff; Leroy Chew; Mikoláš Janota;
PUBLISHED: 2016, SOURCE: AAAI Workshop - Technical Report, VOLUME: WS-16-01 - WS-16-15
INDEXED IN: Scopus
Scopus IN MY: ORCID
ORCID45
TITLE: Algorithms for computing backbones of propositional formulae Full Text
AUTHORS: Janota, M; Lynce, I ; Marques Sliva, J ;
PUBLISHED: 2015, SOURCE: AI COMMUNICATIONS, VOLUME: 28, ISSUE: 2
AUTHORS: Janota, M; Lynce, I ; Marques Sliva, J ;
PUBLISHED: 2015, SOURCE: AI COMMUNICATIONS, VOLUME: 28, ISSUE: 2
46
TITLE: Proof complexity of resolution-based QBF calculi
AUTHORS: Beyersdorff, O; Chew, L; Janota, M;
PUBLISHED: 2015, SOURCE: 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015 in Leibniz International Proceedings in Informatics, LIPIcs, VOLUME: 30
AUTHORS: Beyersdorff, O; Chew, L; Janota, M;
PUBLISHED: 2015, SOURCE: 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015 in Leibniz International Proceedings in Informatics, LIPIcs, VOLUME: 30
INDEXED IN: Scopus
Scopus IN MY: ORCID
ORCID47
TITLE: Expansion-based QBF solving versus Q-resolution Full Text
AUTHORS: Janota, M; Marques Silva, J ;
PUBLISHED: 2015, SOURCE: THEORETICAL COMPUTER SCIENCE, VOLUME: 577, ISSUE: 1
AUTHORS: Janota, M; Marques Silva, J ;
PUBLISHED: 2015, SOURCE: THEORETICAL COMPUTER SCIENCE, VOLUME: 577, ISSUE: 1
48
TITLE: Quantified maximum satisfiability Full Text
AUTHORS: Alexey Ignatiev; Mikoláš Janota; Joao Marques Silva;
PUBLISHED: 2015, SOURCE: Constraints
AUTHORS: Alexey Ignatiev; Mikoláš Janota; Joao Marques Silva;
PUBLISHED: 2015, SOURCE: Constraints
49
TITLE: Exploiting Resolution-Based Representations for MaxSAT Solving
AUTHORS: Neves, M; Martins, R; Janota, M; Lynce, I ; Manquinho, V;
PUBLISHED: 2015, SOURCE: 18th International Conference on Theory and Applications of Satisfiability Testing (SAT) in THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2015, VOLUME: 9340
AUTHORS: Neves, M; Martins, R; Janota, M; Lynce, I ; Manquinho, V;
PUBLISHED: 2015, SOURCE: 18th International Conference on Theory and Applications of Satisfiability Testing (SAT) in THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2015, VOLUME: 9340
50
TITLE: Solving QBF by Clause Selection
AUTHORS: Mikolás Janota; Joao Marques Silva ;
PUBLISHED: 2015, SOURCE: 24th International Joint Conference on Artificial Intelligence, IJCAI 2015 in Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, VOLUME: 2015-January
AUTHORS: Mikolás Janota; Joao Marques Silva ;
PUBLISHED: 2015, SOURCE: 24th International Joint Conference on Artificial Intelligence, IJCAI 2015 in Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, VOLUME: 2015-January
INDEXED IN: Scopus DBLP
Scopus DBLP IN MY: ORCID
ORCID