PhD Position in SAT and MaxSAT Solving: Core-Guided Algorithms and SAT-to-MaxSAT Gadgets

University of Lleida; España; Vor Ort; EUR 33.000 - 38.000; Vollzeit

Benefits dieser Stelle

Fully funded PhD (MSCA)

Enrollment in Doctoral Programme

International research environment

Zusammenfassung

The University of Lleida invites applications for a fully funded PhD position in the Logic & Optimization group, under Dr. Carlos Ansótegui.

The successful candidate will research at the intersection of SAT, MaxSAT, proof complexity, and large language models. This three-year MSCA-funded project aims to transform natural-language problem descriptions into formal MaxSAT models, explore core sequences in core-guided MaxSAT, and apply results to interpretable machine learning problems.

Qualifikationen

• Master's degree in Computer Science, Mathematics, or closely related field by start date.
• Strong background in algorithms, data structures, and computational complexity.
• Solid programming skills in Python and/or C++.
• Familiarity with propositional logic; SAT/MaxSAT exposure is a plus.
• Interest in combining theory with solver implementation and experimentation.

Aufgaben

• Carry out research at the intersection of SAT, MaxSAT, and LLMs.
• Develop problem modelling and encodings with LLM guidance.
• Experiment with solvers and track performance on benchmarks.
• Publish results and contribute to open-source Paramita integration.

Kenntnisse

Master's degree

Algorithms

Data structures

Python

C++

Propositional logic

SAT/MaxSAT

Motivation for theory and impl

Ausbildung

Master's degree or equivalent

Tools

Paramita framework

Python

C++

Jobbeschreibung

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 modelling tools for constructing and solving problems. The algorithms, metaheuristics, LLM-assisted optimization strategies, and natural-language-to-MaxSAT techniques developed in this thesis will be implemented and released as part of the Paramita ecosystem, ensuring reproducibility and broad availability of the results.

What we offer

• A fully funded 3-year PhD contract funded by The Marie Skłodowska-Curie Actions (MSCA) Doctoral Networks programme Grant Agreement / Confident Data-Driven Decision Support (CoRDS) Ref. 101227512].
• The MSCA provides a total annual employment cost of €54,522.72 for this position, which includes the employer's Social Security contributions. After these contributions are deducted, the estimated annual gross salary is €33,272.28. For researchers with family obligations, the total annual employment cost increases to €62,422.72, with an estimated annual gross salary of €37,986 after employer Social Security deductions. In both cases, the employee's own Social Security contributions and personal income tax (IRPF) are deducted from the gross salary to determine the net salary. These amounts may change if Spanish legislation is updated. A detailed explanation of MSCA salary calculations in Spain is available in the Euraxess Spain guide.
• Enrolment in the doctoral programme in Engineering and Information Technology at University of Lleida.
• A stimulating international research environment with opportunities to attend leading conferences (e.g., SAT, IJCAI, AAAI, CP) and collaborate with international partners.

Applications will be evaluated by a coordinator designed by the coordinator of the Doctoral Network on the basis of academic record, research fit, and motivation. Shortlisted candidates will be invited to an online interview. committeecoordinator