|
 |
Joao Marques-Silva is SFI Stokes Professor of Computer Science and Informatics, School of Computer Science and Informatics, University College Dublin, Ireland. Before joining UCD, Joao Marques-Silva held positions at the University of Southampton, UK, and at IST/Technical University of Lisbon, Portugal. Joao Marques-Silva has a BSc and a MSc from IST/Technical University of Lisbon, a PhD from the University of Michigan, and a Habilitation in Computer Science from the Technical University of Lisbon.
|
| Decision and optimization procedures, including Boolean satisfiability and extensions. Applied formal methods. Applications in system verification and model checking, artificial intelligence, design automation, and bioinformatics. |
| J. Marques-Silva and J. Planes; (2011) 'Algorithms for Maximum Satisfiability using Unsatisfiable Cores' In: Recent Advances in Logic Synthesis. Germany: Springer. [Details] |
Ana Graca, Joao Marques-Silva and Ines Lynce; (2011) 'Haplotype Inference using Propositional Satisfiability' In: R. Bruni (eds). Mathematical Approaches to Polymer Sequence Analysis. Germany: Springer.  [DOI] [Details] |
| J. Marques-Silva; (2009) 'Boolean Satisfiability and EDA Applications' In: Cambridge University Press. [Details] |
| J. Marques-Silva and I. Lynce and S. Malik; (2009) 'Conflict-Driven Clause Learning SAT Solvers' In: IOS Press. [Details] |
| I. Lynce and V. Manquinho and J. Marques-Silva; (2008) 'Backtracking' In: Wiley. [Details] |
| A. Bhalla and I. Lynce and J. Sousa and J. Marques-Silva; (2005) 'Heuristic-Based Backtracking Relaxation for Propositional Satisfiability' In: Springer. [Details] | |||||||||
| J. Marques-Silva and K. Sakallah; (2003) 'GRASP - A New Search Algorithm for Satisfiability' In: Kluwer Academic Publishers. [Details] | |||||||||
| I. Lynce and J. Marques-Silva; (2003) 'The Effect of Nogood Recording in DPLL-CBJ SAT Algorithms' In: Springer. [Details] | |||||||||
| W. Kunz and J. Marques-Silva and S. Malik; (2001) 'SAT and ATPG: Algorithms for Boolean Decision Problems' In: Kluwer Academic Publishers. [Details] | |||||||||
| Hide | |||||||||
| J. Marques-Silva and K. Sakallah (Ed.). (2007) 10th International Conference on Theory and Applications of Satisfiability Testing. Springer, LNCS 4501. [Details] |
| Lucas Cordeiro and Bernd Fischer and Joao Marques-Silva; (2011) 'SMT-Based Bounded Model Checking for Embedded ANSI-C Software'. IEEE Transactions on Software Engineering, . [Details] |
| Joao Marques-Silva and Josep Argelich and Ana Graça and Ines Lynce; (2011) 'Boolean Lexicographic Optimization'. Annals of Mathematics and Artificial Intelligence, . [Details] |
| Joao Marques-Silva; (2011) 'Computing Minimally Unsatisfiable Subformulas: State of the Art and Future Directions'. Journal of Multiple-Valued Logic and Soft Computing, . [Details] |
| A. Graça, J. Marques-Silva, I. Lynce and A. Oliveira; (2011) 'Haplotype Inference with Pseudo-Boolean Optimization'. Annals of Operations Research, 184 (1):137-162. [DOI] [Details] |
| I. Lynce and J. Marques-Silva; (2011) 'Restoring CSP Satisfiability with MaxSAT'. Fundamenta Informaticae, . [Details] |
| Karem A. Sakallah and Joao Marques-Silva; (2011) 'Anatomy and Empirical Evaluation of Modern SAT Solvers'. Bulleting of the EATCS, 103 :96-121. [Details] | |||||||||
| Y. Chen, S. Safarpour, J. Marques-Silva and A. Veneris; (2010) 'Automated Design Debugging with Maximum Satisfiability'. IEEE Transactions on COMPUTER-AIDED DESIGN of Integrated Circuits and Systems, 29 (11):1804-1817. [DOI] [Details] |
|||||||||
| Antonio Morgado and Joao Marques-Silva; (2010) 'Combinatorial Optimization Solutions for the Maximum Quartet Consistency Problem'. Fundamenta Informaticae, 102 (3-4):363-389. [DOI] [Details] |
|||||||||
| Ana Graça, Ines Lynce, Joao Marques-Silva and Arlindo Oliveira; (2010) 'Haplotype Inference by Pure Parsimony: a Survey'. Journal of Computational Biology, 17 (8):969-992. [DOI] [Details] |
|||||||||
| M. Liffiton and M. Mneimneh and I. Lynce and Z. Andraus and J. Marques-Silva and K. Sakallah; (2009) 'A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Subformulas'. Constraints: An International Journal, 13 (4):415-442. [Details] | |||||||||
| J. Marques-Silva; (2008) 'Model Checking with Boolean Satisfiability'. Journal of Algorithms in Cognition, Informatics and Logic, . [Details] | |||||||||
| I. Lynce and J. Marques-Silva and S. Prestwich; (2008) 'Boosting Haplotype Inference with Local Search'. Constraints: An International Journal, 13 (1-2):155-179. [Details] | |||||||||
| I. Lynce and J. Marques-Silva; (2008) 'Haplotype Inference with Boolean Satisfiability'. International Journal on Artificial Intelligence Tools, 17 (2):355-287. [Details] | |||||||||
| I. Lynce and J.Marques-Silva; (2007) 'Random Backtracking in Backtrack Search Algorithms for Satisfiability'. Discrete Applied Mathematics, 155 (12):1604-1612. [Details] | |||||||||
| J. Marques-Silva and K. Sakallah and I. Lynce; (2007) 'Report on the SAT 2007 Conference on Theory and Applications of Satisfiability Testing'. AI Magazine, 28 (4):135-136. [Details] | |||||||||
| J. Marques-Silva; (2007) 'Interpolant Learning and Reuse in SAT-Based Model Checking'. Electronic Notes on Theoretical Comptuer Science, 174 (3):31-43. [Details] | |||||||||
| V. Manquinho and J. Marques-Silva; (2006) 'On Using Cutting Planes in Pseudo-Boolean Optimization'. Journal on Satisfiability, Boolean Modeling and Computation, 2 :209-219. [Details] | |||||||||
| A.Bhalla and I. Lynce and J. Sousa and J. Marques-Silva; (2005) 'Heuristic-Based Backtracking Relaxation for Propositional Satisfiability'. Journal on Automated Reasoning, 35 (1-3):3-24. [Details] | |||||||||
| I. Lynce and J. Marques-Silva; (2005) 'Efficient Data Structures for Backtrack Search SAT Solvers'. Annals of Mathematics and Artificial Intelligence, 43 (1-4):137-152. [Details] | |||||||||
| V.~Manquinho e J.~Marques-Silva; (2004) 'On Solving Boolean Optimization with Satisfiability-Based Algorithms'. Annals of Mathematics and Artificial Intelligence, 40 (3-4). [Details] | |||||||||
| J. Marques-Silva and L. Guerra e Silva; (2003) 'Solving Satisfiability in Combinational Circuits'. IEEE Design and Test of Computers, 20 (4):16-21. [Details] | |||||||||
| I. Lynce and J. Marques-Silva; (2003) 'An Overview of Backtrack Search Satisfiability Algorithms'. Annals of Mathematics and Artificial Intelligence, 37 (3):307-326. [Details] | |||||||||
| V.~Manquinho and J.~Marques-Silva; (2002) 'Search Pruning Techniques in SAT-Based Branch-and-Bound Algorithms for the Binate Covering Problem'. IEEE Transactions on Computer-Aided Design, 21 (5):505-516. [Details] | |||||||||
| L.~Guerra e Silva and J.~Marques-Silva and L.~M. Silveira and K.~Sakallah; (2002) 'Satisfiability Models and Algorithms for Circuit Delay Computation'. ACM Transactions on Design Automation of Electronic Systems, 7 (1):137-158. [Details] | |||||||||
| P. Flores and H. Neto and J. Marques-Silva; (2001) 'An Exact Solution to the Minimum-Size Test Pattern Problem'. ACM Transactions on Design Automation of Electronic Systems, 6 (4):629-644. [Details] | |||||||||
| A.~Oliveira e J.~Marques-Silva; (2001) 'Efficient Algorithms for the Inference of Minimum Size DFAs'. Machine Learning, 44 (1-2):93-119. [Details] | |||||||||
| J.~Marques-Silva e K.~Sakallah; (1999) 'GRASP: A Search Algorithm for Propositional Satisfiability'. IEEE Transactions on Computers, 48 (5):506-521. [DOI] [Details] |
|||||||||
| M.~Riepe and J.~Marques-Silva and K.~Sakallah and R.~Brown; (1996) 'Ravel-XL: A Hardware Accelerator for Assigned-Delay Compiled-Code Logic Gate Simulation'. IEEE Transactions on VLSI Systems, 4 (1):113-129. [Details] | |||||||||
| Hide | |||||||||
| Federico Heras and Antonio Morgado and Joao Marques-Silva; (2011) Core-Guided Binary Search Algorithms for Maximum Satisfiability AAAI Conference on Artificial Intelligence [Details] |
| Federico Heras and Joao Marques-Silva; (2011) Read-Once Resolution for Unsatisfiability-Based Max-SAT International Joint Conference on Artificial Intelligence [Details] |
| Anton Belov and Joao Marques-Silva; (2011) Accelerating MUS Extraction with Recursive Model Rotation Formal Methods in Computer-Aided Design Austin, Texas, USA, , 30-OCT-11 - 02-NOV-11 [Details] |
| Joao Marques-Silva and Ines Lynce; (2011) On Improving MUS Extraction Algorithms International Conference on Theory and Applications of Satisfiability Testing [Details] |
| Mikolas Janota and Joao Marques-Silva; (2011) Abstraction-Based Algorithm for 2QBF International Conference on Theory and Applications of Satisfiability Testing [Details] |
| Mikolas Janota and Joao Marques-Silva; (2011) {On Deciding MUS Membership with QBF International Conference on Principles and Practice of Constraint Programming [Details] | |||||||||
| Anton Belov and Joao Marques-Silva; (2011) Minimally Unsatisfiable Boolean Circuits International Conference on Theory and Applications of Satisfiability Testing [Details] | |||||||||
| Mikolas Janota and Joao Marques-Silva; (2011) cmMUS: A Tool for Circumscription-Based MUS Membership Testing International Conference on Logic Programming and Nonmonotonic Reasoning [Details] | |||||||||
| Huan Chen and Joao Marques-Silva; (2011) Improvements to Satisfiability-Based Boolean Function Bi-Decomposition {International Conference on Very Large Scale Integration [Details] | |||||||||
| Hadi Katebi and Karem Sakallah and Joao Marques-Silva; (2011) Empirical Study of the Anatomy of Modern SAT Solvers International Conference on Theory and Applications of Satisfiability Testing [Details] | |||||||||
| Joao Marques-Silva and Mikolas Janota and Ines Lynce; (2010) On Computing Backbones of Propositional Theories European Conference on Artificial Intelligence [Details] | |||||||||
| M. Janota, R. Grigore and J. Marques-Silva; (2010) Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription . In: T. Janhunen and I. Niemela eds. European Conference on Logics in Artificial Intelligence , pp.195-207 [DOI] [Details] |
|||||||||
| Joao Marques-Silva; (2010) Minimal Unsatisfiability: Models, Algorithms & Applications International Symposium on Multi-Valued Logic [Details] | |||||||||
| A. Graca, I. Lynce, J. Marques-Silva and A. Oliveira; (2010) Efficient and Accurate Haplotype Inference by Combining Parsimony and Pedigree Information Algebraic and Numeric Biology [Details] | |||||||||
| A. Darbari, B. Fischer and J. Marques-Silva; (2010) Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking International Colloquium on Theoretical Aspects of Computing Natal, Brazil, , 01-SEP-10 - 03-SEP-10 [Details] | |||||||||
| Lucas Cordeiro and Bernd Fischer and Joao Marques-Silva; (2010) Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking Engineering of Computer-Based Systems [Details] | |||||||||
| M. Janota and G. Botterweck and R. Grigore and J. Marques-Silva; (2010) How to Complete an Interactive Configuration Process? -- Configuring as Shopping International Conference on Current Trends in Theory and Practice of Computer Science [Details] | |||||||||
| Joao Marques-Silva, Josep Argelich, Ana Graca and Ines Lynce; (2010) Boolean Lexicographic Optimization RCRA Workshop [Details] | |||||||||
| Josep Argelich and Daniel Le Berre and Ines Lynce and Joao Marques-Silva and Pascal Rapicault; (2010) Solving Linux Upgradeability Problems Using Boolean Optimization Workshop on Logics for Component Configuration [Details] | |||||||||
| P. Matos and B. Fischer and J. Marques-Silva; (2009) A Lazy Unbounded Model Checker for Event-B International Conference on Formal Engineering Methods [Details] | |||||||||
| Lucas Cordeiro and Bernd Fischer and Joao Marques-Silva; (2009) SMT-Based Bounded Model Checking for Embedded ANSI-C Software International Conference on Automated Software Engineering [Details] | |||||||||
| Huan Chen and Joao Marques-Silva; (2009) TG-PRO: A New Model for SAT-Based ATPG International High Level Design Validation and Test Workshop [Details] | |||||||||
| Ines Lynce and Joao Marques-Silva; (2009) Restoring CSP Satisfiability with MaxSAT Portuguese Conference on Artificial Intelligence [Details] | |||||||||
| Ana Graca and Ines Lynce and Joao Marques-Silva and Arlindo Oliveira; (2009) Haplotype Inference Combining Pedigrees and Unrelated Individuals Workshop on Constraint Based Methods for Bioinformatics [Details] | |||||||||
| Ashish Darbari and Bernd Fischer and Joao Marques-Silva; (2009) Formalizing a SAT Proof Checker in Coq Coq Workshop [Details] | |||||||||
| Josep Argelich and Ines Lynce and Joao Marques-Silva; (2009) On Solving Boolean Multilevel Optimization Problems International Joint Conference on Artificial Intelligence [Details] | |||||||||
| Vasco Manquinho and Joao Marques-Silva and Jordi Planes; (2009) Algorithms for Weighted Boolean Optimization International Conference on Theory and Applications of Satisfiability Testing [Details] | |||||||||
| Yibin Chen and Sean Safarpour and Andreas Veneris and Joao Marques-Silva; (2009) Spatial and Temporal Design Debug using Partial MaxSAT IEEE Great Lakes Symposium on VLSI [Details] | |||||||||
| Lucas Cordeiro and Bernd Fischer and Huan Chen and Joao Marques-Silva; (2009) Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints IEEE International Conference on Embedded Systems and Software [Details] | |||||||||
| A. Morgado and J. Marques-Silva; (2008) Combinatorial Optimization Solutions for the Maximum Quartet Consistency Problem RCRA Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion Udine, Italy, [Details] | |||||||||
| A. Graca and I. Lynce and J. Marques-Silva and A. Oliveira; (2008) Generic ILP vs Specialized 0-1 ILP for Haplotype Inference Workshop on Constraint Based Methods for Bioinformatics Paris, France, [Details] | |||||||||
| A. Morgado and J. Marques-Silva; (2008) A Pseudo-Boolean Solution to the Maximum Quartet Consistency Problem Workshop on Constraint Based Methods for Bioinformatics Paris, France, [Details] | |||||||||
| P.~Matos and J.~Planes and F.~Letombe and J.~Marques-Silva; (2008) An Algorithm Porfolio for MAX-SAT European Conference on Artificial Intelligence Patras, Greece, [Details] | |||||||||
| J.~Marques-Silva; (2008) Practical Applications of Boolean Satisfiability Workshop on Discrete Event Systems Gothenburg, Sweden, , pp.74-80 [Details] | |||||||||
| A.~Graca and J.~Marques-Silva and I.~Lynce and A.~Oliveira; (2008) Efficient Haplotype Inference with Combined CP and OR Techniques International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems Paris, France, , pp.308-312 [Details] | |||||||||
| P.~Matos and J.~Marques-Silva; (2008) Model Checking Event-B by Encoding into Alloy ABZ2008 Conference London, UK, [Details] | |||||||||
| F.~Letombe and J.~Marques-Silva; (2008) Improvements to Hybrid Incremental SAT Algorithms International Conference on Theory and Applications of Satisfiability Testing Guangzhou, China, , pp.168-181 [Details] | |||||||||
| J.~Marques-Silva and V.~Manquinho; (2008) Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms International Conference on Theory and Applications of Satisfiability Testing Guangzhou, China, , pp.225-230 [Details] | |||||||||
| J.~Marques-Silva and J.~Planes; (2008) Algorithms for Maximum Satisfiability using Unsatisfiable Cores Design, Automation and Test in Europe Conference and Exhibition Munich, France, , pp.408-413 [Details] | |||||||||
| J.~Marques-Silva and I.~Lynce and V.~Manquinho; (2008) Symmetry Breaking for Maximum Satisfiability International Conference on Logic for Programming Artificial Intelligence and Reasoning Doha, Qatar, [Details] | |||||||||
| I.~Lynce and A. Graca and J.~Marques-Silva and A.~Oliveira; (2008) Haplotype Inference with Boolean Constraint Solving: An Overview International Conference on Tools with Artificial Intelligence Dayton, Ohio, USA, [Details] | |||||||||
| F.~Heras and V.~Manquinho and J.~Marques-Silva; (2008) On Applying Unit Propagation-Based Lower Bounds in Pseudo-Boolean Optimization International FLAIRS Conference Coconut Grove, Florida, EUA, , pp.71-76 [Details] | |||||||||
| N.~Bombieri and F.~Fummi and G.~Pravadelli and J.~Marques-Silva; (2007) Towards Equivalence Checking Between TLM and RTL Models International Conference on Formal Methods and Models for Codesign Nice, France, , pp.113-122 [Details] | |||||||||
| A.~Graca and J.~Marques-Silva and I.~Lynce and A.~Oliveira; (2007) Efficient Haplotype Inference with Pseudo-Boolean Optimization International Conference on Algebraic Biology Hagenberg, Austria, , pp.125-139 [Details] | |||||||||
| J.~Marques-Silva and I.~Lynce; (2007) Towards Robust CNF Encodings of Cardinality Constraints International Conference on Principles and Practice of Constraint Programming Providence, Rhode Island, USA, , pp.483-497 [Details] | |||||||||
| J.~Marques-Silva and I.~Lynce and A.~Graca and A.~Oliveira; (2007) Efficient and Tight Upper Bounds for Haplotype Inference by Pure Parsimony Portuguese Conference on Artificial Intelligence Guimaraes, Portugal, , pp.621-632 [Details] | |||||||||
| I.~Lynce and J.~Marques-Silva; (2007) Breaking Symmetries in SAT Matrix Models International Conference on Theory and Applications of Satisfiability Testing Lisbon, Portugal, , pp.22-27 [Details] | |||||||||
| J. Marques-Silva; (2006) Interpolant Learning and Reuse in SAT-Based Model Checking Bounded Model Checking Workshop Seattle, Washington, U.S.A, [Details] | |||||||||
| I.~Lynce and J.~Marques-Silva; (2006) SAT in Bioinformatics: Making the Case with Haplotype Inference International Conference on Theory and Applications of Satisfiability Testing Seattle, Washington, USA, , pp.136-141 [Details] | |||||||||
| O. Kullmann and I.~Lynce and J.~Marques-Silva; (2006) Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel International Conference on Theory and Applications of Satisfiability Testing Seattle, Washington, USA, , pp.22-35 [Details] | |||||||||
| I.~Lynce and J.~Marques-Silva; (2006) Efficient Haplotype Inference with Boolean Satisfiability AAAI Conference on Artificial Intelligence Boston, Massachusetts, USA, , pp.104-109 [Details] | |||||||||
| A.~Morgado and P.~Matos and V.~Manquinho and J.~Marques-Silva; (2006) Counting Models in Integer Domains International Conference on Theory and Applications of Satisfiability Testing Seattle, Washington, USA, , pp.410-423 [Details] | |||||||||
| V.~Manquinho and J.~Marques-Silva; (2005) Effective Lower Bounding Techniques for Pseudo-Boolean Optimization Design, Automation and Test in Europe Conference Munich, Germany, , pp.660-665 [Details] | |||||||||
| V.~Manquinho and J.~Marques-Silva; (2005) On Applying Cutting Planes in DLL-Based Algorithms for Pseudo-Boolean Optimization International Conference on Theory and Applications of Satisfiability Testing St.~Andrews, UK, , pp.451-458 [Details] | |||||||||
| J.~Marques-Silva; (2005) Improvements to the Implementation of Interpolant-Based Model Checking Conference on Correct Hardware Design and Verification Methods Saarbrucken, Germany, , pp.367-370 [Details] | |||||||||
| A.~Morgado and J.~Marques-Silva; (2005) Good Learning and Implicit Model Enumeration International Conference on Tools with Artificial Intelligence Hong Kong, China, , pp.131-136 [Details] | |||||||||
| V.~Manquinho and J.~Marques~Silva; (2005) Satisfiability-Based Algorithms for Pseudo-Boolean Optimization Using Gomory Cuts and Search Restarts International Conference on Tools with Artificial Intelligence Hong Kong, China, , pp.150-155 [Details] | |||||||||
| M.~Mneimneh and I.~Lynce and Z.~Andraus and J.~Marques~Silva and K.~Sakallah; (2005) A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas International Conference on Theory and Applications of Satisfiability Testing St.~Andrews, UK, , pp.467-474 [Details] | |||||||||
| Hide | |||||||||
| J. Marques-Silva; (1995) Search Algorithms for Satisfiability Problems in Combinational Switching Circuits. Dissertations/Theses [Details] |
| Year: 2009. Title: 2009 CAV Award |
| Association: Institute of Electrical and Electronics Engineers (IEEE), Function/Role: Senior Member |
| Association: Association for Computing Machinery (ACM), Function/Role: Member |
| Employer: University of Southampton Position: Professor of Computer Science (Sep'07 - Jan'09) |
| Employer: University of Southampton Position: Senior Lecturer (Oct'05 - Aug'07) |
| Employer: IST/Technical University of Lisbon Position: Associate Professor (Sep'04 - Sep'05) |
| Employer: IST/Technical University of Lisbon Position: Assistant Professor (Oct'95 - Aug'04) |
| Year 2004 Institution: European Uni Lisbon Portugal Qualification: HABILITATION Subject: |
| Year 1995 Institution: University of Michigan Qualification: PhD Subject: Electrical Engineering and Computer Science |
| Year 1991 Institution: IST/Technical University of Lisbon Qualification: MSc Subject: Electrical and Computer Engineering |
| Year 1988 Institution: IST/Technical University of Lisbon Qualification: BSc Subject: Electrical and Computer Engineering |
