How to speedup the performance of Z3 solver?

More Rehab Shahin's questions See All

How can I measure MMP-1 protein activity or protein level from liver tissue?

Instead of checking only the mRNA level, I want to check the active protein level of MMP-1 in Liver tissue from mice. How can I do that?

03 March 2021 1,763 2 View

Binary Logistic Generalized Linear Mixed model in SPSS. Is it doable?

I want to analyses the proportion of swimming sperm of three species of fish in two salinities. To analyse the proportion of swimming sperm in a Generalized Linear Model, I would use a Binary...

03 March 2021 2,297 3 View

Looking for Materials with high thermal expansion coefficient and high temperature resistance?

03 March 2021 8,272 1 View

Guidelines for survey (question type) analysis?

Hi. Please tell me what guidelines should i need to follow for questionaries' type research work in India. It is not hospital based work, we are conduction basic institutional based qualitative...

03 March 2021 2,037 3 View

What are the values needed for gabor filter's parameter for cifar10 data?

Hi, I implemented a code to gabor filter cifar10 data but the images after being filtered and stacked are not clear like the original images. I think the problem is in the way I am using the...

03 March 2021 6,317 1 View

Can we block unwanted images during the x-ray prediction?

i am try to classify the x-ray images. During classification , can i block unwanted images (except x-ray image).

03 March 2021 7,100 1 View

No title

03 March 2021 5,360 2 View

What techniques can I use to determine the miscibility of polymer blends?

The term miscibility refers to the single-phase state in thermodynamics. I do not mean the compatibility of different components. To determine the miscibility I know several techniques such as...

03 March 2021 4,107 4 View

Sample dilution for quantitative analysis using ELISA?

If the detection range is in ng/ml but the reference range is in ug/ml for a molecule or protein in serum or plasma .how to dilute and what is the initial volume to be taken for quantitative analysis

02 March 2021 7,670 3 View

The procedure compute?

02 March 2021 5,204 3 View

How can i resolve the "final solutuin is not converged" error in Comsol for my heat transfer simulation??

I have been trying to simulate heat transfer problem in Comsol 5.5 for long time but it always throw an error stating: "Failed to find a solution. Maximum number of Newton iterations...

28 February 2021 8,626 3 View

High aspect ratio hexahedral mesh optimization solver?

I am interested in evaluating mesh optimization solvers that converge to high aspect ratio unstructured hexahedral grids. In other words, I am interested in a solver that optimizes warpage,...

26 February 2021 7,279 2 View

Error in comsol?

Dear respected researchers, while performing CFD analysis in Comsol it's showing like this Error: Nonlinear solver did not converge. The maximum number of Newton iterations reached can...

24 February 2021 249 3 View

Implementation of chance-constrained optimization problem via scenario approach?

23 February 2021 7,826 2 View

Should I use Pressure Based Solver or a Density-Based Solver?

Dear researchers, I want to simulate a flow (air) in a wind tunnel, and I want to integrate a fluidic actuator inside it in order to control the separation of the boundary layer. At the blower...

22 February 2021 4,882 3 View

How to get better phase shift in C-V curves for ferroelectric devices?

I tried to sweep my ferroelectric devices from -2V to 2V and then from 2V to -2V and The two hysteresis peaks are off by several microFarads. Should i increase bias voltage? I am doing these...

16 February 2021 8,514 2 View

Is there any effective FEM solver to perform simulation of balloon inflation with large deformation (e.g. 300% strain)?

Hi! Thank you for your time, attention, and support. I am currently using FEM solver Abaqus to perform a set of balloon inflation simulations, trying to understand the deformation shape, stress,...

14 February 2021 2,524 4 View

How to model in HFSS or FEKO Free Space Material Characterization?

I am having trouble setting up this problem in HFSS or FEKO. In HFSS, I've tried both FEM and FEBI-IE solvers. With FEKO, I've tried it's MoM solver and default settings. I am would like model...

09 February 2021 375 2 View

Is it possible to report hydrodynamic loads on different parts of an ocean vehicle while 6DOF motion analysis in Ansys Fluent is running?

It seems a 6dof UDF containing vehicle characteristics such as mass and moments of inertia can be used for specifying a boundary as reprentative of ocean vehicle. It is required to have...

03 February 2021 7,726 3 View

How to Fix Floating Point Exception in Fluent?

Hello, I am trying to model a solar cyclone tower (The solar cyclone: A solar chimney for harvesting atmospheric water ) in Fluent. At the moment, I am trying to model a simplified version...

30 January 2021 9,448 3 View

Peter Tiedemann

I think you will have to describe what kind of model you are applying it to in order to get an answer.

Rehab Shahin

@ Peter,

I have a square and a set of line segments, I have to get the location of the square such that it intersects with the most possible number of line segments. I am using Z3 optimizer and C++. I am using a lot of implies and ite statements to calculate the intersection points of each line with the square. It generates the expected results but takes too long time so I am asking if using alot of implies, ite may affect the performane? Is there some configurations that I can use to speedup the execution time

I am not sure this is the best place to ask. Have you considered trying https://github.com/Z3Prover/z3/issues ? Also note that you will have to share your model in more detail, for people to be able to help.

You might also want to consider why specifically you have chosen to use an SMT solver. I am no expert, but i don't necessarily think an SMT solver is the best for this type of problem.

@peter,

"but i don't necessarily think an SMT solver is the best for this type of problem."

Would you please explain why?

Because it seems you don't need boolean logic to express this kind of optimization problem, it sounds like a "pure" geometrical problem.

David Déharbe

@Peter, Pure Boolean is the scope of SAT solver, whereas Z3 is an SMT solver, where the T stands for Theory. The theory involved in this thread seems to be non-linear real arithmetics, for which Z3 has some support. Also Z3 may be used not only for solving, but also for optimizing.

I agree that @Rehab should provide more details on how he expressed his problem in SMT language (or any other format supported by Z3).

@ David Déharbe I am well aware of what an SMT solver is :) My point was that SMT solvers are designed to be able to mix pure boolean with other theories, and i am questioning whether this particular problem needs a boolean part.