python (65.2k questions)

javascript (44.3k questions)

reactjs (22.7k questions)

java (20.8k questions)

c# (17.4k questions)

html (16.3k questions)

r (13.7k questions)

android (13k questions)

Questions - z3

Unbounded Infinite vs Bounded Infinite Domain for Universal Quantification over Reals in z3

This is a bit of a theoretical question. I was wondering if there's a difference in performance of z3 when solving universally quantified formulas over reals where the quantification is over a bounded...
test-img

Kshitij Goyal

z3

smt

z3py

quantifiers

Votes: 0

Answers: 1

Latest Answer

The inner workings of most SMT solvers is black-box, where many heuristics/algorithms are in play. For arithmetic however, there are well-known techniques to deal with interesting fragments. I'd recom...
test-img

alias

SAT Core similar to UNSAT Core

I know that there is the possibility to obtain an UNSAT-Core in Z3. But is it also possible to get something you might call SAT-Core? That means if we have a satisfiable instance then there is also a ...
test-img

Daniel Binkele-Raible

z3

Votes: 0

Answers: 1

Latest Answer

I don't think this is a well-defined concept; think about having two variables a and b, with the constraint a = Not(b), and you assert both a and b. No matter which you pick, the other is determined b...
test-img

alias

Z3 Not Showing Infinity on Unbounded Optimization in Python

I am new to Z3 and trying the examples found here, implementing the examples in python. When I try the examples in the "Unbounded Objectives" section I get seemingly random integer values (n...
test-img

Jonathan

python

z3

smt

z3py

Votes: 0

Answers: 1

Latest Answer

You're not quite using the API correctly. You should use the value function on the optimization goal instead. For instance, your second query is coded as: from z3 import * x, y, profit = Ints('x y pr...
test-img

alias

z3 much slower than ortools SAT. Why?

I am trying out different solvers for a toy clique problem and was surprised to find that ortools using SAT seems much faster than z3. I am wondering if I am doing something wrong given that z3 does s...
test-img

Simd

python

z3

or-tools

z3py

sat

Votes: 0

Answers: 2

Latest Answer

Replacing the Int variables by Bool variables reduced the z3py runtime by 28% on my machine: z3.set_option(verbose=1) myVars = [] for i in range(num_variables): myVars += [z3.Bool('v%d' % i)] # ...
test-img

Axel Kemper

Posts

Questions

Blogs

Jobs