53 citations · 136 across the 17 of their papers we have counts for
18 papers
Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience
Ruben Martins
We report on CoreForge, an experience in using large language models (LLMs) to build an unweighted MaxSAT solver from research papers rather than from an existing solver codebase.…
MELT: Mining Effective Lightweight Transformations from Pull Requests
Daniel Ramos, Hailie Mitchell, Inês Lynce +3
Software developers often struggle to update APIs, leading to manual, time-consuming, and error-prone processes. We introduce MELT, a new approach that generates lightweight API mi…
UpMax: User partitioning for MaxSAT
Pedro Orvalho, Vasco Manquinho, Ruben Martins
It has been shown that Maximum Satisfiability (MaxSAT) problem instances can be effectively solved by partitioning the set of soft clauses into several disjoint sets. The partition…
CUBES: A Parallel Synthesizer for SQL Using Examples
Ricardo Brancas, Miguel Terra-Neves, Miguel Ventura +2
In recent years, more people have seen their work depend on data manipulation tasks. However, many of these users do not have the background in programming required to write comple…
SOAR: A Synthesis Approach for Data Science API Refactoring
Ansong Ni, Daniel Ramos, Aidan Yang +4
With the growth of the open-source data science community, both the number of data science libraries and the number of versions for the same library are increasing rapidly. To matc…
FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions
Margarida Ferreira, Miguel Terra-Neves, Miguel Ventura +2
Form validators based on regular expressions are often used on digital forms to prevent users from inserting data in the wrong format. However, writing these validators can pose a…
Program Equivalence for Assisted Grading of Functional Programs (Extended Version)
Joshua Clune, Vijay Ramamurthy, Ruben Martins +1
In courses that involve programming assignments, giving meaningful feedback to students is an important challenge. Human beings can give useful feedback by manually grading the pro…
Reflections on "Incremental Cardinality Constraints for MaxSAT"
Ruben Martins, Saurabh Joshi, Vasco Manquinho +1
To celebrate the first 25 years of the International Conference on Principles and Practice of Constraint Programming (CP) the editors invited the authors of the most cited paper of…
Approximation Strategies for Incomplete MaxSAT
Saurabh Joshi, Prateek Kumar, Ruben Martins +1
Incomplete MaxSAT solving aims to quickly find a solution that attempts to minimize the sum of the weights of the unsatisfied soft clauses without providing any optimality guarante…
Program Synthesis using Conflict-Driven Learning
Yu Feng, Ruben Martins, Osbert Bastani +1
We propose a new conflict-driven program synthesis technique that is capable of learning from past mistakes. Given a spurious program that violates the desired specification, our s…
Relating Complexity-theoretic Parameters with SAT Solver Performance
Edward Zulkoski, Ruben Martins, Christoph Wintersteiger +4
Over the years complexity theorists have proposed many structural parameters to explain the surprising efficiency of conflict-driven clause-learning (CDCL) SAT solvers on a wide va…
Component-based Synthesis of Table Consolidation and Transformation Tasks from Examples
Yu Feng, Ruben Martins, Jacob Van Geffen +2
This paper presents an example-driven synthesis technique for automating a large class of data preparation tasks that arise in data science. Given a set of input tables and an out-…
Type-Directed Code Reuse using Integer Linear Programming
Yuepeng Wang, Yu Feng, Ruben Martins +3
In many common scenarios, programmers need to implement functionality that is already provided by some third party library. This paper presents a tool called Hunter that facilitate…
Automated Synthesis of Semantic Malware Signatures using Maximum Satisfiability
Yu Feng, Osbert Bastani, Ruben Martins +2
This paper proposes a technique for automatically learning semantic malware signatures for Android from very few samples of a malware family. The key idea underlying our technique…
Generalized Totalizer Encoding for Pseudo-Boolean Constraints
Saurabh Joshi, Ruben Martins, Vasco Manquinho
Pseudo-Boolean constraints, also known as 0-1 Integer Linear Constraints, are used to model many real-world problems. A common approach to solve these constraints is to encode them…
Exploiting Resolution-based Representations for MaxSAT Solving
Miguel Neves, Ruben Martins, Mikoláš Janota +2
Most recent MaxSAT algorithms rely on a succession of calls to a SAT solver in order to find an optimal solution. In particular, several algorithms take advantage of the ability of…
Incremental Bounded Model Checking for Embedded Software (extended version)
Peter Schrammel, Daniel Kroening, Martin Brain +3
Program analysis is on the brink of mainstream in embedded systems development. Formal verification of behavioural requirements, finding runtime errors and automated test case gene…
Incremental Cardinality Constraints for MaxSAT
Ruben Martins, Saurabh Joshi, Vasco Manquinho +1
Maximum Satisfiability (MaxSAT) is an optimization variant of the Boolean Satisfiability (SAT) problem. In general, MaxSAT algorithms perform a succession of SAT solver calls to re…