UnB-SAT is the Satisfiability and Automated Planning group at the University of Brasília (FCTE, Gama campus), led by Prof. Bruno César Ribas. We state hard combinatorial problems in the right formal language, Boolean satisfiability (SAT), pseudo-Boolean constraints or automated planning (PDDL and SATPLAN), and study how to solve them efficiently. Alongside this we maintain CD-MOJ, a contest-driven online judge, and at the graduate level we also work on applied artificial intelligence.

• SAT and pseudo-Boolean reasoning. Modular solvers, encodings and preprocessing, and reductions from other problems to SAT and pseudo-Boolean constraints.
• Automated planning. PDDL modeling, planning as satisfiability (SATPLAN, mixed-Horn formulas, the Madagascar planner), and solving puzzles and games as planning.
• CD-MOJ and competitive programming. The Contest-Driven Meta Online Judge and the Maratona-Linux environment.
• Applied AI (graduate research). Natural language processing, data mining and machine learning.

We offer the elective Fundamentos Lógicos da IA (Logical Foundations of AI), a hands-on course where students model the same puzzle as SAT, as pseudo-Boolean constraints and as planning, and then compete on the MOJ judge (Light Up, Lights Out, Bomberda, Minesweeper, a delivery-planning competition, and more). Latest edition, syllabus and challenges: https://www.brunoribas.com.br/flia/2025-1/.

Bruno César Ribas
_{Associate Professor, University of Brasília (FCTE, Gama)}
Site · ORCID · Scholar · DBLP · ResearchGate · LinkedIn · Lattes · GitHub

The team (students and collaborators), advised theses, undergraduate research (Iniciação Científica) and publications are on the group website: https://unb-sat.github.io.

• Group website: https://unb-sat.github.io
• CD-MOJ: judge, docs, github.com/cd-moj
• Maratona-Linux: github.com/maratona-linux
• Advised work: BDM (TCC), UnB repository (M.Sc.)
• Profiles: ORCID, Google Scholar, ResearchGate, DBLP
• Email: bruno.ribas@unb.br