Organisation/Company University of Lleida Department Computer Engineering Research Field Engineering » Computer engineering Researcher Profile First Stage Researcher (R1) Positions PhD Positions Application Deadline 9 Nov 2026 - 23:59 (Europe/Madrid) Country Spain Type of Contract Temporary Job Status Full-time Hours Per Week 37.5 Offer Starting Date 19 Oct 2026 Is the job funded through the EU Research Framework Programme? Horizon Europe - MSCA Marie Curie Grant Agreement Number 101227512 Is the Job related to staff position within a Research Infrastructure? No

Offer Description

We invite applications for a fully funded PhD position at Univesity of Lleida, within the Logic & Optimization group, under the supervision of Dr. Carlos Ansótegui. The successful candidate will carry out research at the intersection of propositional satisfiability (SAT), Maximum Satisfiability (MaxSAT), proof complexity and LLMs.

Requirements

Research Field Computer science » Other Education Level Master Degree or equivalent

Research Field Mathematics » Mathematical logic Education Level Master Degree or equivalent

Skills/Qualifications

- Master's degree (or equivalent granting access to doctoral studies) in Computer Science, Mathematics, or a closely related field, completed by the starting date.
- Strong background in algorithms, data structures, and computational complexity.
- Solid programming skills in Python and/or C++ (the languages of the Paramita framework the candidate will extend).
- Familiarity with propositional logic; prior exposure to SAT/MaxSAT solving, constraint programming, or proof complexity is an asset but not required.
- Motivation to combine theoretical analysis with solver implementation and experimentation.

Languages ENGLISH Level Excellent





Research Field Engineering » Computer engineering Years of Research Experience None

Additional Information

Research topic

Large Language Models (LLMs) are opening new opportunities for automating complex reasoning and optimization tasks, from translating natural-language problem descriptions into formal models to guiding combinatorial search. However, reliably solving these problems requires combining the flexibility of LLMs with the precision and guarantees of formal methods. This PhD project aims to develop novel techniques at the intersection of LLMs, Satisfiability (SAT), and Maximum Satisfiability (MaxSAT), leveraging LLMs to automate problem modelling, guide solver strategies, and improve optimization performance.

A central research direction is the development of LLM-based techniques that automatically transform natural-language descriptions of real-world problems into formal MaxSAT formulations and orchestrate their solution. This includes identifying decision variables and constraints, distinguishing hard constraints from soft preferences, generating and validating encodings, and selecting and invoking suitable solvers and related tools. We will investigate iterative workflows in which solver feedback, validation procedures, and solution analysis help detect modelling errors and refine formulations.



The goal is to bridge the gap between high-level problem descriptions and effective automated optimization while ensuring the correctness and reliability of the resulting solutions.

Another research direction concerns improving the performance of MaxSAT solvers through meta-algorithms and metaheuristics. In particular, we will investigate how to select effective core sequences in core-guided MaxSAT algorithms, where different choices can lead to substantial differences in solver performance. We aim to develop adaptive strategies using techniques such as evolutionary algorithms, reinforcement learning, and LLM-guided search, exploiting solver traces and performance feedback to select promising core sequences, heuristics, and solver configurations. A key challenge is to combine the generalization capabilities of LLMs with systematic optimization and empirical evaluation to obtain robust improvements across diverse problem instances.

To demonstrate impact beyond benchmarks, the project will apply these techniques to challenging mathematical and industrial problems, particularly optimization problems arising from interpretable machine learning models. These applications align with broader objectives in trustworthy AI, where SAT- and MaxSAT-based methods can support the development, optimization, and formal analysis of interpretable decision models.

As part of the thesis, the candidate will contribute to and extend Paramita ( https://pypi.org/project/paramita/ ), an extensible open-source framework for building applications around SAT, MaxSAT, and related satisfiability technologies. Paramita provides a unified API for interacting with different solvers, supports plugins written in C++ and Python, and includes

📌 PhD Position in SAT and MaxSAT Solving: Core-Guided Algorithms and SAT-to-MaxSAT Gadgets (España)
🏢 University of Lleida
📍 España