SubjectsSubjects(version: 978)
Course, academic year 2025/2026
   Login via CAS
   
Seminar on satisfiability - NAIL092
Title: Seminář ze splnitelnosti
Guaranteed by: Department of Theoretical Computer Science and Mathematical Logic (32-KTIML)
Faculty: Faculty of Mathematics and Physics
Actual: from 2022
Semester: summer
E-Credits: 3
Hours per week, examination: summer s.:0/2, C [HT]
Capacity: unlimited
Min. number of students: unlimited
4EU+: no
Virtual mobility / capacity: no
State of the course: cancelled
Language: Czech
Teaching methods: full-time
Guarantor: doc. RNDr. Pavel Surynek, Ph.D.
Class: Informatika Mgr. - volitelný
Classification: Informatics > Theoretical Computer Science
Opinion survey results   Schedule   Noticeboard   
Annotation -
A referative seminar on solving satisfiability problems. The main topic of the seminar are modern algorithmic techniques for solving Boolean satisfiability problems (SAT) and constraint satisfaction problems (CSP).
Last update: Macharová Dana, JUDr. (14.10.2008)
Aim of the course -

To improve knowledge and skills in solving satisfiability problems. To learn to make self-contained theoretical and experimental research.

Last update: Surynek Pavel, doc. RNDr., Ph.D. (21.02.2011)
Literature -

Rina Dechter. Constraint Processing. Morgan Kaufmann Publishers, 2003.

Stuart Russell and Peter Norvig. Artificial Intelligence: A Modern Approach (second edition). Prentice Hall, 2003.

Sborníky konference SAT (International Conference on Theory and Applications of Satisfiability Testing).

Sborníky konference CP (International Conference on Principles and Practice of Constraint Programming).

Sborníky konference CP-AI-OR (International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems).

Last update: TOPFER/MFF.CUNI.CZ (14.10.2008)
Syllabus -

Referred topics cover the modern trends of problem solving in Boolean satisfiability (SAT) and constraint satisfaction (CSP). The relevant topics include (but are not limited to) the following:

Reducing the search space: Intelligent search, symmetries, consistencies, global constraints, preprocessing and transformations of problems, comparison of SAT and CSP techniques, decision heuristics.

Implementation issues: The architecture of complete and incomplete SAT solvers, the architecture of complete and incomplete CSP solvers, efficient implementation, unit propagation, filtration, literal watching, learning, parallel implementations.

Practical problem solving: Software products for solving SAT and CSP, random problems, structured problems, phase transition, diagnosis as SAT, planning as SAT, optimization.

Additional topics according to attendee's interests.

Last update: Macharová Dana, JUDr. (14.10.2008)
 
Charles University | Information system of Charles University | http://www.cuni.cz/UKEN-329.html