EECS 4401/5326: Artificial Intelligence

EECS 4401/5326: Artificial Intelligence

Course details

  • Location: DB 0005
  • Day/time: TH
  • Instructor's office hours: TH 11:30 -- 12:30, LAS 3052B

Course description and Learning Outcomes

Traditionally, this course is devoted to selected special topics in Artificial Intelligence (AI). In its 2019 edit, the selected topic is automated reasoning (AR).

The design of any complex AI agent must consider the acquisition of knowledge and its representation. It is the ability to efficiently reason about such knowledge within the framework of a selected representation that makes the efficient implementation of fundamental cognitive tasks possible, tasks such as planning and scheduling. The main objective of AR is to develop efficient algorithms for automated reasoning and to use them for specific AI applications.

Two fundamental AR approaches will be discussed: resolution-based and satisfiability-based AR algorithms. The resolution theory is a mature AI discipline with a long list of accomplishments and considerable research base. It is well-known to undergraduate AI students exposed to logical approach to knowledge representation and reasoning. This course will discuss resolution based AR systems and their applications in more detail.

The second approach to AR covered in this course is based on propositional satisfiability (SAT). SAT problem is easy to formulate but its theoretical properties are of great significance to the theoretical as well as applied computer science. Researchers and practitioners in areas such as theoretical computer science, AI, and software and hardware verification benefit not only from the theoretical advancements in SAT but also from practical tools that the SAT community is continuously developing and offering as powerful and versatile problem solving tools. Many "classical" problems in AI can be conveniently formulated as SAT instances and practically solved using the so-called SAT solvers. For instance, successful applications of SAT algorithms have been reported in the area of planning, scheduling, diagnosis, knowledge representation and reasoning, games, to name just a few of the subareas of AI. Furthermore, SAT-based tools are routinely used by industry in areas ranging from software and hardware verification to scheduling. IBM, Intel, and Microsoft are just a few large companies that research and employ SAT methods in the design and verification of their products.

Course Work

  • Assignment 1, 10%; deadline: January 29th
  • Assignment 2, 10%; deadline: Feb. 28th
  • Assignment 3, 10%; deadline: March 21st
  • Assignment 4, 10%; deadline: April 4th
  • Test 1: 30% ; date: February 14th
  • Test 2: 30% ; date: March 28th
For all course related information (e.g. assignments, sample tests, lecture notes, etc.) please consult the directory /eecs/dept/course/2018-19/W/4401

Subjects to be covered

  • week 1: Introduction to knowledge representation; SAT defined; encoding problems as SAT instances.
  • week 2: Comlete SAT solvers: DPLL introduced; improving DPLL with clause learning.
  • week 3: Solving diagnosis problems with SAT.
  • week 4: Incomplete SAT solvers: Stochastic Local Search algorithms.
  • week 5: SAT applications: from planning to diagnosis and verification; circuit satisfiability.
  • week 6: Resolution for Propositional Logic.
  • week 7: Resolution for Predcat Logic; making resolution efficient.
  • week 8: Applications of Resolution: Logic Programming.
  • week 9: Applications of Resolution: Logic Programming (cont).
  • week 10: Applications of Resolution: Expert Systems.
  • week 11: Satisfiability Modulo Theory (SMT).
  • week 12: SMT applications.

Reading List and Other Resources:

There is no single textbook for this course. The reading list, consisting of WEB resources and relevant book and research paper publications, will be provided (and updated, if necessary). However, please note that:

  • you should undust your logic textbook to review the propositional and first-order (predicate) logics;
  • introductory exposition to resolution and SAT methods could be found in most AI textbooks such as
    Russell and Norvig, Artificial Intelligence, A Modern Approach;
  • most subjects on resolution are covered in:
    • Chang and Lee, Symbolic Logic and Mechanical Theorem Proving,
    • A. Robinson and A. Voronkov, Handbook of Automated Reasoning;
  • most subjects on SAT are covered in
    A. Biere [et al.], Handbook of satisfiability;
  • You can find a wealth of information on SAT and SMT following these links:
  • SAT solvers (picosat and minisat) used in this course can be uploaded from: