Maximum Satisfiability

Solving MaxSAT Problems from Natural Language Descriptions with LLMs and PySAT @ LLM-Solve @ FLoC 2026 featured image

Solving MaxSAT Problems from Natural Language Descriptions with LLMs and PySAT @ LLM-Solve @ FLoC 2026

In this talk, we will present a framework for solving MaxSAT problems expressed in natural language by combining large language models with the PySAT toolkit. We will show how LLMs …

avatar
Pedro Orvalho
Read more
📄🤖 2 Papers accepted @ EPIA 2026!! 🎉🎉 featured image

📄🤖 2 Papers accepted @ EPIA 2026!! 🎉🎉

Excited to share that two of our papers have been accepted at EPIA 2026, covering the robustness of LLMs for code understanding and neuro-symbolic feedback for Vision-Language …

avatar
Pedro Orvalho
Read more
MaxSAT-Based Feedback for Guiding Vision-Language Models in Sudoku featured image

MaxSAT-Based Feedback for Guiding Vision-Language Models in Sudoku

In this paper, we propose a neuro-symbolic approach that integrates formal constraint reasoning into the VLM solving process via a Maximum Satisfiability (MaxSAT) oracle. Rather …

avatar
Pedro Orvalho
Read more
📄📄📄 3 Papers accepted @ FLoC 2026!! 🎉🎉🎉 featured image

📄📄📄 3 Papers accepted @ FLoC 2026!! 🎉🎉🎉

Excited to share that three of our papers have been accepted at FLoC 2026, covering automated feedback for Prolog education, data-driven mutation testing for Prolog, and …

avatar
Pedro Orvalho
Read more
Solving MaxSAT Problems from Natural Language Descriptions with LLMs and PySAT featured image

Solving MaxSAT Problems from Natural Language Descriptions with LLMs and PySAT

In this paper, we study a neuro-symbolic approach in which an LLM translates a natural language description of an optimisation problem into executable Python code using PySAT. The …

avatar
Pedro Orvalho
Read more
Counterexample Guided Program Repair Using Large Language Models and MaxSAT-based Fault Localization @ IIIA-CSIC featured image

Counterexample Guided Program Repair Using Large Language Models and MaxSAT-based Fault Localization @ IIIA-CSIC

In this talk I will present a hybrid method to automated repair of C code, using Maximum Satisfiability (MaxSAT)-based fault localization, CFaults, to localize bugs and LLMs to …

avatar
Pedro Orvalho
Read more
MENTOR: Automated Feedback for Introductory Programming Exercises @ FCT-UNL featured image

MENTOR: Automated Feedback for Introductory Programming Exercises @ FCT-UNL

In my talk, I will present MENTOR, a semantic automated program repair (APR) framework designed to provide Automated Feedback for Introductory Programming Exercises.

avatar
Pedro Orvalho
Read more
Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization @ OutSystems featured image

Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization @ OutSystems

In this talk I will present our novel approach that combines the strengths of both FM-based fault localization and LLMs, via zero-shot learning, to enhance Automated Program …

avatar
Pedro Orvalho
Read more
LLM-Driven Automated Program Repair Using MaxSAT-based Fault Localization @ Oxford featured image

LLM-Driven Automated Program Repair Using MaxSAT-based Fault Localization @ Oxford

In this talk I will present a hybrid method to automated repair of C code, using Maximum Satisfiability (MaxSAT)-based fault localization, CFaults, to localize bugs and LLMs to …

avatar
Pedro Orvalho
Read more
User partitioning for Maximum Satisfiability featured image

User partitioning for Maximum Satisfiability

The Maximum Satisfiability (MaxSAT) problem is the optimisation variant of the Satisfiability (SAT) problem. Solving MaxSAT efficiently often involves partitioning the set of soft …

avatar
Pedro Orvalho
Read more
UpMax: User partitioning for MaxSAT @ SAT 2023 featured image

UpMax: User partitioning for MaxSAT @ SAT 2023

In this talk I will present a new framework called UpMax that decouples the partitioning procedure from the MaxSAT solving algorithms.

avatar
Pedro Orvalho
Read more
UpMax: User partitioning for MaxSAT featured image

UpMax: User partitioning for MaxSAT

This paper proposes a new framework called UpMax that decouples the partitioning procedure from the MaxSAT solving algorithms. As a result, new partitioning procedures can be …

avatar
Pedro Orvalho
Read more

AlloyMax: Bringing Maximum Satisfaction to Relational Specifications

We propose AlloyMax, an extension of Alloy with a capability to express and analyze problems with optimal solutions. AlloyMax introduces (1) a small addition of language constructs …

Changjian Zhang
Read more