Solving Fuzzy Satisfiability via Mixed-Integer Non-Linear Programming

TL;DR

This paper presents SATFuL, a novel fuzzy logic SAT solver using MINLP techniques, capable of handling various fuzzy logics with competitive performance and easy extensibility.

Contribution

Introduces SATFuL, a versatile fuzzy SAT solver based on MINLP, outperforming existing solvers for certain fuzzy logics and supporting multiple fuzzy logic variants.

Findings

SATFuL performs comparably to state-of-the-art Lukasiewicz logic solvers.

SATFuL outperforms existing solvers for Product logic.

The approach is sound, complete, and easily extendable.

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.