Recent Publications

Book Chapters

• J. P. Marques-Silva and K. Sakallah, "GRASP - A New Search Algorithm for Satisfiability", A. Kuehlmann (Ed.), The Best of ICCAD: 20 Years of Excellence in Computer Aided Design, Kluwer Academic Publishers, pp. 73-89, 2003.

• I. Lynce and J. P. Marques-Silva, "The Effect of Nogood Recording in DPLL-CBJ SAT Algorithms", B. O'Sullivan (Ed.), Recent Advances in Constraints, Springer Verlag, vol. 2627, pp. 144-158, 2003.

• W. Kunz, J. P. Marques-Silva and S. Malik, "SAT and ATPG: Algorithms for Boolean Decision Problems", S. Hassoun and T. Sasao and R. Brayton (Ed.), Logic Synthesis and Verification, Kluwer Academic Publishers, pp. 309-341, 2001.

• A. Bhalla, I. Lynce, J. T. de Sousa and J. P. Marques-Silva, "Heuristic-Based Backtracking Relaxation for Propositional Satisfiability", Journal of Automated Reasoning, SAT2005 special issue, Accepted, To be published in 2005.

• I. Lynce and J. P. Marques-Silva, "Random Backtracking in Backtrack Search Algorithms for Satisfiability", Discrete Applied Mathematics, Accepted, To be published in 2005.

• I. Lynce and J. P. Marques-Silva, "Efficient Data Structures for Backtrack Search SAT Solvers", Annals of Mathematics and Artificial Intelligence, vol. 43, no. 1-4, pp. 137-152, January 2005.

• V. Manquinho and J. P. Marques-Silva, "Satisfiability-Based Algorithms for Boolean Optimization", Annals of Mathematics and Artificial Intelligence, vol. 40, no. 3-4, March 2004.

• J. P. Marques Silva and L. Guerra e Silva, "Solving Satisfiability in Combinational Circuits", IEEE Design and Test of Computers, vol. 20, no. 4, pp. 16-21, July 2003.

• I. Lynce and J. P. Marques-Silva, "An Overview of Backtrack Search Satisfiability Algorithms", Annals of Mathematics and Artificial Intelligence, vol. 37, no. 3, pp. 307-326, March 2003.

• V. M. Manquinho and J. P. Marques-Silva, "Search Pruning Techniques in SAT-Based Branch-and-Bound Algorithms for the Binate Covering Problem", IEEE Transactions on Computer-Aided Design, vol. 21, no. 5, pp. 505-516, May 2002.

• L. Guerra e Silva, J. P. Marques-Silva, L. M. Silveira and K. A. Sakallah, "Satisfiability Models and Algorithms for Circuit Delay Computation", ACM Transactions on Design Automation of Electronic Systems, vol. 7, no. 1, pp. 137-158, January 2002.

• P. F. Flores, H. C. Neto and J. P. Marques-Silva, "An Exact Solution to the Minimum-Size Test Pattern Problem", ACM Transactions on Design Automation of Electronic Systems, vol. 6, no. 4, pp. 629-644, October 2001.

• A. L. Oliveira and J. P. Marques-Silva, "Efficient Algorithms For The Inference Of Minimum Size DFAs", Machine Learning, vol. 44, no. 1/2, pp. 93-119, July 2001.

• J. P. Marques-Silva and K. A. Sakallah, "GRASP-A Search Algorithm for Propositional Satisfiability", IEEE Transactions on Computers, vol. 48, no. 5, pp. 506-521, May 1999.

• M. A. Riepe, J. P. Marques-Silva, K. A. Sakallah and R. B. Brown, "Ravel-XL: a hardware accelerator for assigned-delay compiled-code logic gate simulation", IEEE Transactions on VLSI Systems, vol. 4, no. 1, pp. 113-129, March 1996.

• João P. Marques-Silva, Improvements to the Implementation of Interpolant-Based Model Checking, Accepted for Publication, Conference on Correct Hardware Design and Verification Methods (CHARME'05), October 2005.

• Vasco Manquinho and João P. Marques-Silva, On Applying Cutting Planes in DLL-Based Algorithms for Pseudo-Boolean Optimization, Accepted for Publication, 8th International Conference on Theory and Applications of Satisfiability Testing (SAT'05), June 2005.

• Maher Mneimneh, Inês Lynce, Zaher Andraus, João P. Marques-Silva and Karem A. Sakallah, A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas, Accepted for Publication, 8th International Conference on Theory and Applications of Satisfiability Testing (SAT'05), June 2005.

• Vasco Manquinho and João P. Marques-Silva, Effective Lower Bounding Techniques for Pseudo-Boolean Optimization, ACM/IEEE Design, Automation and Testing Conference (DATE'05), March 2005.

• Vasco Manquinho and João P. Marques-Silva, Integration of Lower Bound Estimates in Pseudo-Boolean Optimization, 16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'04), November 2004.

• Inês Lynce and João P. Marques-Silva, Hidden Structure in Unsatisfiable Random 3-SAT: an Empirical Study, 16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'04), November 2004.

• Vasco Manquinho and João P. Marques-Silva, Using Lower-Bound Estimates in SAT-Based Pseudo-Boolean, 7th International Conference on Theory and Applications of Satisfiability Testing (SAT'04), May 2004.

• Inês Lynce and João P. Marques-Silva, On Computing Minimum Unsatisfiable Cores, 7th International Conference on Theory and Applications of Satisfiability Testing (SAT'04), May 2004.

• Elsa Carvalho and João P. Marques-Silva, Using Rewarding Mechanisms for Improving Branching Heuristics, 7th International Conference on Theory and Applications of Satisfiability Testing (SAT'04), May 2004.

• Inês Lynce and João P. Marques-Silva, The CQuest SAT Solver, 7th International Conference on Theory and Applications of Satisfiability Testing (SAT'04), May 2004.

• Ateet Bhalla, Inês Lynce, José T. de Sousa and João P. Marques-Silva, Heuristic-Based Backtracking for Propositional Satisfiability, In the Proceedings of the 11th Portuguese Conference on Artificial Intelligence (EPIA'03), December 2003.

• Inês Lynce and João P. Marques-Silva, Probing-Based Preprocessing Techniques for Propositional Satisfiability, in Proceedings of the IEEE International Conference on Tools with Artificial Intelligence (ICTAI'03), November 2003.

• Inês Lynce and João P. Marques-Silva, Propositional Satisfiability Algorithms based on Inference of Constraints, Eighth International Joint Conference on Artificial Intelligence (IJCAI'03), Doctoral Consortium, August 2003.

• Ateet Bhalla, Inês Lynce, José T. de Sousa and João P. Marques-Silva, Heuristic Backtracking Algorithms for SAT, 4th International Workshop on Microprocessor Test and Verification (MTV'03), May 2003.

• Inês Lynce and João P. Marques-Silva, On Implementing More Efficient SAT Data Structures, Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT'03), May 2003.

• Gilles Audemard, Daniel Le Berre, Olivier Roussel, Inês Lynce and João P. Marques-Silva, OpenSAT: An Open Source SAT Software Project, Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT'03), May 2003.

• Inês Lynce and João P. Marques-Silva, Building State-of-the-Art SAT Solvers, in Proceedings of the European Conference on Artificial Intelligence (ECAI), July 2002.

• Inês Lynce and João P. Marques-Silva, Efficient data structures for backtrack search SAT solvers, in Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT), May 2002.

• Inês Lynce and João P. Marques-Silva, Complete unrestricted backtracking algorithms for Satisfiability, in Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT), May 2002.

• Lyndon Drake, Alan Frisch, Inês Lynce, João P. Marques-Silva and Toby Walsh, Comparing SAT preprocessing techniques , in Ninth Workshop on Automated Reasoning, April 2002.

• Inês Lynce, Luís Baptista and João P. Marques-Silva, Towards Provably Complete Stochastic Search Algorithms for Satisfiability, in the Proceedings of the 10th Portuguese Conference on Artificial Intelligence (EPIA), December 2001.

• Inês Lynce and João P. Marques-Silva, The Puzzling Role of Simplification in Propositional Satisfiability, in the EPIA'01 Workshop on Constraint Satisfaction and Operational Research Techniques for Problem Solving (EPIA-CSOR), December 2001.

• Inês Lynce and João P. Marques-Silva, The Interaction Between Simplification and Search in Propositional Satisfiability, in the CP'01 Workshop on Modeling and Problem Formulation (Formul'01), November 2001.

• Inês Lynce and João P. Marques-Silva, Improving SAT Algorithms by Using Search Pruning Techniques, 7th International Conference on Principles and Practice of Constraint Programming (CP) - Doctoral Programme, November 2001. [Best students' poster]

• Inês Lynce, Luís Baptista and João P. Marques-Silva, Unrestricted Backtracking Algorithms for Satisfiability, accepted for publication in the AAAI Fall Symposium Using Uncertainty within Computation (AAAI-UAC), November 2001.

• Luís Baptista, Inês Lynce and João P. Marques-Silva, Complete Search Restart Strategies for Satisfiability, in the IJCAI'01 Workshop on Stochastic Search Algorithms (IJCAI-SSA), August 2001.

• Inês Lynce and João P. Marques-Silva, Integrating Simplification Techniques in SAT Algorithms, in Logic in Computer Science Short Paper Session (LICS-SP), June 2001.

• Inês Lynce, Luís Baptista and João P. Marques-Silva, Stochastic Systematic Search Algorithms for Satisfiability, in the LICS Workshop on Theory and Applications of Satisfiability Testing (LICS-SAT), June 2001.

• José de Sousa, João P. Marques-Silva and Miron Abramovici, A Configurable Hardware/Software Approach to SAT Solving, in the 2001 IEEE Symposium on Field-Programmable Custom Computing Machines (FCCM), May 2001.

• Vasco Manquinho and João P. Marques-Silva, Lower Bounding Techniques for SAT-Based Boolean Optimization, in the Third International Workshop on Integration of AI and OR Techniques (CPAIOR), April 2001.

• Luís Baptista and João P. Marques-Silva, Using Randomization and Learning to Solve Hard Real-World Instances of Satisfiability, in Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming (CP), September 2000.

• João P. Marques-Silva, Algebraic Simplification Techniques for Propositional Satisfiability, in Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming (CP), September 2000.

• Vasco Manquinho and João P. Marques-Silva, Search Pruning Conditions for Boolean Optimization, in Proceedings of the European Conference on Artificial Intelligence (ECAI), August 2000.

• João P. Marques-Silva, On Selecting Problem Instances for Evaluating Satisfiability Algorithms, in ECAI Workshop on Empirical Methods in Artificial Intelligence (ECAI-EMAI), August 2000.

• Luís Baptista and João P. Marques-Silva, The Interplay of Randomization and Learning on Real-World Instances of Satisfiability, in AAAI Workshop on Leveraging Probability and Uncertainty in Computation (AAAI-LPUC), July 2000.

• Vasco Manquinho and João P. Marques-Silva, Conditions for Non-Chronological Backtracking in Boolean Optimization, in AAAI Workshop on Integration of AI and OR Techniques for Combinatorial Optimization (AAAI-AIOR), July 2000.

• João P. Marques-Silva and Karem A. Sakallah, Boolean Satisfiability in Electronic Design Automation, in Proceedings of the IEEE/ACM Design Automation Conference (DAC), June 2000. (This paper is associated with an Embedded Tutorial presented at DAC.)

• Vasco Manquinho and João P. Marques-Silva, On Using Satisfiability-Based Pruning Techniques in Covering Algorithms, in Proceedings of the IEEE/ACM Design, Automation and Test in Europe Conference (DATE), March 2000.

• Joonyoung Kim, Jesse Whittemore, João P. Marques-Silva and Karem A. Sakallah, On Applying Incremental Satisfiability to Delay Fault Testing, in Proceedings of the IEEE/ACM Design, Automation and Test in Europe Conference (DATE), March 2000.

• Fadi A. Aloul, João Marques-Silva and Karem A. Sakallah, An Experimental Study of Satisfiability Search Heuristics, in Proceedings of the IEEE/ACM Design, Automation and Test in Europe Conference (DATE), March 2000.

• Vasco Manquinho and João P. Marques-Silva, On Solving Boolean Optimization with Satisfiability-Based Algorithms, in Sixth International Symposium on Artificial Intelligence and Mathematics, January 2000.

• Joonyoung Kim, João P. Marques-Silva and Karem A. Sakallah, Satisfiability-Based Functional Delay Fault Testing, in Proceedings of the X IFIP International Conference on VLSI (IFIP-VLSI), December 1999.

• João P. Marques-Silva and Luís Guerra e Silva, Algorithms for Satisfiability in Combinational Circuits Based on Backtrack Search and Recursive Learning, in Proceedings of the XII Symposium Integrated Circuits and Systems Design (SBCCI), September/October 1999.

• João P. Marques-Silva, The Impact of Branching Heuristics in Propositional Satisfiability Algorithms, in Proceedings of the 9th Portuguese Conference on Artificial Intelligence (EPIA), September 1999.

• Joonyoung Kim, Jesse Whittemore, João P. Marques-Silva and Karem A. Sakallah, Incremental Boolean Satisfiability and its Application to Delay Fault Testing, in IEEE/ACM International Workshop on Logic Synthesis (IWLS), June 1999.

• João P. Marques-Silva and Luís Guerra e Silva, Algorithms for Satisfiability in Combinational Circuits Based on Backtrack Search and Recursive Learning, in IEEE/ACM International Workshop on Logic Synthesis (IWLS), June 1999.

• Paulo F. Flores, Horácio C. Neto, Krishnendu Chakrabarty and João P. Marques-Silva, Test Pattern Generation for Width Compression in BIST, Proceedings of IEEE International Symposium on Circuits and Systems (ISCAS), May/June 1999.

• João P. Marques-Silva and Thomas Glass, Combinational Equivalence Checking Using Satisfiability and Recursive Learning, in Proceedings of the IEEE/ACM Design, Automation and Test in Europe Conference (DATE), March 1999.

• Luís Guerra e Silva, Luís Miguel Silveira and João P. Marques-Silva, Algorithms for Solving Boolean Satisfiability in Combinational Circuits, in Proceedings of the IEEE/ACM Design, Automation and Test in Europe Conference (DATE), March 1999.

• Paulo F. Flores, Horácio C. Neto and João P. Marques-Silva, On Applying Set Covering Models to Test Set Compaction, in Proceedings of the IEEE 9th Great Lakes Symposium on VLSI (GLSVLSI), March 1999.

• Paulo F. Flores, José C. Costa, Horácio C. Neto, José C. Monteiro and João P. Marques-Silva, Assignment and Reordering of Incompletely Specified Pattern Sequences Targetting Minimum Power Dissipation, in Proceedings of the IEEE International Conference on VLSI Design (VLSI), January 1999.

• Paulo F. Flores, Horácio C. Neto and João P. Marques-Silva, An Exact Solution to the Minimum-Size Test Pattern Problem, in Proceedings of the IEEE International Conference on Computer Design (ICCD), October 1998.

• João P. Marques-Silva, Improving Satisfiability Algorithms by Using Recursive Learning, in Proceedings of the International Workshop on Boolean Problems (IWBP), September 1998.

• Vasco M. Manquinho, Arlindo L. Oliveira and João P. Marques-Silva, Models and Algorithms for Computing Minimum-Size Prime Implicants, in Proceedings of the International Workshop on Boolean Problems (IWBP), September 1998.

• Arlindo L. Oliveira and João P. Marques-Silva, Efficient Search Techniques for the Inference of Minimum Size Finite Automata, in Proceedings of the 1998 IEEE South American Symposium on String Processing and Information Retrieval (SPIRE), September 1998.

• Luís Guerra e Silva, João P. Marques-Silva, Luís M. Silveira and Karem A. Sakallah, Timing Analysis Using Propositional Satisfiability, in Proceedings of the IEEE International Conference on Electronics, Circuits and Systems (ICECS), September 1998.

• Vasco M. Manquinho, João P. Marques-Silva, Arlindo L. Oliveira and Karem A. Sakallah, Satisfiability-Based Algorithms for 0-1 Integer Programming, in IEEE/ACM International Workshop on Logic Synthesis (IWLS), June 1998.

• Paulo F. Flores, Horácio C. Neto and João P. Marques-Silva, An Exact Solution to the Minimum-Size Test Pattern Problem, in IEEE/ACM International Workshop on Logic Synthesis (IWLS), June 1998.

• José C. Costa, Paulo F. Flores, Horácio C. Neto, José C. Monteiro and João P. Marques-Silva, Power Redution in BIST by Exploiting Don't Cares in Test Patterns, in IEEE/ACM International Workshop on Logic Synthesis (IWLS), June 1998.

• Luís Guerra e Silva, João P. Marques-Silva, Luís M. Silveira and Karem A. Sakallah, Realistic Delay Modeling in Satisfiability-Based Timing Analysis, in Proceedings of the IEEE International Symposium on Circuits and Systems (ISCAS), May 1998.

• Paulo F. Flores, Horácio C. Neto, Krishnendu Chakrabarty and João P. Marques-Silva, A Model and Algorithm for Computing Minimum-Size Test Patterns, in IEEE European Test Workshop (ETW), May 1998.

• José C. Costa, Paulo F. Flores, Horácio C. Neto, José C. Monteiro and João P. Marques-Silva, Exploiting Don't Cares in Test Patterns to Reduce Power During BIST, in IEEE European Test Workshop (ETW), May 1998.

• Paulo F. Flores, Horácio C. Neto, Krishnendu Chakrabarty and João P. Marques-Silva, A Model and Algorithm for Computing Minimum-Size Test Patterns, in Proceedings of the Cadence Technical Conference (CTC), May 1998.

• José C. Costa, Paulo F. Flores, José C. Monteiro and João P. Marques-Silva, Power Reduction in BIST by Exploiting Don't Cares in Test Patterns, in Proceedings of the Cadence Technical Conference (CTC), May 1998.

• João P. Marques-Silva, Integer Programming Models for Optimization Problems in Test Generation, in IEEE/ACM Proceedings of the Asian and South Pacific Design Automation Conference (ASP-DAC), February 1998.

• João P. Marques-Silva, An Overview of Backtrack Search Satisfiability Algorithms, in Fifth International Symposium on Artificial Intelligence and Mathematics, January 1998.

• Luís Guerra e Silva, João P. Marques-Silva, Luís M. Silveira and Karem A. Sakallah, Satisfiability Models and Algorithms for Circuit Delay Computation, in ACM Workshop on Timing Issues in the Specification and Synthesis of Digital Systems (TAU), December 1997.

• Vasco M. Manquinho, Paulo F. Flores, João P. Marques-Silva and Arlindo L. Oliveira, Prime Implicant Computation Using Satisfiability Algorithms, in Proceedings of the IEEE International Conference on Tools with Artificial Intelligence (ICTAI), November 1997.

• José Carlos Monteiro and João P. Marques-Silva, Testability Analysis of Circuits Using Data-Dependent Power Management Techniques, in Proceedings of IFIP VLSI: Integrated Systems on Silicon, August 1997.

• Arlindo L. Oliveira and João P. Marques-Silva, Efficient Search Techniques for the Inference of Minimum Sized Finite State Machines, in Workshop on Automata Induction, Grammatical Inference, and Language Acquisition, July 1997.

• João P. Marques-Silva and Karem A. Sakallah, Robust Search Algorithms for Test Pattern Generation, in Proceedings of the IEEE Fault-Tolerant Computing Symposium, June 1997.

• João P. Marques-Silva, José Carlos Monteiro and Karem A. Sakallah, Test Pattern Generation for Circuits Using Power Management Techniques, in IEEE European Test Workshop, May 1997.

• João P. Marques-Silva, On Computing Minimum Size Prime Implicants, in IEEE/ACM International Workshop on Logic Synthesis, May 1997.

• João P. Marques-Silva and Arlindo L. Oliveira, Improving Satisfiability Algorithms with Dominance and Partitioning, in IEEE/ACM International Workshop on Logic Synthesis, May 1997.

• Joonyoung Kim, João P. Marques-Silva, Hamid Savoj and Karem A. Sakallah, RID-GRASP: Redundancy Identification and Removal Using Grasp, in IEEE/ACM International Workshop on Logic Synthesis, May 1997.

• João P. Marques-Silva, On Computing Minimum Size Prime Implicants, in Proceedings of the Cadence Technical Conference, May 1997.

• Arlindo L. Oliveira and João P. Marques-Silva, Reduction of Loop Free Finite State Machines, in Proceedings of the Cadence Technical Conference, May 1997.

• Joonyoung Kim, João P. Marques-Silva, Hamid Savoj and Karem A. Sakallah, RID-GRASP: Redundancy Identification and Removal Using Grasp, in Proceedings of the Cadence Technical Conference, May 1997.

• João P. Marques-Silva and Karem A. Sakallah, "GRASP -- A New Search Algorithm for Satisfiability," in Proceedings of IEEE/ACM International Conference on Computer-Aided Design, November 1996.

• João P. Marques-Silva and Karem A. Sakallah, "Conflict Analysis in Search Algorithms for Propositional Satisfiability," in Proceedings of the IEEE International Conference on Tools with Artificial Intelligence, November 1996.