Navigation

Researchers at UCD

researcher

Joao Marques-Silva

Sfi Stokes Professor Computer Science & Informatics

School of Computer Science & Informatics
UCD CASL
Belfield Office Park, Dublin 4

Tel: +353 1 716 5700
Email: jpms@ucd.ie

Biography

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.

 

Professional

Honours and Awards

Year: 2009.
Title: 2009 CAV Award

Associations

Association: Institute of Electrical and Electronics Engineers (IEEE), Function/Role: Senior Member
Association: Association for Computing Machinery (ACM), Function/Role: Member
         

Employment

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)

Education

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
         

Publications

 

Book Chapters

J. Marques-Silva and J. Planes; (2011) 'Algorithms for Maximum Satisfiability using Unsatisfiable Cores' In: J. Marques-Silva and J. Planes; (eds). 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. , pp.127-147 Available Online [DOI] [Details]
J. Marques-Silva; (2009) 'Boolean Satisfiability and EDA Applications' In: J. Marques-Silva; (eds). Cambridge University Press. [Details]
J. Marques-Silva and I. Lynce and S. Malik; (2009) 'Conflict-Driven Clause Learning SAT Solvers' In: J. Marques-Silva and I. Lynce and S. Malik; (eds). IOS Press. [Details]
I. Lynce and V. Manquinho and J. Marques-Silva; (2008) 'Backtracking' In: I. Lynce and V. Manquinho and J. Marques-Silva; (eds). Wiley. [Details]
A. Bhalla and I. Lynce and J. Sousa and J. Marques-Silva; (2005) 'Heuristic-Based Backtracking Relaxation for Propositional Satisfiability' In: A. Bhalla and I. Lynce and J. Sousa and J. Marques-Silva; (eds). Springer. [Details]
J. Marques-Silva and K. Sakallah; (2003) 'GRASP - A New Search Algorithm for Satisfiability' In: J. Marques-Silva and K. Sakallah; (eds). Kluwer Academic Publishers. [Details]
I. Lynce and J. Marques-Silva; (2003) 'The Effect of Nogood Recording in DPLL-CBJ SAT Algorithms' In: I. Lynce and J. Marques-Silva; (eds). Springer. , pp.144-158 [Details]
W. Kunz and J. Marques-Silva and S. Malik; (2001) 'SAT and ATPG: Algorithms for Boolean Decision Problems' In: W. Kunz and J. Marques-Silva and S. Malik; (eds). Kluwer Academic Publishers. , pp.309-341 [Details]

Edited Books

J. Marques-Silva and K. Sakallah (Ed.). (2007) 10th International Conference on Theory and Applications of Satisfiability Testing. Springer, LNCS 4501. [Details]

Peer Reviewed Journals

Anton Belov and Mikol\'as Janota and In\^es Lynce and Joao Marques-Silva (2014) 'Algorithms for computing minimal equivalent subformulas'. Artif. Intell, 216 :309-326. Available Online [DOI] [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]
Lucas Cordeiro and Bernd Fischer and Joao Marques-Silva (2012) 'SMT-Based Bounded Model Checking for Embedded ANSI-C Software'. IEEE Transactions on Software Engineering, 38 (4):957-974. [Details]
Joao Marques-Silva (2012) 'Computing Minimally Unsatisfiable Subformulas: State of the Art and Future Directions'. Journal of Multiple-Valued Logic and Soft Computing, 19 (1-3):163-183. [Details]
Anton Belov and Joao Marques-Silva (2012) 'MUSer2: An Efficient MUS Extractor'. JSAT, 8 (1/2):123-128. [Details]
Huan Chen and Joao Marques-Silva (2012) 'TG-Pro: A SAT-based ATPG System'. JSAT, 8 (1/2):83-88. [Details]
Mikol\'as Janota and In\^es Lynce and Vasco M. Manquinho and Joao Marques-Silva (2012) 'PackUp: Tools for Package Upgradability Solving'. JSAT, 8 (1/2):89-94. [Details]
Florian Letombe and Joao Marques-Silva (2012) 'Hybrid Incremental Algorithms for Boolean Satisfiability'. International Journal on Artificial Intelligence Tools, 21 (6). [Details]
Anton Belov and In\^es Lynce and Joao Marques-Silva (2012) 'Towards efficient MUS extraction'. AI Communications, 25 (2):97-116. [Details]
Antonio Morgado, Federico Heras, Mark Liffiton, Jordi Planes, Joao Marques-Silva (2013) 'Iterative and core-guided MaxSAT solving: A survey and assessment'. Constraints, 18 (4):478-534. [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. Available Online [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. Available Online [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. Available Online [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. Available Online [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. Available Online [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]
 

Conference Publications

Graca, A,Marques-Silva, J,Lynce, I,Oliveira, AL (2011) ANNALS OF OPERATIONS RESEARCH Haplotype inference with pseudo-Boolean optimization , pp.137-162 [DOI] [Details]
Ant\'onio Morgado and Federico Heras and Joao Marques-Silva (2013) Model-Guided Approaches for MaxSAT Solving LPAR , pp.931-938 Available Online [Details]
Antonio Morgado and Federico Heras and Joao Marques-Silva (2013) Model-Guided Approaches for MaxSAT Solving ICTAI Washington DC, USA, , 04-NOV-13 - 06-NOV-13 [Details]
William Klieber and Mikolas Janota and Joao Marques-Silva and Edmund M. Clarke (2013) Solving QBF with Free Variables CP , pp.415-431 Available Online [Details]
Anton Belov and Antonio Morgado and Joao Marques-Silva (2013) SAT-Based Preprocessing for MaxSAT LPAR , pp.96-111 Available Online [Details]
Alexey Ignatiev and Antonio Morgado and Jordi Planes and Joao Marques-Silva (2013) Maximal Falsifiability - Definitions, Algorithms, and Applications LPAR , pp.439-456 Available Online [Details]
Mikol\'as Janota and Radu Grigore and Joao Marques-Silva (2013) On QBF Proofs and Preprocessing LPAR , pp.473-489 Available Online [Details]
Alexey Ignatiev and Mikolas Janota and Joao Marques-Silva (2014) Towards efficient optimization in package management systems ICSE , pp.745-755 Available Online [Details]
Yuri Malitsky and Barry O'Sullivan and Alessandro Previti and Joao Marques-Silva (2014) Timeout-Sensitive Portfolio Approach to Enumerating Minimal Correction Subsets for Satisfiability Problems ECAI , pp.1065-1066 Available Online [Details]
Joao Marques-Silva and Alexey Ignatiev and Antonio Morgado and Vasco M. Manquinho and Ines Lynce (2014) Efficient Autarkies ECAI , pp.603-608 Available Online [Details]
Alexey Ignatiev and Antonio Morgado and Vasco M. Manquinho and Ines Lynce and Joao Marques-Silva (2014) Progression in Maximum Satisfiability ECAI , pp.453-458 Available Online [Details]
Yuri Malitsky and Barry O'Sullivan and Alessandro Previti and Joao Marques-Silva (2014) A Portfolio Approach to Enumerating Minimal Correction Subsets for Satisfiability Problems CPAIOR , pp.368-376 Available Online [Details]
Arie Gurfinkel and Anton Belov and Joao Marques-Silva (2014) Synthesizing Safe Bit-Precise Invariants TACAS , pp.93-108 Available Online [Details]
Anton Belov and Marijn Heule and Joao Marques-Silva (2014) MUS Extraction Using Clausal Proofs SAT , pp.48-57 Available Online [Details]
Joao Marques-Silva and Alessandro Previti (2014) On Computing Preferred MUSes and MCSes SAT , pp.58-74 Available Online [Details]
Alexey Ignatiev and Antonio Morgado and Joao Marques-Silva (2014) On Reducing Maximum Independent Set to Minimum Satisfiability SAT , pp.103-120 Available Online [Details]
Federico Heras and Ant\'onio Morgado and Joao Marques-Silva (2012) An Empirical Study of Encodings for Group MaxSAT Canadian Conference on AI , pp.85-96 [Details]
Anton Belov and Mikol\'as Janota and In\^es Lynce and Joao Marques-Silva (2012) On Computing Minimal Equivalent Subformulas CP , pp.158-174 [Details]
Huan Chen and Mikol\'as Janota and Joao Marques-Silva (2012) QBf-based boolean function bi-decomposition DATE , pp.816-819 [Details]
Ant\'onio Morgado and Mark H. Liffiton and Joao Marques-Silva (2012) MaxSAT-Based MCS Enumeration Haifa Verification Conference , pp.86-101 [Details]
Lucas Bordeaux and Mikol\'as Janota and Joao Marques-Silva and Pierre Marquis (2012) On Unit-Refutation Complete Formulae with Existentially Quantified Variables KR [Details]
Mikol\'as Janota and William Klieber and Joao Marques-Silva and Edmund M. Clarke (2012) Solving QBF with Counterexample Guided Refinement SAT , pp.114-128 [Details]
Ant\'onio Morgado and Federico Heras and Joao Marques-Silva (2012) Improvements to Core-Guided Binary Search for MaxSAT SAT , pp.284-297 [Details]
Anton Belov and Alexander Ivrii and Arie Matsliah and Joao Marques-Silva (2012) On Efficient Computation of Variable MUSes SAT , pp.298-311 [Details]
Lucas Bordeaux and Joao Marques-Silva (2012) Knowledge Compilation with Empowerment SOFSEM , pp.612-624 [Details]
Federico Heras and Antonio Morgado and Jordi Planes and Joao Marques-Silva (2012) Iterative SAT Solving for Minimum Satisfiability ICTAI , pp.922-927 Available Online [Details]
Anton Belov and Huan Chen and Alan Mishchenko and Joao Marques-Silva (2013) Core minimization in SAT-based abstraction DATE , pp.1411-1416 [Details]
Alessandro Previti and Joao Marques-Silva (2013) Partial MUS Enumeration AAAI [Details]
Joao Marques-Silva and Mikolas Janota and Anton Belov (2013) Minimal Sets over Monotone Predicates in Boolean Formulae CAV , pp.592-607 [Details]
William Klieber and Mikolas Janota and Joao Marques-Silva and Edmund M. Clarke (2013) Solving QBF with Free Variables CP , pp.415-431 [Details]
Anton Belov and Matti Jarvisalo and Joao Marques-Silva (2013) Formula Preprocessing in MUS Extraction TACAS , pp.108-123 [Details]
Joao Marques-Silva and Federico Heras and Mikolas Janota and Alessandro Previti and Anton Belov (2013) On Computing Minimal Correction Subsets IJCAI [Details]
Mikolas Janota and Joao Marques-Silva (2013) On Propositional QBF Expansions and Q-Resolution SAT , pp.67-82 [Details]
Anton Belov and Norbert Manthey and Joao Marques-Silva (2013) Parallel MUS Extraction SAT , pp.133-149 [Details]
Alexey Ignatiev and Mikolas Janota and Joao Marques-Silva (2013) Quantified Maximum Satisfiability: - A Core-Guided Approach SAT , pp.250-266 [Details]
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 Available Online [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]
         

Dissertations/Theses

J. Marques-Silva; (1995) Search Algorithms for Satisfiability Problems in Combinational Switching Circuits. Dissertations/Theses [Details]
                                                                             

Research

Research Interests

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.