SAT 和 MaxSAT 求解的博士研究员（科研助理，Paramita 框架）

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 / required education level / degree: Master Degree or equivalent

Requirements / required education level / discipline: Computer science

Requirements / required education level / degree: Master Degree or equivalent

Requirements / required education level / discipline: Mathematics

Requirements / skills: - 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.

Requirements / required languages / language: ENGLISH

Requirements / required languages / language level: Excellent

Research experience / main research field: Engineering

Research experience / research sub field: Computer engineering

Research experience / years of research experience: None

Additional information / benefits: 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. https://www.euraxess.es/system/files/2025-02/Guide%20on%20salary%20calculations%20for%20MSCA%20fellowships%20in%20Spain_0.pdf

Additional information / eligibility criteria: - Candidates must be eligible for admission to the doctoral programme at University of Lleida (https://www.doctorat.udl.cat/en/doctorands/admissio/). - Mobility or nationality requirements imposed by the funding programme, if any.

Additional information / selection process: 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

Additional information / comment: How to apply Send the following documents in a single PDF to info@cords-dn.at with the subject "Application DC 10" : 1. Curriculum vitae. 2. Academic transcripts (Bachelor's and Master's). 3. Motivation letter (max. 1 page) describing your interest in the topic. 4. Contact details of [1–2] referees (or reference letters). Deadline: 31/08/2026 . Informal enquiries are welcome and may be addressed to Carlos Ansótegui (carlos.ansotegui@udl.cat). Note: We updated the deadline to August 31, 2026.

Work location / nr job positions: 1

Work location / job organisation institute: University of Lleida

Work location / job country: Spain

Work location / job state province: Lleida

Work location / job city: Lleida

Work location / job postal code: 25001

Work location / job street: Jaume II, n 69

Hiring contact / organisation institute: University of Lleida

Hiring contact / organisation institute type: Higher Education Institute

Hiring contact / division faculty: Computer Engineering

Hiring contact / country: Spain

Hiring contact / city: Lleida

Hiring contact / postal code: 25001

Hiring contact / street: Jaume II, 69

Hiring contact / website: https://ulog.udl.cat/

Application / how to apply: e-mail

Application / application email: info@cords-dn.at

EU funding / framework programme: Horizon Europe - MSCA

EU funding / cofund nr job position: 1

EU funding / sesam agreement number: 101227512

Research field / main research field: Engineering

Research field / sub research field: Computer engineering

Researcher profile: First Stage Researcher (R1)

Positions: PhD Positions

Contract: Temporary

Job status: Full-time

Application deadline (as exported; timezone unverified): 2026-11-09T22:59:59