Solving Fuzzy Satisfiability via Mixed-Integer Non-Linear Programming

1. Problem Statement

The paper addresses the Satisfiability (SAT) problem for fuzzy logics. Unlike Boolean SAT, where formulas evaluate to true (1) or false (0), fuzzy logic formulas evaluate to values within the continuous interval $[0, 1]$.

• Context: While Boolean SAT solvers are mature and widely used (e.g., in SMT solvers and model checking), fuzzy SAT solvers are underdeveloped.
• Challenges:
  • Diversity of Logics: Fuzzy logics vary based on the definition of the t-norm (conjunction). The paper focuses on Łukasiewicz, Product, and Gödel logics. Existing tools are often tailored to specific logics (e.g., only Łukasiewicz) and struggle to generalize.
  • Scalability & Completeness: Current fuzzy solvers suffer from scalability issues. Some rely on reduction to finite-valued logics (losing precision) or evolutionary strategies (incomplete).
  • Specific Limitations: Existing Product logic solvers (like MNiBLoS) often use incomplete transformations of non-linear arithmetic, potentially misclassifying unsatisfiable clauses as satisfiable.

2. Methodology: SATFuL

The authors propose SATFuL, a new SAT solver that translates fuzzy satisfiability problems into Mixed-Integer Non-Linear Programming (MINLP) problems.

Core Approach

Instead of using specialized heuristics for fuzzy logic, SATFuL leverages the power of modern MINLP solvers (specifically Gurobi and SCIP) to handle the arithmetic constraints inherent in fuzzy logic.

The Algorithm

The solver operates in two main stages:

1. Translation (toMINLP procedure):
   • The algorithm recursively traverses a fuzzy formula.
   • For every sub-formula $\phi'$, it introduces a fresh real-valued variable $x_{\phi'} \in [0, 1]$.
   • It generates a set of linear and non-linear constraints ($I$) and integer variables ($Z$) that mathematically enforce the semantics of the fuzzy operators.
   • Key Handling of Operators:
     • Łukasiewicz: Uses linear constraints for conjunction/disjunction and introduces binary variables to handle the implication operator ($x \Rightarrow_L y$).
     • Product Logic: Handles the non-linear multiplication ($x \cdot y$) directly. Crucially, it models the implication ($x \Rightarrow_\Pi y$) and negation using auxiliary binary variables and non-linear constraints to ensure exactness, avoiding the approximations used in previous tools.
     • Gödel Logic: Not explicitly coded as separate operators because they can be expressed using Łukasiewicz operators within the framework.
2. Solving (SAT procedure):
   • The set of clauses is converted into a single MINLP problem $\langle I, Z, M \rangle$, where $I$ are constraints, $Z$ are integer variables, and $M$ is the objective function (minimizing a sum of variables, though feasibility is the primary goal).
   • The tool calls an external MINLP solver.
   • If the solver finds a feasible solution, the formula is SAT; otherwise, it is UNSAT.

Theoretical Guarantees

• Soundness and Completeness: The paper proves (Theorem 1 and 2) that the set of valuations satisfying the fuzzy clauses is exactly equivalent to the set of feasible solutions of the constructed MINLP problem. This ensures the solver is both sound (no false positives) and complete (no false negatives), modulo the correctness of the underlying MINLP solver.

Tool Architecture

SATFuL is an open-source Python tool consisting of three modules:

1. Preprocessing: Parses input and builds an Abstract Syntax Tree (AST).
2. MINLP Module: Implements the recursive translation algorithm using a visitor pattern.
3. Solver Module: Interfaces with Gurobi or SCIP to solve the generated MINLP problem.

3. Key Contributions

1. Generalization: Unlike previous tools restricted to specific logics, SATFuL handles Łukasiewicz, Product, and Gödel logics within a single framework.
2. Exactness for Product Logic: It provides a sound and complete reduction for Product logic, addressing the incompleteness issues of existing solvers like MNiBLoS (which maps non-linear arithmetic to negative arithmetic, risking errors).
3. Leveraging MINLP Advances: The paper capitalizes on recent advancements in commercial (Gurobi) and academic (SCIP) MINLP solvers, which have become significantly more powerful and scalable than when earlier MILP-based approaches were attempted.
4. Extensibility: The modular design allows for the easy addition of new fuzzy operators or logics by simply defining their corresponding MINLP constraints.

4. Experimental Results

The authors evaluated SATFuL against state-of-the-art competitors:

• Competitors:
  • fuzzySAT: A state-of-the-art solver for Łukasiewicz logic (reduces to CSP).
  • MNiBLoS: A Product logic solver using the SMT solver Z3.
• Setup: Experiments ran on a MacBook M2 (16GB RAM) using benchmarks from [16].
• Findings:
  • Łukasiewicz Logic:
    • With Gurobi, SATFuL consistently outperformed fuzzySAT on both SAT and UNSAT instances.
    • With SCIP, SATFuL was comparable to fuzzySAT on SAT instances but significantly superior on UNSAT instances (fuzzySAT timed out frequently, while SATFuL solved all).
  • Product Logic:
    • SATFuL (with both Gurobi and SCIP) outperformed MNiBLoS in all cases (both SAT and UNSAT).
    • This confirms that the MINLP approach is more robust and scalable than the SMT-based reduction used by MNiBLoS.

5. Significance

• Bridging the Gap: SATFuL narrows the performance gap between fuzzy SAT solvers and the highly optimized Boolean SAT solvers.
• Reliability: By providing a sound and complete reduction for Product logic, it eliminates the risk of incorrect satisfiability classifications found in previous approaches.
• Practical Utility: The tool offers a unified, maintainable, and extensible platform for verifying systems involving fuzzy reasoning (e.g., neural networks, image processing, multi-agent systems) without needing to rewrite solvers for every specific logic variant.
• Future Potential: The success of this approach suggests that Mixed-Integer Non-Linear Programming is a viable and powerful backend for solving complex many-valued logic problems, opening the door for further extensions (e.g., stochastic variables, relational operators).