Searcharxiv⌕ Search

arXiv subjects

Maximilian Heisinger

Publications and source records attributed to Maximilian Heisinger.

3 recordsLinked to original sources

From Natural Language to Exact Cover: A Neuro-Symbolic Approach to Zebra Puzzles

Chain-of-Thought (CoT) generation has substantially improved the performance of Large Language Models (LLMs) on complex reasoning tasks, including code generation, data analysis, and exam-style question answering. Despite these advances, purely neural LLMs continue to struggle with elementary logical reasoning problems and lack the determinism, soundness, and reliability characteristic of symbolic reasoning systems. Conversely, classical symbolic methods such as SAT solving and exact cover guarantee correctness and completeness, but require problems to be expressed in highly specialized formal encodings, limiting their applicability to natural language inputs. In this work, we present a synergistic neuro-symbolic framework that bridges this gap by combining neural semantic parsing with deterministic exact cover reasoning. Given a Zebra-style logic puzzle in natural language, an LLM translates entities and constraints into structured tool calls that construct an exact cover instance. A symbolic solver then computes the solution and provides feedback to iteratively refine invalid, under- or overconstrained encodings, exploiting the uniqueness property of Zebra puzzles. We conduct a comprehensive empirical evaluation across multiple parameter scales, post-training paradigms, and LLM families. The results demonstrate that our hybrid approach consistently outperforms strong plain neural baselines, including CoT prompting, as well as recent neuro-symbolic methods.

cs.AI↗

f4ncgb: High Performance Gröbner Basis Computations in Free Algebras

We present f4ncgb, a new open-source C++ library for Gröbner basis computations in free algebras, which transfers recent advancements in commutative Gröbner basis software to the noncommutative setting. As our experiments show, f4ncgb establishes a new state-of-the-art for noncommutative Gröbner basis computations. We also discuss implementation details and design choices.

cs.MS↗

Search-Space Pruning with Int-Splits for Faster QBF Solving

In many QBF encodings, sequences of Boolean variables stand for binary representations of integer variables. Examples are state labels in bounded model checking or actions in planning problems. Often not the full possible range is used, e.g., for representing six different states, three Boolean variables are required, rendering two of the eight possible assignments irrelevant for the solution of the problem. As QBF solvers do not have any domain-specific knowledge on the formula they process, they are not able to detect this pruning opportunity. In this paper, we introduce the idea of int-splits, which provide domain-specific information on integer variables to QBF solvers. This is particularly appealing for parallel Divide-and-Conquer solving which partitions the search space into independently solvable sub-problems. Using this technique, we reduce the number of generated sub-problems from a full expansion to only the required subset. We then evaluate how many resources int-splits save in problems already well suited for D&C. In that context, we provide a reference implementation that splits QBF formulas into many sub-problems with or without int-splits and merges results. We finally propose a comment-based optional syntax extension to (Q)DIMACS that includes int-splits and is suited for supplying proposed guiding paths natively to D&C solvers.

cs.LO↗