Incorrect saturations for problems containing FOOL

[ibnyusuf]

Under certain circumstances, we incorrectly claim saturations for FOOL problems.

This happens when we use a preprocessing technique that gets rid of equalities such as inequality splitting or equality proxy. When setting up the saturation algorithm, we do not add superposition, as the problem no longer contains equalities. However, FOOLParamodulation can reintroduce equalities into the problem. Without superposition (and related rules) to deal with these equalities we can then saturate incorrectly.

[easychair]

What is a FOOL problem? As a side note, inequality splitting preserves satisfiability. Equality proxy can turn an unsatisfiable problem into a satisfiable one. Andrei

…

On Wed, 14 Jun 2023 at 12:17, ibnyusuf ***@***.***> wrote: Under certain circumstances, we incorrectly claim saturations for FOOL problems. This happens when we use a preprocessing technique that gets rid of equalities such as inequality splitting or equality proxy. When setting up the saturation algorithm, we do not add superposition, as the problem no longer contains equalities. However, FOOLParamodulation can reintroduce equalities into the problem. Without superposition (and related rules) to deal with these equalities we can then saturate incorrectly. — Reply to this email directly, view it on GitHub <#454>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABVY4BIOGBGYFYHH75YO5S3XLGMWJANCNFSM6AAAAAAZGGOCAI> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[ibnyusuf]

A problem containing terms of interpreted Boolean sort.

Right, so we don't need to worry about equlity proxy in that case since we can't saturate. Only inequality splitting.

@quickbeam123, this seems to be pretty much a corner case. Perhaps the solution that we implemented on the HOL branch will be suitable for master as well.

[quickbeam123]

I think, this still stays relevant with ep=RSTC. But yes, the fix from the HOL branch could be tried. It seems we are talking of a very cornerny corner case.

[easychair]

Yes, ep=RSTC preserves completeness, but it is hardly useful for anything. A

…

On Sat, 17 Jun 2023 at 07:10, Martin Suda ***@***.***> wrote: I think, this still stays relevant with ep=RSTC. But yes, the fix from the HOL branch could be tried. It seems we are talking of a very cornerny corner case. — Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you commented.Message ID: ***@***.***>