Mark Liffiton

mliffito -at- domain

Publications

Citation information is available on Google Scholar.

Journals
Fast, Flexible MUS Enumeration
Mark H. Liffiton, Alessandro Previti, Ammar Malik, and João Marques-Silva
Constraints, 21(2):223-250, 2016.
[MARCO software | Algorithm visualization | Springer's published version is available here.]
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.
[Springer's published version is available here.]
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]
[Springer's published version is available here.]
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]
[CAMUS software | Springer's published version is available here.]
Conferences
Parallelizing Partial MUS Enumeration
Wenting Zhao and Mark H. Liffiton
in Proc. 28th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2016), [to appear], November 2016.
Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets
Bernard Blackham, Mark H. Liffiton, and Gernot Heiser
in Proc. 20th 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. 10th 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. 8th 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. 15th 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. 12th 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. 15th 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. 11th 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. 6th 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. 11th 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. 19th 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. 8th International Conference on Theory and Applications of Satisfiability Testing (SAT-2005), 173-186, June 2005.
(For a better (newer, more complete) reference for this work, see the paper in the Journal of Automated Reasoning (2008) above.)
Exploiting Structure in Symmetry Detection for CNF
Paul T. Darga, Mark H. Liffiton, Karem A. Sakallah, and Igor L. Markov
in Proc. 41st IEEE/ACM Design Automation Conference (DAC-04), 530-534, June 2004.
Technical Reports
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.