8000 Slow performance on simple inequality · Issue #7329 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Slow performance on simple inequality #7329

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and co 8000 ntact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
ds0ayane opened this issue Aug 3, 2024 · 1 comment
Closed

Slow performance on simple inequality #7329

ds0ayane opened this issue Aug 3, 2024 · 1 comment

Comments

@ds0ayane
Copy link
ds0ayane commented Aug 3, 2024

Hi, z3 runs slowly on this instance:

$ cat slow.smt2
(declare-fun i0 () Int)
(assert (<= 1 (- i0 (* 32 32 32 i0 i0 i0 i0))))
(check-sat)
$ timeout -s 9 30 z3 slow.smt2
Killed

while cvc5 can solve it immediately.

$ time cvc5 slow.smt2
unsat

real    0m0.018s
user    0m0.014s
sys     0m0.005s
NikolajBjorner added a commit that referenced this issue Aug 3, 2024
@NikolajBjorner
add max conflict throttle to SAT based QFNIA tactic #7329
26b8d63 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
Copy link
Contributor

It is a general issue with the qfnia tactic. It uses a SAT solver to check for small models, but this solver may take all resources.
It is not obvious the SAT solver should run first (or at all). I am setting a max-conflict on this to throttle it.
It is generally observed that the SAT tactic can even be removed and the solver then handles more qfnia benchmarks.
Fine tuning and experimentation with how to optimize tactic use or harness the SAT backend is more effort than adding this throttle.

arbipher pushed a commit to arbipher/z3 that referenced this issue Apr 17, 2025
@NikolajBjorner @arbipher
add max conflict throttle to SAT based QFNIA tactic Z3Prover#7329
c1d01fb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@NikolajBjorner @ds0ayane
0