Questions tagged [optimathsat]
21 questions
4
votes
2 answers
Timeout for Z3 Optimize
How do you set a timeout for the z3 optimizer such that it will give you the best known solution when it runs out of time?
from z3 import *
s = Optimize()
# Hard Problem
print(s.check())
print(s.model())
Follow-up question, can you set z3 to…
HiDefender
- 2,088
- 2
- 14
- 31
3
votes
1 answer
Gap tolerance control in Z3 optimization
I would like to use z3 optimize class to get sub-optimal results, while still being able to control how far am I from the optimum result. I am using the C++ API.
As an example, CPLEX has the parameters epgap and epagap for relative and absolute…
3
votes
1 answer
Unsatisfiable solution with `constraint forall(i in x)( x[i] <= x[i+1] );`
I'm working on a toy problem to learn minizinc. Take an array (hardcoded to size 3 for now) of values between 0 and 9 and find the combinations where the sum is equal to the product.
par int: n = 3; % hardcode for now
array[1..n] of var 0..9:…
Chris Snow
- 23,813
- 35
- 144
- 309
3
votes
3 answers
z3 control preference for model return values
Question: Is it possible to control some sort of preference for model return values in z3?
Example: Given the following propositional logic formula, there are 2 possible models.
a: True, b: True, c: False (preferred)
a: True, b: False, c: True…
timmwagener
- 2,368
- 2
- 19
- 27
2
votes
1 answer
How to Solve Vertex Cover Problem by SAT and Optimization?
So right now I am working on using SAT to resolve the minimum vertex cover problem, and here is my encoding for the graph G = {V,E} has k vertex cover, and here are the clauses:
Let n = sizeof(V);
Firstly, at lease one vertex is in the vertex…
RobinXu
- 23
- 6
2
votes
1 answer
Minizinc. Count number of shifts in a cycle
Continuing with the other post ( Minizinc: generate a valid shift ). I am trying to have a maximum of 2 im between double ls. Doing this with a regular constraint is quite hard as the transition table would be quite big (too many paths). Is there…
trxw
- 63
- 6
2
votes
2 answers
How to maximize a var int that is larger than 32 bits?
I am using minizinc with built-in Gecode 6.1.1 and I want to maximize an objective function with values that are far greater than the max int 32.
The maximum value of an integer with 32 bits is 2147483646. While not much information seems to be…
Spyros K
- 2,480
- 1
- 20
- 37
2
votes
1 answer
Z3 Optimization, strict inqualities
I'm having a problem which was referred to before where I do not quite get the solution (combining substitute with simplify). In my encoding, I have strict inequalities and I would need to set the epsilon either to 0 or to a very small value. For…
Nils Jansen
- 21
- 1
1
vote
1 answer
What conversion operators are available in Z3 and CVC4 for Bit-Vectors?
I am writing a BV encoding of a problem which requires converting
some Int to BitVec and viceversa.
In mathsat/optimathsat one can use:
((_ to_bv BITS) ) ; Int => BitVec
(sbv_to_int ) ; Signed BitVec => Int
(ubv_to_int…
Patrick Trentin
- 7,126
- 3
- 23
- 40
1
vote
2 answers
MiniZinc Geocode not printing all solutions to CSP with "all" solutions enabled
The Issue
With solve minimize I only get one solution, even though there are multiple optimal solutions. I have enabled printout of multiple solutions in the solver configurations. The other optimal solutions are found with solve satisfy, along with…
Mats
- 165
- 1
- 3
- 14
1
vote
1 answer
parallel execution with a fixed order
#!/bin/bash
doone() {
tracelength="$1"
short="$2"
long="$3"
ratio="$4"
echo "$tracelength $short $long $ratio" >> results.csv
python3 main.py "$tracelength" "$short" "$long" "$ratio" >> file.smt2
gtime -f "%U"…
basel117
- 189
- 1
- 10
1
vote
1 answer
Correct order of parallel execution of shell `time` command
I need to execute the command below (as part of a script) but I don't know in what order to put things so that it executes correctly. What I am trying to do is to give file.smt2 as input to optimathsat, execute it, get the execution time. But I…
basel117
- 189
- 1
- 10
1
vote
1 answer
parralelizing a part of a script shell
#!/bin/bash
for tracelength in 10 20 50 100 ; do
step=0.1
short=0
long=1
for firstloop in {1..10}; do
ratio=0
for secondloop in {1..10} ; do
for repeat in {1..20} ; do
echo $tracelength…
basel117
- 189
- 1
- 10
1
vote
1 answer
Can I get a solution using "timeout" when using Optimize.minimize()?
I'm trying to minimize a variable, but z3 takes to long in order to give me a solution.
And I would like to know if it's possible to get a solution when timeout gets triggered.
If yes how can i do that?
Thx in advance!
Andre Oliveira
- 45
- 6
1
vote
1 answer
runtime.getruntime.exec does not recognize executable file
I am using Runtime.getRuntime().exec() method for running 'optimathsat.exe' file. My code is like
public boolean runOptimathSat() throws InterruptedException {
boolean runSucceed = false;
smtInputFileDirectory = getInputDirectory();
…
Alireza Parvizimosaed
- 365
- 1
- 5
- 13