FASILL documentation Source fasill_tuning_smt

Tuning with SAT/SMT solvers

This library provides predicates for tuning FASILL programs using SAT/SMT solvers.

In order to increase the performance of the original tuning techniques, we make use of the powerful and well-known SAT/SMT solver Z3:

  1. Firstly, the lattice of truth degrees of the FASILL program to be tuned is translated to Z3 syntax.

  2. Next, the set of sfca's obtained after partially evaluating the test cases introduced a priori by the user are also automatically coded as a Z3 formula.

  3. Finally, the Z3 solver is launched in order to minimize the deviation of the solutions w.r.t. the set of test cases while checking the satisfiability of such formula.

For more details see:

  • Riaza, José A., and Ginés Moreno. "Using SAT/SMT solvers for efficiently tuning fuzzy logic programs." 2020 IEEE International Conference on Fuzzy Systems (FUZZ-IEEE). IEEE, 2020. https://doi.org/10.1109/FUZZ48607.2020.9177798

tuning_smt/4

tuning_smt( +Domain, +LatFile, ?Substitution, ?Deviation )

This predicate succeeds when Substitution is the best symbolic substitution for the set of test cases loaded into the current environment, with deviation Deviation. LatFile is an SMT-LIB script representing the corresponding Prolog lattice.

tuning_smt_answer/3

tuning_smt_answer( +Z3answer, ?Substitution, ?Deviation )

This predicate succeeds when Z3answer is the answer of the Z3 solver and Substitution is the best symbolic substitution of the tuning process with deviation Deviation.

tuning_smt_decl_const/3

tuning_smt_decl_const( +Domain, +FASILL, ?SMTLIB )

This predicate succeeds when FASILL is a list of symbolic FASILL constants and SMTLIB is a list of declarations of that constants in SMT-LIB.

tuning_smt_members/2

tuning_smt_members( +Constants, ?Members )

This predicate succeeds when Constants is a list of symbolic FASILL constants and Members is a list of membering assertions of that constants in SMT-LIB.

tuning_smt/1

tuning_smt( ?Minimize )

This predicate succeeds when Minimize is the command to minimize the set of tests cases w.r.t. the expected truth degrees.

testcase_to_smtlib/2

testcase_to_smtlib( +SFCA, ?SMTLIB )

This predicate succeeds when SFCA is a valid FASILL term representing a symbolic fuzzy computed answer and SMTLIB is the corresponding answer in SMT-LIB format.

tuning_theory_options/2

tuning_theory_options( +Theory, -Options )

This predicate succeeds when Options is a list of options in SMT-LIB format for the theory Theroy.