Matti Jarvisalo Matti Järvisalo

[News and Highlights] [Research] [Publications] [Activities] [Teaching]

Professor of Computer Science Principal Investigator Constraint Reasoning and Optimization Docent Department of Computer Science Faculty of Science University of Helsinki D.Sc.(Tech.), Lic.Sc.(Tech.), M.Sc.(Tech.) Helsinki University of Technology (today Aalto U.)

Postal Address: Department of Computer Science / HIIT P.O. Box 68 FI-00014 University of Helsinki Finland Office: Room A312, 3rd floor of Exactum, wing A Pietari Kalmin katu 5 Telephone: +358 50 3199 248 Email: matti.jarvisalohelsinki.fi

I lead the Constraint Reasoning and Optimization Group at the University of Helsinki.

News

See also recent work for new publications. I'm chairing the KR 2023 Applications and Systems track (with Francesco Ricca) and the 14th International Workshop on Pragmatics of SAT (with Daniel Le Berre). In 2023, on the PCs of IJCAI, CADE, SAT, SoCS. I am editorial board member of Journal of Automated Reasoning and Journal on Satisfiability, Boolean Modeling and Computation. My Academy of Finland project Declarative Boolean Optimization: Pushing the Envelope (9/2019-8/2023) is funded under the Academy Research Project for Early-Career Researchers scheme. Further activities are listed here. Earlier Highlights I was promoted to (Full) Professor starting 1/2022. I gave an online ECAI 2020 tutorial on advances in maximum satisfiability together with Jeremias Berg and Ruben Martins. I gave an invited talk at the 4th Workshop on Advances in Argumentation In Artificial Intelligence, Italy/Online. Our JAIR article Clause Elimination for SAT and QSAT has been selected as the winner of the 2019 IJCAI-JAIR Best Paper Prize as an outstanding paper published in JAIR in the preceding five calendar years. My Academy of Finland project Decision Procedures for the Polynomial Hierarchy, Boolean Optimization, and Model Counting (9/2014-8/2019) was funded under the Academy Research Fellow scheme. I gave a keynote talk at 2nd International Workshop on Systems and Algorithms for Formal Argumentation (SAFA 2018), Poland. My project Harnessing Constraint Reasoning for Structure Discovery ran for the years 2015-2018 under the three-year research project funding scheme of the University of Helsinki. I was a member of the COIN Finnish Centre of Excellence in Computational Inference Research (2012-2017). I served on the steering committee of SAT during 2013-2017. Invited talk at IJCAI-16: Early Career Spotlight I gave a AAAI 2016 tutorial Algorithms for Maximum Satisfiability with Applications to AI together with Fahiem Bacchus. I was PC Chair of SAT 2013 - 16th International Conference on Theory and Applications of Satisfiability Testing, July 8-12 2013 in Helsinki, Finland. I was conferred the title Adjunct Professor (dosentti in Finnish) in computer science at University of Helsinki in May 2012. I received the Best Researcher Award in 2011 by the Department of Computer Science at University of Helsinki. I was the PI of an Academy of Finland Postdoctoral project during 2010-2013. During April-September 2009 I visited Prof. Armin Biere's Institute for Formal Models and Verification at Johannes Kepler University Linz, Austria. I defended my doctoral thesis Structure-Based Satisfiability Checking: Analyzing and Harnessing the Potential in November 2008.

M. Järvisalo, A. Van Gelder (eds.), LNCS 7962, Springer, 2013.

Research

Research Interests

Boolean satisfiability and generalizations, decision procedures, constraint satisfaction, combinatorial/discrete optimization, automated reasoning, artificial intelligence, operations research, knowledge representation, complexity of reasoning, computational aspects of argumentation, probabilistic graphical models, structure discovery, ...

Awards and Honors

• 1st (track 2) and 2nd (track 1) places in Model Counting Competition 2022
• University of Helsinki Outstanding Thesis Award of the Doctoral School in Natural Sciences 2022 Award to my PhD student Kari Rantanen
• 1st place in tracks 1, 2 and 4 in Model Counting Competition 2021
• Best Finnish PhD Thesis in Computer Science Award 2021 (by Finnish Information Processing Association) to my PhD student Andreas Niskanen
• Vienna Center of Logic and Algorithms (VCLA) Outstanding Master Thesis Award 2021 to my MSc student Tuukka Korhonen
• Association for Constraint Programming (ACP) Doctoral Research Award 2020 to my PhD student Jeremias Berg
• 2019 IJCAI-JAIR Best Paper Prize
• ICCMA 2019 Best Solver (both main track and dynamic track)
• University of Helsinki 2019 Doctoral Dissertation Award to my PhD student Jeremias Berg
• PGM 2018 Best Student Paper Award to my PhD student Kari Rantanen for our joint paper
• CP 2017 Distinguished Paper Award
• IJCAI 2016 Early Career Spotlight as one of 22 (6 within Europe) most active early career researchers in all representative areas of AI.
• ECAI 2016 Runner-Up Best Student Paper Award to my PhD student Andreas Niskanen for our joint paper
• Best solver at MaxSAT Evaluation 2015 on industrial and crafted weighted partial MaxSAT instances
• ICCMA 2015 Honorary Mention at
• KR 2012 Distinguished Student Paper Prize
• 2011 Best Researcher Award< at Department of Computer Science, University of Helsinki.
• Runner-up for the CP 2007 Best Paper Award
• ICLP 2007 Best Student Paper Award

Projects

• Declarative Boolean Optimization: Pushing the Envelope (9/2019-8/2023; PI) funded by Academy of Finland (Academy project funding for early-career researchers)
• Symbolic Reasoning for Formally Verified and Explainable AI (2020-2022; PI) funded by Academy of Finland (ICT 2023 Autonomous Everything)
• Decision Procedures for the Polynomial Hierarchy, Boolean Optimization, and Model Counting (9/2014-8/2019; PI), funded by Academy of Finland (Academy Research Fellow funding scheme)
• Harnessing Constraint Reasoning for Structure Discovery (2015-2018; PI), Research Funds of the University of Helsinki (Three-year Research Projects funding scheme)
• Extending the Reach of Boolean Constraint Reasoning (1/2010-4/2013; PI), Academy of Finland (Postdoctoral Project funding scheme)

• Finnish Centre of Excellence in Computational Inference Research COIN (2012-2017), Academy of Finland (member)
• Lightweight Formal Methods for Distributed Component-based Embedded Systems (2009), Tekes (member)
• Methods for Constructing and Solving Large Constraint Models (2008-2009), Academy of Finland (member)
• Advanced Constraint Programming Techniques for Large Structured Problems (2005-2007), Academy of Finland (member)
• Applications of Rule-Based Constraint Programming (2002-2005), Academy of Finland (member)

Publications

A complete list of my publications with downloadable papers and bibtex entries is available both by year and by type.

External sources:
DBLP entry, Google Scholar profile, Semantic Scholar, Orcid ID 0000-0003-2572-063X (incomplete data), Scopus Author ID 23397451200 (incomplete data).

Some recent work

• Unifying Core-Guided and Implicit Hitting Set based Optimization, IJCAI 2023 [pdf]
• SAT-based Judgment Aggregation, AAMAS 2023 [pdf]
• Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization, CP 2023 [pdf]
• Oracle-Based Local Search for Pseudo-Boolean Optimization, ECAI 2023 [pdf]
• MaxSAT-Based Inconsistency Measurement, ECAI 2023 [pdf]
• Argumentative Reasoning in ASPIC+ under Incomplete Information, KR 2023 [pdf]
• Computing MUS-Based Inconsistency Measures, JELIA 2023 [pdf]
• Incremental Maximum Satisfiability, SAT 2022 [pdf]
• MaxSAT-Based Bi-Objective Boolean Optimization, SAT 2022 [pdf]
• Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization, SAT 2022 [pdf]
• Clause Redundancy and Preprocessing in Maximum Satisfiability, IJCAR 2022 [pdf]
• Computing Stable Argumentative Conclusions under the Weakest-Link Principle in the ASPIC+ Framework, KR 2022 [pdf]
• Algorithms for Reasoning in a Default Logic Instantiation of Assumption-Based Argumentation, COMMA 2022 [pdf]
• Computing Smallest MUSes of Quantified Boolean Formulas, LPNMR 2022 [pdf]
• Maximum Satisfiability, SAT Handbook (2021) [pdf]
• Preprocessing in SAT Solving, SAT Handbook (2021) [pdf]
• SAT Competition 2020, Artificial Intelligence (2021) [pdf]
• Acceptance in Incomplete Argumentation Frameworks, Artificial Intelligence (2021) [pdf]
• Declarative Algorithms and Complexity Results for Assumption-Based Argumentation, J. Artificial Intelligence Research (2021) [pdf]
• Maximal Ancestral Graph Structure Learning via Exact Search, UAI 2021 [pdf]
• Harnessing Incremental Answer Set Solving for Reasoning in Assumption-Based Argumentation, ICLP 2021 [pdf]
• Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters, CP 2021 [pdf]
• Pseudo-Boolean Optimization by Implicit Hitting Sets, CP 2021 [pdf]
• Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT under Changing Weights, CP 2021 [pdf]
• Refined Core Relaxation for Core-Guided MaxSAT Solving, CP 2021 [pdf]

Research-Related Software See here.

Professional Activities

Editorial Board Memberships

• Journal of Automated Reasoning, 2021-
• Journal of Satisfiability, Boolean Modeling and Computation, 2018-

Steering Committee Memberships

• SAT: International Conferences on Theory and Applications of Satisfiability Testing, 2013-2017.

Organization

Competitions:

• Co-organizer, ICCMA 2023: 5th International Competition on Computational Models of Argumentation
• Co-organizer, SAT Competition 2023, 2022, 2021, 2020, 2018, 2017, 2016, 2014, 2013, 2011
• Co-organizer, MaxSAT Evaluation 2023, 2022, 2021, 2020, 2019, 2018, 2017
• Co-organizer, SAT Race 2019
• Co-organizer, SAT Challenge 2012

Conferences:

• Local Chair, FoIKS 2022: 12th International Symposium on Foundations of Information and Knowledge Systems , June 20-23, 2022, Helsinki, Finland
• Local Chair, SAT 2013: 16th International Conference on Theory and Applications of Satisfiability Testing, July 8-12, 2013, Helsinki, Finland
• Co-organizer, SAT-SMT Summer School 2013
• Local organizer, SWAT 2012: 13th Scandinavian Symposium and Workshops on Algorithm Theory, July 4-6, 2012, Helsinki, Finland
• Local Chair, JELIA 2010: 12th European Conference on Logics in Artificial Intelligence, September 13-15, 2010, Helsinki, Finland

Program Committee Chairing, Guest Editorials, Senior PC Memberships

• Applications and Systems Track Chair, KR 2023: 20th International Conference on Principles of Knowledge Representation and Reasoning (together with Francesco Ricca)
• PC Chair, PoS 2023: 14th International Workshop on Pragmatics of SAT (together with Daniel Le Berre)
• PC Chair, PoS 2022: 13th International Workshop on Pragmatics of SAT (together with Daniel Le Berre)
• Senior PC Member, IJCAI 2021: 30th International Joint Conference on Artificial Intelligence
• PC Chair, PoS 2021: 12th International Workshop on Pragmatics of SAT, online (together with Daniel Le Berre)
• Demo Track Chair, IJCAI-PRICAI 2020: 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence, Yokohama, Japan
• PC Chair, PoS 2020: 11th International Workshop on Pragmatics of SAT, Alghero, Italy (together with Daniel Le Berre)
• Senior PC Member, IJCAI-PRICAI 2020: 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence
• PC Chair, PoS 2019: 10th International Workshop on Pragmatics of SAT, Lisbon, Portugal (together with Daniel Le Berre)
• Senior PC Member, IJCAI 2019: 28th International Joint Conference on Artificial Intelligence
• Senior PC Member, AAAI 2019: 33rd AAAI Conference on Artificial Intelligence
• PC Chair, PoS 2018: 9th International Workshop on Pragmatics of SAT, Oxford, UK (together with Daniel Le Berre)
• Senior PC Member, IJCAI 2016: 25th International Joint Conference on Artificial Intelligence
• Guest Editor, Journal of Satisfiability, Boolean Modeling and Computation, Special Issue on the SAT 2014 Competitions and Evaluations, 2015
• PC Chair, SAT 2013: 16th International Conference on Theory and Applications of Satisfiability Testing, Helsinki, Finland (together with Allen Van Gelder)

Program Committee Memberships

• CADE 2023: 29th International Conference on Automated Deduction
• IJCAI 2023: 32nd International Joint Conference on Artificial Intelligence
• SAT 2023: 26th International Conference on Theory and Applications of Satisfiability Testing
• SoCS 2023: 16th Annual Symposium on Combinatorial Search
• IJCAI 2022: 31st International Joint Conference on Artificial Intelligence
• AAAI 2022: 36th AAAI Conference on Artificial Intelligence
• SAT 2022: 25th International Conference on Theory and Applications of Satisfiability Testing
• FoIKS 2022: 12th International Symposium on Foundations of Information and Knowledge Systems
• ICLP 2022: 38th International Conference on Logic Programming
• KR 2022: 19th International Conference on Principles of Knowledge Representation and Reasoning
• SAC 2022: 37th ACM/SIGAPP Symposium On Applied Computing KRR track
• SAFA 2022: 4th International Workshop on Systems and Algorithms for Formal Argumentation
• AAAI 2021: 35th AAAI Conference on Artificial Intelligence
• ICAART 2021: 13th International Conference on Agents and Artificial Intelligence
• ICLP 2021: 37th International Conference on Logic Programming applications track
• KR 2021: 18th International Conference on Principles of Knowledge Representation and Reasoning
• SAC 2021: 36th ACM/SIGAPP Symposium On Applied Computing KRR track
• SAT 2021: 24th International Conference on Theory and Applications of Satisfiability Testing
• SoCS 2021: 14th Annual Symposium on Combinatorial Search
• ICTAI 2020: 32nd IEEE International Conference on Tools with Artificial Intelligence SAT/CSP Track
• SoCS 2020: 13th Annual Symposium on Combinatorial Search
• SAT 2020: 23rd International Conference on Theory and Applications of Satisfiability Testing
• AAAI 2020: 34th AAAI Conference on Artificial Intelligence
• CPAIOR 2020: 17th International Conference on Integration of AI and OR Techniques in Constraint Programming
• ECAI 2020: 24th European Conference on Artificial Intelligence
• FoIKS 2020: 11th International Symposium on Foundations of Information and Knowledge Systems
• SAC 2020: 35th ACM/SIGAPP Symposium On Applied Computing KRR track
• SAFA 2020: 3rd International Workshop on Systems and Algorithms for Formal Argumentation
• ICTAI 2019: 31st IEEE International Conference on Tools with Artificial Intelligence SAT/CSP Track
• SoCS 2019: 12th Annual Symposium on Combinatorial Search
• UAI 2019: 35th Conference on Uncertainty in Artificial Intelligence
• SAT 2019: 22nd International Conference on Theory and Applications of Satisfiability Testing
• CPAIOR 2019: 16th International Conference on Integration of AI and OR Techniques in Constraint Programming
• ICML 2019: 36th International Conference on Machine Learning ("Reviewer")
• NeurIPS 2019: 33rd Annual Conference on Neural Information Processing Systems ("Reviewer")
• SAC 2019: 34th ACM/SIGAPP Symposium On Applied Computing KRR track
• AAAI 2018: 32nd AAAI Conference on Artificial Intelligence
• CPAIOR 2018: 15th International Conference on Integration of AI and OR Techniques in Constraint Programming
• ICTAI 2018: 30th IEEE International Conference on Tools with Artificial Intelligence SAT/CSP Track
• IJCAI-ECAI 2018: 27th International Joint Conference on Artificial Intelligence and the 23rd European Conference on Artificial Intelligence
• NeurIPS 2018: 32nd Annual Conference on Neural Information Processing Systems ("Reviewer")
• SAT 2018: 21st International Conference on Theory and Applications of Satisfiability Testing
• SAC 2018: 33rd ACM/SIGAPP Symposium On Applied Computing KRR track
• RCRA 2018: 25th RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
• CP/ICLP/SAT DP 2017: CP/ICLP/SAT Doctoral Program 2017
• ICTAI 2017: 29th IEEE International Conference on Tools with Artificial Intelligence SAT/CSP Track
• AAAI 2017: 31st AAAI Conference on Artificial Intelligence
• CPAIOR 2017: 14th International Conference on Integration of AI and OR Techniques in Constraint Programming
• RCRA 2017: 24th RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
• IEA/AIE 2017: 30th International Conference on Industrial, Engineering, and Other Applications of Applied Intelligent Systems Special Track on Applications of Argumentation
• SAT 2016: 19th International Conference on Theory and Applications of Satisfiability Testing
• AAAI 2016: 30th AAAI Conference on Artificial Intelligence
• AAAI 2016 Beyond NP: AAAI-16 Workshop on Beyond NP
• SAT PoS 2016: 7th Workshop on Pragmatics of SAT
• CP 2016 DP: 22nd International Conference on Principles and Practice of Constraint Programming Doctoral Program
• IJCAI 2015: 24th International Joint Conference on Artificial Intelligence Main Track
• IJCAI 2015 ML: 24th International Joint Conference on Artificial Intelligence Machine Learning Track
• AAAI 2015: 29th AAAI Conference on Artificial Intelligence
• SAT 2015: 18th International Conference on Theory and Applications of Satisfiability Testing
• RCRA 2015: 22nd RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
• CP 2015 DP: 21st International Conference on Principles and Practice of Constraint Programming Doctoral Program
• ECAI 2014: 21st European Conference on Artificial Intelligence
• SAT 2014: 17th International Conference on Theory and Applications of Satisfiability Testing
• ECAI CoCoMile 2014: 3rd Workshop on Combining Constraint Solving with Mining and Learning
• ICLP-SAT LaSh 2014: 4th International Workshop on Logic and Search
• CP 2014 DP: 20th International Conference on Principles and Practice of Constraint Programming Doctoral Program
• IJCAI 2013: 23rd International Joint Conference on Artificial Intelligence
• AAAI CoCoMile 2013: 2nd Workshop on Combining Constraint Solving with Mining and Learning
• RCRA 2013: 20th RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
• ICLP 2013 DC: 9th ICLP Doctoral Consortium
• AAAI 2012: 26th AAAI Conference on Artificial Intelligence
• ECML-PKDD 2012: European Conference on Machine Learning and Principles and Practice of Knowledge Discovery in Databases
• ECAI CoCoMile 2012: 1st Workshop on Combining Constraint Solving with Mining and Learning
• ICLP LoCoCo 2012: 3rd Workshop on Logics for Component Configuration
• KR NMR 2012: 14th International Workshop on Non-Monotonic Reasoning
• SAT PoS 2012: 3rd Workshop on Pragmatics of SAT
• IJCAI 2011: 22nd International Joint Conference on Artificial Intelligence
• SAT PoS 2011: 2nd Workshop on Pragmatics of SAT
• SAT LoCoCo 2010: 1st Workshop on Logics for Component Configuration

Reviewing

Reviewed scientific manuscripts for journals Journal of Artificial Intelligence Research, Journal of Universal Computer Science, Artificial Intelligence, Annals of Mathematics and Artificial Intelligence, International Journal of Approximate Reasoning, Theory and Practice of Logic Programming, IEEE Intelligent Systems, Information Sciences, Journal of Automated Reasoning, Journal of Experimental and Theoretical Artificial Intelligence, Journal on Satisfiability, Boolean Modeling and Computation, AI Communications, Journal of Logic and Computation (and various conferences).

Teaching

To prospective students: If you're interested in conducting research aiming at a thesis under my guidance, feel free to contact me via email. To get a feel for possible topic areas, see my research interests above. You can also have a look at my publications.

Teaching

Lectured (teacher-in-charge of) the following courses at the University of Helsinki:

• Bachelor's Thesis Project, spring 2023 (supervisor)
• Seminar on Automated Reasoning and Optimization (5 ECTS), spring 2023
• Combinatorial Optimization (5 ECTS), autumn 2022
• Automated Logical Reasoning (5 ECTS), spring 2022
• Seminar on Logic-Enabled Verified and Explainable AI (5 ECTS), autumn 2021
• Bachelor's Thesis Project, autumn 2021 (supervisor)
• Automated Logical Reasoning (5 ECTS), spring 2021
• Combinatorial Optimization (5 ECTS), autumn 2020
• Bachelor's Thesis Project, spring 2020 (supervisor)
• Seminar on Model Checking (5 ECTS), autumn 2019
• Automated Logical Reasoning (5 ECTS), spring 2019
• Seminar on Discrete Algorithms (5 ECTS), spring 2019 (with Juha Kärkkäinen and Veli Mäkinen)
• Combinatorial Optimization (5 ECTS), autumn 2018
• Seminar on Automated Planning (5 ECTS), autumn 2018
• Seminar on Applied Discrete Algorithms A (5 ECTS), spring 2018 (with Juha Kärkkäinen and Veli Mäkinen)
• Bachelor's Thesis Project, spring 2018 (supervisor)
• Seminar on Computational Social Choice (3 ECTS), autumn 2016.
  MSc-level seminar course based on the recent Handbook of Computational Social Choice. Topics included voting theory, fair allocation, coalition formation (matchings and hedonic games), and automated theorem discovery.
• Satisfiability, Boolean Modeling and Computation (5 ECTS), spring 2016.
  Central computational aspects of SAT, focusing on techniques that are important for modern real-world applications of SAT. Topics included: basics of propositional logic and computation; modern SAT solver algorithms and search techniques; preprocessing; modelling real-world problems as SAT; building complex SAT-based procedures for Boolean optimization and other search problems beyond NP.
• Seminar on Tractability (3 ECTS), autumn 2015.
  MSc-level seminar course based on the recent book Tractability: Practical Approaches to Hard Problems. Fundamental concepts and state-of-the-art techniques to tame intractability. Topics included: tractability in terms of graphical structures underlying problems, language restrictions, approximation algorithms, and kernelization methods, as well as utilizing heuristics in modern SAT-solvers.
• Satisfiability, Boolean Modeling and Computation (3 ECTS), intensive course in May 2015
  Central computational aspects of Boolean satisfiability (SAT), focusing on techniques that are important for modern real-world applications of SAT.
• Seminar: Constraint Solving Meets Machine Learning and Data Mining (3 ECTS), spring 2013.
  A snapshot into the current state of forefront research in the intersection of constraint solving, machine learning and data mining.
• Discrete Optimization Project (2 ECTS), spring 2012.
  Independent hands-on project work in the areas of constraint satisfaction and discrete optimization, involving problem modelling, algorithm implementation, and/or practical performance evaluation of search and optimization algorithms within a chosen topic.
• Discrete Optimization (3 ECTS), autumn 2011.
  Combinatorial search spaces and optimization problems. Exhaustive and heuristic methods. Linear and integer programming.
• Seminar on Boolean Constraint Reasoning (3 ECTS), autumn 2010.
  Theoretical and applied aspects of Boolean satisfiability, SAT solvers and their extensions.

Previously, I've been involved as TA on:

• Advanced Course in Computational Logic, Helsinki University of Technology, spring 2009, 2008, 2007 2006
  Modal logics, applications of temporal logics (LTL, CTL) in concurrent and distributed systems
• Computational Complexity Theory, Helsinki University of Technology, autumn 2008, 2007, 2006, 2005, 2004, 2003
  NP-completeness, randomized algorithms, cryptography, approximation algorithms, parallel algorithms, polynomial hierarchy, PSPACE-completeness
• Logic in Computer Science: Foundations, Helsinki University of Technology, spring 2007, autumn 2003
  Propositional logic and predicate logic, proof theory and applications
• Introduction to Theoretical Computer Science Y, Helsinki University of Technology, spring 2006
• Introduction to Theoretical Computer Science T spring 2006, 2005, 2004: autumn, spring, 2002: autumn, spring
  Finite automata and regular languages, context-free grammars and pushdown automata, Turing machines
• Seminar on Theoretical Computer Science, Helsinki University of Technology, spring 2003: Propositional Satisfiability Checking Techniques
• Basic Course in Programming L1, Helsinki University of Technology, autumn 2001