J. Marques-Silva, and I. Lynce, "SAT Solvers", Tractability: Practical Approaches to Hard Problems, Cambridge University Press, February 2014.

A. Graca, J. Marques-Silva and I. Lynce, "Haplotype Inference using Propositional Satisfiability", Mathematical Approaches to Polymer Sequence Analysis and Related Problems, Springer, October 2010.

I. Lynce, V. Manquinho and J. Marques-Silva, "Backtracking", Encyclopedia of Computer Science and Engineering, Wiley InterScience, Volume 1, 283-289, January 2009.

J. Marques-Silva, I. Lynce, and S. Malik,
"Conflict-Driven Clause Learning SAT Solvers",
Handbook of Satisfiability,
IOS Press,
February 2009.

**Journals**

R. Martins, S. Joshi, V. Manquinho and I. Lynce, "On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving", Journal on Satisfiability, Boolean Modeling and Computation, Volume 9, Pages 59-81, 2015.

R. Martins, V. Manquinho and I. Lynce, "Improving Linear Search Algorithms with Model-based Approaches for MaxSAT Solving", Journal of Experimental & Theoretical Artificial Intelligence, Volume 27, Issue 5, 2015.

R. Martins, V. Manquinho and I. Lynce, "Deterministic Parallel MaxSAT Solving", International Journal on Artificial Intelligence Tools, Volume 24, Issue 3, 2015.

M. Janota, I. Lynce and J. Marques-Silva, "Algorithms for Computing Backbones of Propositional Formulae", AI Communications, Volume 28, Issue 2, 2015.

A. Belov, M. Janota, I. Lynce and J. Marques-Silva, "Algorithms for Computing Minimal Equivalent Subformulas", Artificial Intelligence Journal, 216: pp. 309-326, 2014.

R. Camacho, P. Carreira, I. Lynce and S. Resendes, "An Ontology-based approach to conflict resolution in Home and Building Automation Systems", Expert Systems With Applications, 41(14): pp. 6161-6173, 2014.

M. Miranda, I. Lynce and V. Manquinho, "Inferring Phylogenetic Trees Using Pseudo-Boolean Optimization", AI Communications, 27(3): pp. 229-243, 2014.

A. Belov, I. Lynce and J. Marques-Silva, "Towards Efficient MUS Extraction", AI Communications, 25(2): pp. 97-116, 2012.

R. Martins, V. Manquinho and I. Lynce, "Parallel Search for Maximum Satisfiability", AI Communications, 25(2): pp. 75-95, 2012.

R. Martins, V. Manquinho and I. Lynce, "An Overview of Parallel SAT Solving", Constraints, 17(3): pp. 304-347, 2012.

J. Argelich, A. Cabiscol, I. Lynce and F. Manya, "Efficient Encodings from CSP into SAT, and from MaxCSP into MaxSAT", Journal of Multiple-Valued Logic and Soft Computing, 19(1-3): pp. 3-23, 2012.

M. Janota, I. Lynce, V. Manquinho and J. Marques-Silva, "PackUp: Tools for Package Upgradability Solving", Journal on Satisfiability, Boolean Modeling and Computation, 8: pp. 89-94, 2012.

J. Marques-Silva, J. Argelich, A. Graca and I. Lynce, "Boolean Lexicographic Optimization: Algorithms & Applications", Annals of Mathematics and Artificial Intelligence, 62 (3): pp. 317-343, 2011

I. Lynce and J. Marques-Silva, "Restoring CSP Satisfiability with MaxSAT", Fundamenta Informaticae, 107 (1-2): pp. 249-266, April 2011.

A. Graca, J. Marques-Silva, I. Lynce and A. Oliveira, "Haplotype Inference with Pseudo-Boolean Optimization", Annals of Operations Research, 184 (1): pp. 137-162, April 2011.

J. Delgado, I. Lynce and V. Manquinho, "Computing the Summed Adjacency Disruption Number between Two Genomes with Duplicate Genes", Journal of Computational Biology, 17(9): pp. 1243-1265, September 2010.

A. Graca, I. Lynce, J. Marques-Silva and A. Oliveira, "Haplotype Inference by Pure Parsimony: a Survey", Journal of Computational Biology, 17(8): pp. 969-992, August 2010.

M. Liffiton, M. Mneimneh, I. Lynce, Z. Andraus, J. Marques-Silva and K. Sakallah, "A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Subformulas", Constraints, 14(4): pp. 415-442, December 2009.

I. Lynce and J. P. Marques-Silva, "Haplotype Inference with Boolean Satisfiability", International Journal on Artificial Intelligence Tools, 17 (2): pp. 355-387, April 2008.

I. Lynce, J. P. Marques-Silva and S. Prestwich, "Boosting Haplotype Inference with Local Search", Constraints, 13 (1): pp. 155-179, 2008.

J. P. Marques-Silva, K. Sakallah and I. Lynce, "Report on the SAT 2007 Conference on Theory and Applications of Satisfiability Testing", AI Magazine, 28(4): pp. 135-136, Winter 2007.

I. P. Gent, C. Jefferson, T. Kelsey, I. Lynce, I. Miguel, P. Nightingale, B. M. Smith, S. A. Tarim, "Search in the Patience Game Black Hole", AI Communications, Special Issue on Constraint Programming for Planning and Scheduling, 20(3): pp. 211-226, September 2007.

I. Lynce and J. P. Marques-Silva, "Random Backtracking in Backtrack Search Algorithms for Satisfiability", Discrete Applied Mathematics, 155 (12): pp. 1604-1612, June 2007.

I. Lynce, "Propositional Satisfiability: Techniques, Algorithms and Applications", AI Communications, Thesis Abstract, 19 (2): pp. 187-189, June 2006.

A. Bhalla, I. Lynce, J. T. de Sousa and J. P. Marques-Silva, "Heuristic-Based Backtracking Relaxation for Propositional Satisfiability", Journal of Automated Reasoning, 35 (1-3): pp. 3-24, October 2005.

I. Lynce and J. P. Marques-Silva, "Efficient Data Structures for Backtrack Search SAT Solvers", Annals of Mathematics and Artificial Intelligence (AMAI), 43 (1): pp. 137-152, January 2005.

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

**Conferences and Workshops**

M. Neves, R. Martins, M. Janota, I. Lynce and V. Manquinho, Exploiting Resolution-Based Representations for MaxSAT Solving. SAT, LNCS, September 2015.

R. Martins, S. Joshi, V. Manquinho and I. Lynce, Incremental Cardinality Constraints for MaxSAT, CP, LNCS, September 2014.

J. Marques-Silva, A. Ignatiev, A. Morgado, V. Manquinho and I. Lynce, Efficient Autarkies, ECAI, IOS, August 2014.

A. Ignatiev, A. Morgado, V. Manquinho, I. Lynce and J. Marques-Silva, Progression in Maximum Satisfiability, ECAI, IOS, August 2014.

R. Martins, V. Manquinho and I. Lynce, Open-WBO: a Modular MaxSAT Solver, SAT, LNCS, July 2014.

R. Martins, V. Manquinho and I. Lynce, Community-based Partitioning for MaxSAT Solving, SAT, LNCS, July 2013.

R. Martins, V. Manquinho and I. Lynce, Model-based Partitioning for MaxSAT Solving, RCRA, June 2013.

A. Belov, M. Janota, I. Lynce and J. Marques-Silva, On Computing Minimal Equivalent Subformulas, CP, LNCS, October 2012.

J. Guerra and I. Lynce, Reasoning over Biological Networks using Maximum Satisfiability, CP, LNCS, October 2012.

R. Martins, V. Manquinho and I. Lynce, On Partitioning for Maximum Satisfiability, ECAI, August 2012.

R. Martins, V. Manquinho and I. Lynce, Clause Sharing in Deterministic Parallel Maximum Satisfiability, RCRA, June 2012.

M. Janota, I. Lynce and J. Marques-Silva, Experimental Analysis of Backbone Computation Algorithms, RCRA, June 2012.

R. Martins, V. Manquinho and I. Lynce, Clause Sharing in Parallel MaxSAT, LION, LNCS, January 2012.

R. Martins, V. Manquinho and I. Lynce, Exploiting Cardinality Encodings in Parallel Maximum Satisfiability, 23th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'11), November 2011.

J. P. Marques-Silva and I. Lynce, On Improving MUS Extraction Algorithms, SAT'11, LNCS, June 2011.

R. Martins, V. Manquinho and I. Lynce, Improving Search Space Splitting for Parallel SAT Solving, 22th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'10), October 2010.

P. Trezentos, I. Lynce and A. Oliveira, Apt-pbo: Solving the Software Dependency Problem using Pseudo-Boolean Optimization, ASE'10, IEEE, September 2010.

J. P. Marques-Silva, M. Janota and I. Lynce, On Computing Backbones of Propositional Theories, ECAI'10, IOS Press, August 2010.

A. Graca, I. Lynce, J. P. Marques-Silva and A. Oliveira, Efficient and Accurate Haplotype Inference by Combining Parsimony and Pedigree Information, ANB'10, LNCS, August 2010.

C. Peschiera, L. Pulina, A. Tacchella, U. Bubeck, O. Kullmann and I. Lynce, The Seventh QBF Solvers Evaluation (QBFEVAL'10), SAT'10, LNCS, July 2010.

V. Manquinho, R. Martins and I. Lynce, Improving Unsatisfiability-based Algorithms for Boolean Optimization, SAT'10, LNCS, July 2010.

J. Argelich, D. Le Berre, I. Lynce, J. Marques-Silva and P. Rapicault, Solving Linux Upgradeability Problems Using Boolean Optimization, LoCoCo'10, July 2010.

J. Marques-Silva, J. Argelich, A. Graca and I. Lynce, Boolean Lexicographic Optimization, RCRA'10, June 2010.

J. Argelich, A. Cabiscol, I. Lynce and F. Manya, New Insights into Encodings from MaxCSP into Partial MaxSAT, ISMVL'10, IEEE, May 2010.

I. Lynce and J. P. Marques-Silva, Restoring CSP Satisfiability with MaxSAT, EPIA'09, October 2009.

J.Delgado, I. Lynce and V. Manquinho, Computing the Summed Adjacency Disruption Number between Two Genomes with Duplicate Genes using Pseudo-Boolean Optimization, RECOMB-CG'09, LNBI, September 2009.

R. Martins, I. Lynce and V. Manquinho, Preprocessing in Pseudo-Boolean Optimization: An Experimental Evaluation, ModRef'09, September 2009.

D. Pereira, I. Lynce and S. Prestwich, On Improving Local Search for Unsatisfiability, LSCS'09, September 2009.

A. Graca, I. Lynce, J. P. Marques-Silva and A. Oliveira, Haplotype Inference Combining Pedigrees and Unrelated Individuals, WCB'09, September 2009.

J. Argelich, I. Lynce and J.P. Marques Silva, On Solving Boolean Multilevel Optimization Problems, IJCAI'09, July 2009. Benchmarks available here.

J. Argelich, A. Cabiscol, I. Lynce and F. Manya, Sequential Encodings from MAX-CSP into Partial MAX-SAT, SAT'09, LNCS, June 2009.

J. Argelich, A. Cabiscol, I. Lynce and F. Manya, New Encodings from MAX-CSP into Partial MAX-SAT, ISMVL'09, IEEE, May 2009.

J. Argelich and I. Lynce, CNF Instances from the Software Package Installation Problem, RCRA'08, December 2008.

R. Martins and I. Lynce, Effective CNF Encodings for the Towers of Hanoi, Short Paper, LPAR'08, November 2008.

J.P. Marques-Silva, I. Lynce and V. Manquinho, Symmetry Breaking for Maximum Satisfiability, LPAR'08, LNCS 5330, November 2008.

I. Lynce, A. Graca, J. P. Marques-Silva and A. Oliveira, Haplotype Inference with Boolean Constraint Solving: an Overview, 20th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'08), November 2008.

A. Graca, I. Lynce, J. P. Marques-Silva and A. Oliveira, Generic ILP vs Specialized 0-1 ILP for Haplotype Inference, WCB'08, May 2008.

A. Graca, J. P. Marques-Silva, I. Lynce and A. Oliveira, Efficient Haplotype Inference with Combined CP and OR Techniques (Short Paper), CPAIOR'08, LNCS, May 2008.

J. Argelich, A. Cabiscol, I. Lynce and F. Manya, Encoding MAX-CSP into Partial MAX-SAT, ISMVL'08, IEEE, May 2008.

J. Argelich, A. Cabiscol, I. Lynce and F. Manya, Modelling Max-CSP as Partial Max-SAT, SAT'08, LNCS, May 2008.

D. LeBerre and I. Lynce, CSP2SAT4J: A Simple CSP to SAT Translator, Proceedings of the Second International CSP Solver Competition, 2008.

J. P. Marques-Silva, I. Lynce, A. Graca and A. Oliveira, Efficient and Tight Upper Bounds for Haplotype Inference by Pure Parsimony, EPIA'07, LNAI 4874, December 2007.

J.P. Marques-Silva and I. Lynce, Towards Robust CNF Encodings of Cardinality Constraints, CP'07, LNCS 4741, September 2007.

F. Aloul, I. Lynce and S. Prestwich, Symmetry Breaking in Local Search for Unsatisfiability, 7th International Workshop on Symmetry and Constraint Satisfaction Problems, CP'07, September 2007.

R. Martins and I. Lynce, Breaking Local Symmetries in Quasigroup Completion Problems, RCRA'07, July 2007.

S. Prestwich and I. Lynce, Refutation by Randomised General Resolution, AAAI'07 Nectar Track, pages 1667-1670, July 2007.

A. Graca, J. P. Marques-Silva, I. Lynce and A. Oliveira, Efficient Haplotype Inference with Pseudo-Boolean Optimization, Algebraic Biology 2007, LNCS 4545, July 2007.

I. Lynce and J.P. Marques-Silva, Breaking Symmetries in SAT Matrix Models, SAT'07, LNCS 4501, May 2007.

S. Prestwich and I. Lynce, Local Search for Unsatisfiability, SAT'06, LNCS 4121, August 2006.

I. Lynce and J.P. Marques Silva, SAT in Bioinformatics: Making the Case with Haplotype Inference (short paper), SAT'06, LNCS 4121, August 2006.

O. Kullmann, I. Lynce and J.P. Marques Silva, Categorisation of clauses in conjunctive normal forms: Minimally unsatisfiable sub-clause-sets and the lean kernel, SAT'06, LNCS 4121, August 2006.

I. Lynce and J.P. Marques Silva, Efficient Haplotype Inference with Boolean Satisfiability, AAAI'06, July 2006. Get SHIPs software

I. Lynce and J. Ouaknine, Sudoku as a SAT Problem, 9th International Symposium on Artificial Intelligence and Mathematics, January 2006.

I.P. Gent and I. Lynce, A SAT Encoding for the Social Golfer Problem, IJCAI'05 workshop on Modelling and Solving Problems with Constraints, July 2005.

M. N. Mneimneh, I. Lynce, Z. S. Andraus, K. A. Sakallah and J.P. Marques-Silva, A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas, 8th International Conference on Theory and Applications of Satisfiability Testing (SAT'05), LNCS 3569, June 2005.

I. Lynce, A SAT Encoding for the Social Golfer Problem: Benchmark Description, SAT Competition Booklet, 8th International Conference on Theory and Applications of Satisfiability Testing (SAT'05), June 2005.

I. Lynce and J. 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.

I. Lynce and J. P. Marques-Silva, The CQuest SAT solver, 7th International Conference on Theory and Applications of Satisfiability Testing (SAT'04), May 2004.

I. Lynce and J. P. Marques-Silva, On Computing Minimum Unsatisfiable Cores, 7th International Conference on Theory and Applications of Satisfiability Testing (SAT'04), May 2004.

A. Bhalla, I. Lynce, J. T. de Sousa and J. P. Marques-Silva, Heuristic-Based Backtracking for Propositional Satisfiability, 11th Portuguese Conference on Artificial Intelligence (EPIA'03), LNAI 2902, December 2003.

I. Lynce and J. P. Marques-Silva, Probing-Based Preprocessing Techniques for Propositional Satisfiability, 15th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'03), November 2003.

I. Lynce and J. P. Marques-Silva, Propositional Satisfiability Algorithms based on Inference of Constraints, 8th International Joint Conference on Artificial Intelligence (IJCAI'03), Doctoral Consortium, August 2003.

A. Bhalla, I. Lynce, J. T. de Sousa and J. P. Marques-Silva, Heuristic Backtracking Algorithms for SAT, 4th International Workshop on Microprocessor Test and Verification (MTV'03), May 2003.

I. Lynce and J. P. Marques-Silva, On Implementing More Efficient SAT Data Structures, 6th International Conference on Theory and Applications of Satisfiability Testing (SAT'03), May 2003.

G. Audemard, D. Le Berre, O. Roussel, I. Lynce and J. P. Marques-Silva, OpenSAT: An Open Source SAT Software Project, 6th International Conference on Theory and Applications of Satisfiability Testing (SAT'03), May 2003.

I. Lynce and J. P. Marques-Silva, The Effect of Nogood Recording in DPLL-CBJ SAT Algorithms, in O'Sullivan, B. (Ed.), Recent Advances in Constraints, Vol. 2627 of Lecture Notes on Artificial Intelligence, pp. 144-158, Springer Verlag, March 2003.

I. Lynce and J. P. Marques-Silva, Tuning Randomization in Backtrack Search SAT Algorithms, 8th International Conference on Principles and Practice of Constraint Programming (CP'02), Doctoral Programme, LNCS 2470, September 2002.

I. Lynce and J. P. Marques-Silva, Building State-of-the-Art SAT Solvers, 15th European Conference on Artificial Intelligence (ECAI'02), Julho 2002.

I. Lynce and J. P. Marques-Silva, The Effect of Nogood Recording in DPLL-CBJ SAT Algorithms, ERCIM/CologNet Workshop on Constraint Solving and Constraint Logic Programming, June 2002.

I. Lynce and J. P. Marques-Silva, Efficient data structures for backtrack search SAT solvers, 5th International Symposium on the Theory and Applications of Satisfiability Testing (SAT'02), May 2002.

I. Lynce and J. P. Marques-Silva, Complete unrestricted backtracking algorithms for Satisfiability, 5th International Symposium on the Theory and Applications of Satisfiability Testing (SAT'02), May 2002.

L. Drake, A. Frisch, I. Lynce, J. Marques-Silva and T. Walsh, Comparing SAT preprocessing techniques, 9th Workshop on Automated Reasoning, April 2002.

I. Lynce, L. Baptista and J. P. Marques-Silva, Towards Provably Complete Stochastic Search Algorithms for Satisfiability, 10th Portuguese Conference on Artificial Intelligence (EPIA'01), LNAI 2258, December 2001.

I. Lynce and J. P. Marques-Silva, The Puzzling Role of Simplification in Propositional Satisfiability, EPIA'01 Workshop on Constraint Satisfaction and Operational Research Techniques for Problem Solving (EPIA-CSOR'01), December 2001.

I. Lynce and J. P. Marques-Silva, The Interaction Between Simplification and Search in Propositional Satisfiability, CP'01 Workshop on Modeling and Problem Formulation (Formul'01), December 2001.

I. Lynce, Improving Satisfiability Algorithms by Using Search Pruning Techniques, 7th Conference on Principles and Practice of Constraint Programming (CP'01), Doctoral Programme, LNCS 2239, December 2001. (Best student's poster)

I. Lynce, L. Baptista and J.P. Marques-Silva, Unrestricted Backtracking Algorithms for Satisfiability, AAAI 2001 Fall Symposium - Using Uncertainty within Computation, November 2001.

L. Baptista, I. I. Lynce and J.P. Marques-Silva, Complete Search Restart Strategies for Satisfiability, IJCAI Workshop on Stochastic Search Algorithms, August 2001.

I. Lynce and J.P. Marques-Silva, Integrating Simplification Techniques in SAT Algorithms, IEEE Symposium on Logic in Computer Science (LICS'01), Short Paper Session, June 2001.

I. Lynce, L. Baptista and J.P. Marques-Silva,
Stochastic Systematic Search Algorithms for Satisfiability,
LICS Workshop on Theory and Applications of Satisfiability Testing, June 2001.

**Thesis**

Propositional Satisfiability: Techniques, Algorithms and Applications, PhD Thesis, Instituto Superior Técnico, Universidade Técnica de Lisboa, February 2005. (see errata)

Algebraic Simplification Techniques for Propositional Satisfiability, Master Thesis, Instituto Superior Técnico, Universidade Técnica de Lisboa, March 2001.