arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2604.15992

Solving Fuzzy Satisfiability via Mixed-Integer Non-Linear Programming

Pablo F. Castro
View original source ↗Read source document ↗Export metadata ↓

Abstract

This paper introduces SATFuL, a SAT solver for fuzzy logics. In contrast to the Boolean case, for which numerous SAT solvers exist, the SAT problem for fuzzy logics has attracted less attention, even though these tools have interesting applications. Unlike existing SAT solvers for fuzzy logics, SATFuL uses MINLP (Mixed Integer Non-Linear Programming) solvers to check the satisfiability of fuzzy formulas. This approach offers certain benefits; for instance, our tool can handle all major variations of fuzzy propositional logic, whereas other fuzzy solvers are usually tailored to specific versions of fuzzy logic. We conduct some experiments and demonstrate that the performance of our tool is comparable with state-of-the-art fuzzy solvers for Lukasiewicz logic, and outperforms available solvers for Product logic. The approach is sound and complete and can be easily extended to accommodate new fuzzy operators.

Explore related subjects

cs.LO

Keep this discovery

BibTeXRIS

Pablo F. Castro. 2026-08-28. Solving Fuzzy Satisfiability via Mixed-Integer Non-Linear Programming. https://arxiv.org/abs/2604.15992

Cite the original work for its findings. Save a collection to share your selection of sources.

Discover connections

cs.LO subject

Connections use source metadata and explicit phrase matches, not verified experimental comparisons.

KEEP EXPLORING

Related papers

arXiv2026

A categorical formulation of Kraus' paradox

We give a categorical formulation of Kraus' "magic trick" for recovering information from truncated types. Rather than type theory, we work in Van den Berg-Moerdijk path categories with a univalent universe, and rather than propositional truncation we work with arbitrary cofibrations, which includes truncation as a special case. We show, using Kraus' argument that any cofibration with homogeneous domain is a monomorphism. We give some simple concrete examples in groupoids to illustrate the interaction between homogeneous types, cofibrations and univalent fibrations.

math.CT↗
arXiv2026

Quantified propositional calculi and narrow implicit proofs

In the implicit version of a propositional proof system Q, we work with Q-proofs that are not written down directly, but are succinctly encoded by circuits. Thus implicit Q-proofs are potentially exponentially shorter than usual Q-proofs. We study narrow implicit proofs, a restricted version of this notion, in which lines in the encoded proof can only have polynomial size. We use a cut-elimination construction to show that G_{i+1} is equivalent to narrow implicit G_i, for i >= 1, where G_i is the extension of Frege allowing reasoning with Sigma^q_i quantified propositional formulas. We show that G_1 is equivalent to implicit resolution.

cs.LO↗
arXiv2026

Exponential Gaps Between Intuitionistic Linear Extended Frege Systems

In this paper, we establish exponential separations between Extended Frege systems for a range of intuitionistic substructural and linear logics. More precisely, for any logic $L$ below the intuitionistic logic obtained by extending $\mathbf{ILL}$ with structural rules, and any logic $M$ not contained in $L$, we construct a family of $\mathsf{FL_e}$-provable formulas that have short proofs in $M$-Frege but require proofs of exponential size in $L$-Extended Frege. The same result holds in the $!$-free settings, using $\mathbf{IMALL}$ and $\mathbf{FL_e}$ in place of $\mathbf{ILL}$. The key ingredient in proving these separations is a variant of the feasible disjunction property for $L$-Frege, which may be of independent interest.

cs.LO↗