Optimization

from z3 import *

# Create optimization context
opt = Optimize()

# Add hard constraints (must be satisfied)
x = Int('x')
y = Int('y')
opt.add(x > 0, y > 0, x + y < 10)

# Add optimization objectives
opt.maximize(x + y)  # Maximize the sum

# Check and get result
if opt.check() == sat:
    m = opt.model()
    print(f"x = {m[x]}, y = {m[y]}")
    print(f"Optimal value: {m.eval(x + y)}")

from z3 import *

opt = Optimize()

# Variables
x, y = Reals('x y')

# Constraints
opt.add(x >= 0, y >= 0)
opt.add(x + 2*y >= 8)
opt.add(2*x + y >= 10)

# Minimize cost function
cost = 3*x + 4*y
opt.minimize(cost)

if opt.check() == sat:
    m = opt.model()
    print(f"Minimum cost: {m.eval(cost)}")
    print(f"x = {m[x]}, y = {m[y]}")

from z3 import *

opt = Optimize()

# Boolean variables representing preferences
p1, p2, p3 = Bools('p1 p2 p3')

# Hard constraint: at least one must be true
opt.add(Or(p1, p2, p3))

# Soft constraints with weights
opt.add_soft(p1, weight=10)      # Prefer p1 (weight 10)
opt.add_soft(p2, weight=5)       # Prefer p2 (weight 5)
opt.add_soft(Not(p3), weight=3)  # Prefer p3 to be false (weight 3)

if opt.check() == sat:
    m = opt.model()
    print(f"p1={m[p1]}, p2={m[p2]}, p3={m[p3]}")

from z3 import *

opt = Optimize()
x = Int('x')

# Add soft constraints with group identifiers
opt.add_soft(x > 5, weight=1, id='group1')
opt.add_soft(x < 10, weight=1, id='group1')
opt.add_soft(x % 2 == 0, weight=2, id='group2')

if opt.check() == sat:
    print(opt.model())

from z3 import *

opt = Optimize()

x, y, z = Ints('x y z')

# Constraints
opt.add(x >= 0, y >= 0, z >= 0)
opt.add(x + y + z <= 100)

# Multiple objectives (in priority order)
h1 = opt.maximize(x)        # First priority: maximize x
h2 = opt.maximize(y)        # Second priority: maximize y
h3 = opt.minimize(z)        # Third priority: minimize z

if opt.check() == sat:
    m = opt.model()
    print(f"x = {m[x]}, y = {m[y]}, z = {m[z]}")
    
    # Get bounds for each objective
    print(f"Objective 0 bounds: {opt.lower(h1)} - {opt.upper(h1)}")
    print(f"Objective 1 bounds: {opt.lower(h2)} - {opt.upper(h2)}")
    print(f"Objective 2 bounds: {opt.lower(h3)} - {opt.upper(h3)}")

from z3 import *

opt = Optimize()
x = Int('x')

opt.add(x >= 0)
opt.maximize(x)

opt.push()
opt.add(x <= 10)
print(opt.check())  # sat, x=10

opt.pop()
opt.push()
opt.add(x <= 5)
print(opt.check())  # sat, x=5

from z3 import *

opt = Optimize()
x = Int('x')

opt.add(x >= 0, x <= 100)
opt.maximize(x)

# Hint: start search near x=50
opt.set_initial_value(x, IntVal(50))

opt.check()
print(opt.model())

from z3 import *

opt = Optimize()
x = Real('x')

opt.add(x >= 0, x <= 10)
h = opt.maximize(x * x)

if opt.check() == sat:
    print(f"Lower bound: {opt.lower(h)}")
    print(f"Upper bound: {opt.upper(h)}")
    
    # For more precise bounds with infinitesimals
    lower_vec = opt.lower_as_vector(h)
    print(f"Lower vector: {lower_vec}")  # [infinity_coeff, value, epsilon_coeff]

from z3 import *

# Allocate tasks to workers minimizing total time
opt = Optimize()

# 3 workers, 5 tasks
# task_time[i] = time required for task i
task_times = [3, 5, 2, 7, 4]
num_workers = 3
num_tasks = len(task_times)

# assignment[i] = worker assigned to task i (0, 1, or 2)
assignment = [Int(f'task_{i}') for i in range(num_tasks)]

# Each task assigned to a valid worker
for i in range(num_tasks):
    opt.add(assignment[i] >= 0, assignment[i] < num_workers)

# Calculate total time for each worker
worker_time = [Int(f'worker_{w}_time') for w in range(num_workers)]

for w in range(num_workers):
    time_expr = Sum([If(assignment[i] == w, task_times[i], 0) 
                     for i in range(num_tasks)])
    opt.add(worker_time[w] == time_expr)

# Minimize maximum worker time (makespan)
makespan = Int('makespan')
for w in range(num_workers):
    opt.add(makespan >= worker_time[w])

opt.minimize(makespan)

if opt.check() == sat:
    m = opt.model()
    print(f"Minimum makespan: {m[makespan]}")
    for i in range(num_tasks):
        worker = m[assignment[i]].as_long()
        print(f"Task {i} (time={task_times[i]}) -> Worker {worker}")
    for w in range(num_workers):
        print(f"Worker {w} total time: {m[worker_time[w]]}")

#include <z3.h>

Z3_context ctx = Z3_mk_context(cfg);
Z3_optimize opt = Z3_mk_optimize(ctx);

// Add hard constraint
Z3_optimize_assert(ctx, opt, constraint);

// Add soft constraint with weight
unsigned id = Z3_optimize_assert_soft(ctx, opt, soft_constraint, "10", Z3_mk_string_symbol(ctx, ""));

// Add objective
unsigned h = Z3_optimize_maximize(ctx, opt, objective_expr);

// Check satisfiability
Z3_lbool result = Z3_optimize_check(ctx, opt, 0, NULL);

if (result == Z3_L_TRUE) {
    Z3_model m = Z3_optimize_get_model(ctx, opt);
    // Get bounds
    Z3_ast lower = Z3_optimize_get_lower(ctx, opt, h);
    Z3_ast upper = Z3_optimize_get_upper(ctx, opt, h);
}

Z3_optimize_dec_ref(ctx, opt);

opt.set('maxsat_engine', 'maxres')  # MaxSAT engine: 'core_maxsat', 'maxres', 'pd-maxres'
opt.set('opt.priority', 'box')       # Multi-objective: 'lex', 'box', 'pareto'
opt.set('timeout', 10000)            # Timeout in milliseconds