1 citations · 1 across the 10 of their papers we have counts for
13 papers
Neurosymbolic Discovery of Algebraic Graph Constructions
David Seka, Stefan Szeider
There are several methods for searching for graphs with prescribed properties, such as SAT solvers and specialized generators. These methods return the result as raw data: an adjac…
LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean
Pablo Manrique, Stefan Szeider
Constraint programming is a core technology for solving complex combinatorial problems in scheduling, planning, configuration, and verification. Trusting its results therefore dema…
Streaming LRAT Certificates into Lean Theorems
Stefan Szeider
If the certificate produced by a SAT solver is checked by a verified checker, we get a verdict which convinces. But this verdict cannot be named, reused as a lemma, or composed wit…
Algorithm Selection with Zero Domain Knowledge via Text Embeddings
Stefan Szeider
We propose ZeroFolio, a feature-free approach to algorithm selection that uses pretrained text embeddings instead of hand-crafted instance features. It reads the raw instance file…
Streamliners for Answer Set Programming
Florentina Voboril, Martin Gebser, Stefan Szeider +1
Streamliner constraints reduce the search space of combinatorial problems by ruling out portions of the solution space. We adapt the StreamLLM approach, which uses Large Language M…
Agentic Neurosymbolic Collaboration for Mathematical Discovery: A Case Study in Combinatorial Design
Hai Xia, Carla P. Gomes, Bart Selman +1
We study mathematical discovery through the lens of neurosymbolic reasoning, where an AI agent powered by a large language model (LLM), coupled with symbolic computation tools, and…
From the Finite to the Infinite: Sharper Asymptotic Bounds on Norin's Conjecture via SAT
Markus Kirchweger, Tomáš Peitl, Bernardo Subercaseaux +1
Norin (2008) conjectured that any -edge-coloring of the hypercube in which antipodal edges receive different colors must contain a monochromatic path between some pair of…
What Do LLM Agents Do When Left Alone? Evidence of Spontaneous Meta-Cognitive Patterns
Stefan Szeider
We introduce an architecture for studying the behavior of large language model (LLM) agents in the absence of externally imposed tasks. Our continuous reason and act framework, usi…
CP-Agent: Agentic Constraint Programming
Stefan Szeider
The translation of natural language to formal constraint models requires expertise in the problem domain and modeling frameworks. To explore the effectiveness of agentic workflows,…
Optimal Decision Tree Pruning Revisited: Algorithms and Complexity
Juha Harviainen, Frank Sommer, Manuel Sorge +1
We present a comprehensive classical and parameterized complexity analysis of decision tree pruning operations, extending recent research on the complexity of learning small decisi…
Breaking Symmetries in Quantified Graph Search: A Comparative Study
Mikoláš Janota, Markus Kirchweger, Tomáš Peitl +1
Graph generation and enumeration problems often require handling equivalent graphs -- those that differ only in vertex labeling. We study how to extend SAT Modulo Symmetries (SMS),…
Extracting Problem Structure with LLMs for Optimized SAT Local Search
André Schidler, Stefan Szeider
Local search preprocessing makes Conflict-Driven Clause Learning (CDCL) solvers faster by providing high-quality starting points and modern SAT solvers have incorporated this techn…
Smart Cubing for Graph Search: A Comparative Study
Markus Kirchweger, Hai Xia, Tomáš Peitl +1
Parallel solving via cube-and-conquer is a key method for scaling SAT solvers to hard instances. While cube-and-conquer has proven successful for pure SAT problems, notably the Pyt…