Mark Liffiton

Fast, Flexible MUS Enumeration
Mark H. Liffiton, Alessandro Previti, Ammar Malik, and João Marques-Silva
Constraints, 21(2):223-250, 2016.

Iterative and core-guided MaxSAT solving: A survey and assessment
Antonio Morgado, Federico Heras, Mark H. Liffiton, Jordi Planes, and João Marques-Silva
Constraints, 18(4):478-534, 2013.

A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Subformulas
Mark H. Liffiton, Maher Mneimneh, Inês Lynce, Zaher Andraus, João Marques-Silva, and Karem Sakallah
Constraints, 14(4):415-442, 2009. [published online August, 2008]

Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints
Mark H. Liffiton and Karem A. Sakallah
Journal of Automated Reasoning, 40(1):1-33, January 2008. [published online September, 2007]

Finding graph decompositions via SAT
Wenting Zhao, Mark H. Liffiton, Peter G. Jeavons, and Dan Roberts
in Proc. 29^th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2017), November 2017.

Parallelizing Partial MUS Enumeration
Wenting Zhao and Mark H. Liffiton
in Proc. 28^th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2016), 464-471, November 2016.

Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets
Bernard Blackham, Mark H. Liffiton, and Gernot Heiser
in Proc. 20^th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2014), 169-178, April 2014.

Enumerating Infeasibility: Finding Multiple MUSes Quickly
Mark H. Liffiton and Ammar Malik
in Proc. 10^th International Conference on Integration of Artificial Intelligence (AI) and Operations Research (OR) techniques in Constraint Programming (CPAIOR-2013), 160-175, May 2013.

MaxSAT-Based MCS Enumeration
Antonio Morgado, Mark H. Liffiton, and João Marques-Silva
in Proc. 8^th International Haifa Verification Conference (HVC-2012), 86-101, November 2012.

A Cardinality Solver: More Expressive Constraints for Free (Poster Presentation)
Mark H. Liffiton and Jordyn C. Maglalang
in Proc. 15^th International Conference on Theory and Applications of Satisfiability Testing (SAT-2012), 485-486, June 2012.

Generalizing Core-Guided Max-SAT
Mark H. Liffiton and Karem A. Sakallah
in Proc. 12^th International Conference on Theory and Applications of Satisfiability Testing (SAT-2009), 481-494, June 2009.

Reveal: A Formal Verification Tool for Verilog Designs
Zaher S. Andraus, Mark H. Liffiton, and Karem A. Sakallah
in Proc. 15^th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-2008), 343-352, November 2008.

Searching for Autarkies to Trim Unsatisfiable Clause Sets
Mark H. Liffiton and Karem A. Sakallah
in Proc. 11^th International Conference on Theory and Applications of Satisfiability Testing (SAT-2008), 182-195, May 2008.

Improved Design Debugging using Maximum Satisfiability
Sean Safarpour, Mark H. Liffiton, Hratch Mangassarian, Andreas Veneris, and Karem A. Sakallah
in Proc. 6^th International Conference on Formal Methods in Computer-Aided Design (FMCAD-2007), 13-19, November 2007.

Refinement Strategies for Verification Methods Based on Datapath Abstraction
Zaher S. Andraus, Mark H. Liffiton, and Karem A. Sakallah
in Proc. 11^th Asia and South Pacific Design Automation Conference (ASP-DAC-2006), 19-24, January 2006.

Identifying Conflicts in Overconstrained Temporal Problems
Mark H. Liffiton, Michael D. Moffitt, Martha E. Pollack, and Karem A. Sakallah
in Proc. 19^th International Joint Conference on Artificial Intelligence (IJCAI-05), 205-211, August 2005.

On Finding All Minimally Unsatisfiable Subformulas
Mark H. Liffiton and Karem A. Sakallah
in Proc. 8^th International Conference on Theory and Applications of Satisfiability Testing (SAT-2005), 173-186, June 2005.

Exploiting Structure in Symmetry Detection for CNF
Paul T. Darga, Mark H. Liffiton, Karem A. Sakallah, and Igor L. Markov
in Proc. 41^st IEEE/ACM Design Automation Conference (DAC-04), 530-534, June 2004.

CEGAR-Based Formal Hardware Verification: A Case Study
Zaher S. Andraus, Mark H. Liffiton, and Karem A. Sakallah
CSE-TR-531-07, University of Michigan, May 2007.

From Max-SAT to Min-UNSAT: Insights and Applications
Mark H. Liffiton, Zaher S. Andraus, and Karem A. Sakallah
CSE-TR-506-05, University of Michigan, February 2005.