UnB-SAT logo

UnB-SAT

About

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 (B.Sc. 2008, M.Sc. 2011 and Ph.D. 2015 in Computer Science, Federal University of Paraná).

Our work follows a single premise: many hard combinatorial problems become tractable once they are stated in the right formal language. We encode problems such as scheduling, resource consolidation, graph queries, puzzles and games into Boolean satisfiability (SAT), pseudo-Boolean constraints or classical planning (PDDL and SATPLAN), and then study how to solve them efficiently. In parallel we maintain CD-MOJ, a contest-driven online judge, together with the Maratona-Linux environment used in programming contests. At the graduate level the group also works on applied artificial intelligence, including natural language processing and data mining.

Research lines

  • 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.

Teaching

We offer the elective Fundamentos Lógicos da IA (Logical Foundations of AI), where students model the same puzzle as SAT, as pseudo-Boolean constraints and as planning, then compete on the MOJ judge. See Teaching for the full description.

Explore

UnB-SAT is a research and teaching group, not yet a formally consolidated laboratory at UnB; a proposal to establish the laboratory is planned for the near future. Built with support from Claude (Anthropic).

This site uses Just the Docs, a documentation theme for Jekyll.