arXiv subjects

Marek Dančo

Publications and source records attributed to Marek Dančo.

4 recordsLinked to original sources

arXiv2026

Revisiting Incremental Linearization for Nonlinear Integer Arithmetic

Incremental Linearization has previously been proposed for solving SMT problems over quantifier-free nonlinear integer arithmetic and has proven effective despite its conceptual simplicity. In this paper, we introduce a revised axiom set that improves convergence on polynomial constraints built from higher-degree monomials, such as powers and mixed products, a class of problems on which prior axiomatizations struggled. We present a standalone implementation built on top of Z3 for linear integer arithmetic and evaluate it on the NIA benchmark set from SMT-LIB. Our results show that the approach is competitive with state-of-the-art solvers overall and substantially outperforms them on benchmarks dominated by such polynomial constraints.

cs.LO↗

arXiv2026

Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols

The combination of uninterpreted function symbols and universal quantification occurs in many applications of automated reasoning, for example, due to their ability to reason about arrays. Yet the satisfiability of such formulas is, in general, undecidable. In practice, SMT solvers are often successful in the unsatisfiable case, using heuristics. However, in the satisfiable case, they rely on explicit model construction, which fails for formulas whose smallest model is not small enough. We introduce an alternative approach that certifies satisfiability using induction arguments, and apply it to the case of linear integer arithmetic. The resulting algorithm is able to prove satisfiability of formulas that are out of reach for current SMT solvers.

cs.LO↗

arXiv2025

From MBQI to Enumerative Instantiation and Back

This work investigates the relation between model-based quantifier instantiation (MBQI) and enumerative instantiation (EI) in Satisfiability Modulo Theories (SMT). MBQI operates at the semantic level and guarantees to find a counterexample to a given a non-model. However, it may lead to weak instantiations. In contrast, EI strives for completeness by systematically enumerating terms at the syntactic level. However, such terms may not be counter-examples. Here we investigate the relation between the two techniques and report on our initial experiments of the proposed algorithm that combines the two.

cs.LO↗

arXiv2025

Complete Symmetry Breaking for Finite Models

This paper introduces a SAT-based technique that calculates a compact and complete symmetry-break for finite model finding, with the focus on structures with a single binary operation (magmas). Classes of algebraic structures are typically described as first-order logic formulas and the concrete algebras are models of these formulas. Such models include an enormous number of isomorphic, i.e. symmetric, algebras. A complete symmetry-break is a formula that has as models, exactly one canonical representative from each equivalence class of algebras. Thus, we enable answering questions about properties of the models so that computation and search are restricted to the set of canonical representations. For instance, we can answer the question: How many non-isomorphic semigroups are there of size $n$? Such questions can be answered by counting the satisfying assignments of a SAT formula, which already filters out non-isomorphic models. The introduced technique enables us calculating numbers of algebraic structures not present in the literature and going beyond the possibilities of pure enumeration approaches.

cs.LO↗