mirror of
https://github.com/Z3Prover/z3
synced 2025-10-08 08:51:55 +00:00
Implement max PB constraints optimization feature
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
parent
cb039c95aa
commit
016539cd61
5 changed files with 257 additions and 1 deletions
|
@ -345,6 +345,21 @@ namespace opt {
|
|||
m_optsmt.setup(*m_opt_solver.get());
|
||||
update_lower();
|
||||
|
||||
// Try to detect and optimize max PB constraints pattern before deciding optimization strategy
|
||||
if (m_objectives.size() > 1) {
|
||||
expr_ref_vector maxsat_terms(m);
|
||||
vector<rational> maxsat_weights;
|
||||
rational maxsat_offset;
|
||||
bool maxsat_neg;
|
||||
symbol maxsat_id;
|
||||
|
||||
if (detect_max_pb_constraints(maxsat_terms, maxsat_weights, maxsat_offset, maxsat_neg, maxsat_id)) {
|
||||
TRACE(opt, tout << "Max PB pattern detected, switching to single maxsat objective\n";);
|
||||
// The pattern was detected and objectives were modified by detect_max_pb_constraints
|
||||
// Now we have a single objective, so we can process it as such
|
||||
}
|
||||
}
|
||||
|
||||
switch (m_objectives.size()) {
|
||||
case 0:
|
||||
break;
|
||||
|
@ -1077,12 +1092,135 @@ namespace opt {
|
|||
neg = is_max;
|
||||
std::ostringstream out;
|
||||
out << mk_bounded_pp(orig_term, m, 2) << ':' << index;
|
||||
id = symbol(out.str());
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool context::detect_max_pb_constraints(expr_ref_vector& terms,
|
||||
vector<rational>& weights, rational& offset,
|
||||
bool& neg, symbol& id) {
|
||||
// This function detects when we have multiple maximize objectives that are PB constraints
|
||||
// and transforms them to use auxiliary variables.
|
||||
//
|
||||
// Pattern: maximize { PB1, ..., PBn } where each PB_i is a weighted sum of Boolean variables
|
||||
// Transform to: PB_i >= k => p_i_k for k = 1, ..., max_potential_sum(PB_i)
|
||||
// maximize sum(p_i_k for all i,k)
|
||||
|
||||
TRACE(opt, tout << "detect_max_pb_constraints called with " << m_objectives.size() << " objectives\n";);
|
||||
|
||||
unsigned num_maximize_objs = 0;
|
||||
vector<unsigned> max_indices;
|
||||
vector<expr_ref_vector> pb_terms;
|
||||
vector<vector<rational>> pb_weights;
|
||||
vector<rational> pb_offsets;
|
||||
|
||||
// First pass: collect all maximize objectives that are PB constraints
|
||||
for (unsigned idx = 0; idx < m_objectives.size(); ++idx) {
|
||||
objective const& obj = m_objectives[idx];
|
||||
TRACE(opt, tout << "Objective " << idx << " type: " << obj.m_type << "\n";);
|
||||
if (obj.m_type == O_MAXIMIZE && obj.m_term) {
|
||||
expr_ref_vector pb_terms_i(m);
|
||||
vector<rational> pb_weights_i;
|
||||
rational pb_offset_i;
|
||||
|
||||
if (get_pb_sum(obj.m_term, pb_terms_i, pb_weights_i, pb_offset_i)) {
|
||||
max_indices.push_back(idx);
|
||||
pb_terms.push_back(pb_terms_i);
|
||||
pb_weights.push_back(pb_weights_i);
|
||||
pb_offsets.push_back(pb_offset_i);
|
||||
num_maximize_objs++;
|
||||
TRACE(opt, tout << "Objective " << idx << " is a PB constraint with " << pb_terms_i.size() << " terms\n";);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
TRACE(opt, tout << "Found " << num_maximize_objs << " PB maximize objectives\n";);
|
||||
|
||||
// Only apply transformation if we have multiple PB maximize objectives
|
||||
if (num_maximize_objs < 2) {
|
||||
return false;
|
||||
}
|
||||
|
||||
TRACE(opt, tout << "Detected " << num_maximize_objs << " PB maximize objectives, applying transformation\n";);
|
||||
|
||||
// Clear output vectors
|
||||
terms.reset();
|
||||
weights.reset();
|
||||
offset = rational::zero();
|
||||
neg = true; // We negate because we convert maximize to maxsat (minimizing penalty)
|
||||
|
||||
arith_util arith(m);
|
||||
|
||||
// For each PB constraint, create auxiliary variables and constraints
|
||||
for (unsigned i = 0; i < num_maximize_objs; ++i) {
|
||||
expr_ref_vector const& pb_terms_i = pb_terms[i];
|
||||
vector<rational> const& pb_weights_i = pb_weights[i];
|
||||
rational const& pb_offset_i = pb_offsets[i];
|
||||
|
||||
// Calculate maximum potential sum for this PB constraint
|
||||
rational max_sum = pb_offset_i;
|
||||
for (unsigned j = 0; j < pb_weights_i.size(); ++j) {
|
||||
if (pb_weights_i[j].is_pos()) {
|
||||
max_sum += pb_weights_i[j];
|
||||
}
|
||||
}
|
||||
|
||||
TRACE(opt, tout << "PB constraint " << i << " has max sum " << max_sum << "\n";);
|
||||
|
||||
// Create auxiliary variables p_i_k for k = 1 to max_sum
|
||||
for (rational k = rational::one(); k <= max_sum; k += rational::one()) {
|
||||
std::ostringstream aux_name;
|
||||
aux_name << "pb_aux_" << i << "_" << k.to_string();
|
||||
expr_ref aux_var(m.mk_const(symbol(aux_name.str()), m.mk_bool_sort()), m);
|
||||
|
||||
// Create PB constraint: sum(pb_weights_i[j] * pb_terms_i[j]) for j
|
||||
expr_ref pb_sum(arith.mk_numeral(pb_offset_i, true), m);
|
||||
for (unsigned j = 0; j < pb_terms_i.size(); ++j) {
|
||||
expr_ref weighted_term(arith.mk_mul(arith.mk_numeral(pb_weights_i[j], true),
|
||||
m.mk_ite(pb_terms_i[j], arith.mk_numeral(rational::one(), true), arith.mk_numeral(rational::zero(), true))), m);
|
||||
pb_sum = arith.mk_add(pb_sum, weighted_term);
|
||||
}
|
||||
|
||||
// Add constraint: pb_sum >= k => aux_var
|
||||
expr_ref constraint(m.mk_implies(arith.mk_ge(pb_sum, arith.mk_numeral(k, true)), aux_var), m);
|
||||
add_hard_constraint(constraint);
|
||||
|
||||
// Add auxiliary variable to maximize
|
||||
terms.push_back(aux_var);
|
||||
weights.push_back(rational::one());
|
||||
offset += rational::one();
|
||||
}
|
||||
}
|
||||
|
||||
// Now modify m_objectives to replace the multiple maximize objectives with a single maxsat objective
|
||||
// Find the first maximize objective to replace
|
||||
unsigned target_index = max_indices[0];
|
||||
objective& obj = m_objectives[target_index];
|
||||
obj.m_id = symbol("max_pb_unified");
|
||||
obj.m_type = O_MAXSMT;
|
||||
obj.m_term = nullptr;
|
||||
obj.m_terms.reset();
|
||||
obj.m_terms.append(terms);
|
||||
obj.m_weights.reset();
|
||||
obj.m_weights.append(weights);
|
||||
obj.m_adjust_value.set_offset(offset);
|
||||
obj.m_adjust_value.set_negate(neg);
|
||||
|
||||
// Remove other maximize objectives that were converted (in reverse order to maintain indices)
|
||||
for (int i = max_indices.size() - 1; i >= 1; --i) {
|
||||
unsigned idx_to_remove = max_indices[i];
|
||||
m_objectives.erase(m_objectives.begin() + idx_to_remove);
|
||||
}
|
||||
|
||||
// Create a unique ID for this transformation
|
||||
id = symbol("max_pb_unified");
|
||||
|
||||
TRACE(opt, tout << "Transformed to " << terms.size() << " auxiliary variables, " << m_objectives.size() << " objectives remaining\n";);
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
expr* context::mk_objective_fn(unsigned index, objective_t ty, unsigned sz, expr*const* args) {
|
||||
ptr_vector<sort> domain;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
|
@ -1119,6 +1257,7 @@ namespace opt {
|
|||
void context::from_fmls(expr_ref_vector const& fmls) {
|
||||
TRACE(opt, tout << fmls << "\n";);
|
||||
m_hard_constraints.reset();
|
||||
|
||||
for (expr * fml : fmls) {
|
||||
app_ref tr(m);
|
||||
expr_ref orig_term(m);
|
||||
|
|
|
@ -313,6 +313,9 @@ namespace opt {
|
|||
bool is_maxsat(expr* fml, expr_ref_vector& terms,
|
||||
vector<rational>& weights, rational& offset, bool& neg,
|
||||
symbol& id, expr_ref& orig_term, unsigned& index);
|
||||
bool detect_max_pb_constraints(expr_ref_vector& terms,
|
||||
vector<rational>& weights, rational& offset,
|
||||
bool& neg, symbol& id);
|
||||
void purify(app_ref& term);
|
||||
app* purify(generic_model_converter_ref& fm, expr* e);
|
||||
bool is_mul_const(expr* e);
|
||||
|
|
10
test_pb_max.smt2
Normal file
10
test_pb_max.smt2
Normal file
|
@ -0,0 +1,10 @@
|
|||
(declare-fun x1 () Bool)
|
||||
(declare-fun x2 () Bool)
|
||||
(declare-fun y1 () Bool)
|
||||
(declare-fun y2 () Bool)
|
||||
|
||||
; Create two PB maximize objectives - must be integer expressions
|
||||
(maximize (+ (ite x1 2 0) (ite x2 1 0))) ; PB1: max = 3
|
||||
(maximize (+ (ite y1 1 0) (ite y2 2 0))) ; PB2: max = 3
|
||||
|
||||
(check-sat)
|
BIN
test_pb_optimization
Executable file
BIN
test_pb_optimization
Executable file
Binary file not shown.
104
test_pb_optimization.cpp
Normal file
104
test_pb_optimization.cpp
Normal file
|
@ -0,0 +1,104 @@
|
|||
#include "z3++.h"
|
||||
#include <iostream>
|
||||
|
||||
using namespace z3;
|
||||
|
||||
void test_pb_max_pattern() {
|
||||
std::cout << "Testing PB max pattern detection\n";
|
||||
|
||||
context c;
|
||||
|
||||
// Create boolean variables
|
||||
expr x1 = c.bool_const("x1");
|
||||
expr x2 = c.bool_const("x2");
|
||||
expr x3 = c.bool_const("x3");
|
||||
expr y1 = c.bool_const("y1");
|
||||
expr y2 = c.bool_const("y2");
|
||||
expr z1 = c.bool_const("z1");
|
||||
expr z2 = c.bool_const("z2");
|
||||
expr z3 = c.bool_const("z3");
|
||||
|
||||
// Create PB constraints like weighted sums
|
||||
expr pb1 = 2*ite(x1, c.int_val(1), c.int_val(0)) + 3*ite(x2, c.int_val(1), c.int_val(0)) + ite(x3, c.int_val(1), c.int_val(0)); // potential max = 6
|
||||
expr pb2 = ite(y1, c.int_val(1), c.int_val(0)) + 2*ite(y2, c.int_val(1), c.int_val(0)); // potential max = 3
|
||||
expr pb3 = ite(z1, c.int_val(1), c.int_val(0)) + ite(z2, c.int_val(1), c.int_val(0)) + ite(z3, c.int_val(1), c.int_val(0)); // potential max = 3
|
||||
|
||||
optimize opt(c);
|
||||
|
||||
// The pattern the issue might be referring to:
|
||||
// Instead of maximizing pb1 + pb2 + pb3 directly,
|
||||
// we should detect the pattern and introduce auxiliary variables
|
||||
|
||||
// Current approach: maximize pb1 + pb2 + pb3
|
||||
opt.maximize(pb1 + pb2 + pb3);
|
||||
|
||||
std::cout << "check: " << opt.check() << std::endl;
|
||||
|
||||
if (opt.check() == sat) {
|
||||
model m = opt.get_model();
|
||||
std::cout << "Model: " << m << std::endl;
|
||||
|
||||
// Get objective values
|
||||
std::cout << "Objectives: " << opt.objectives().size() << std::endl;
|
||||
}
|
||||
}
|
||||
|
||||
void test_pb_max_with_constraints() {
|
||||
std::cout << "\nTesting what the issue might want - auxiliary variables\n";
|
||||
|
||||
context c;
|
||||
|
||||
// Create boolean variables
|
||||
expr x1 = c.bool_const("x1");
|
||||
expr x2 = c.bool_const("x2");
|
||||
expr y1 = c.bool_const("y1");
|
||||
expr y2 = c.bool_const("y2");
|
||||
|
||||
// PB expressions
|
||||
expr pb1 = 2*ite(x1, c.int_val(1), c.int_val(0)) + ite(x2, c.int_val(1), c.int_val(0)); // max = 3
|
||||
expr pb2 = ite(y1, c.int_val(1), c.int_val(0)) + 2*ite(y2, c.int_val(1), c.int_val(0)); // max = 3
|
||||
|
||||
optimize opt(c);
|
||||
|
||||
// What the issue might want: auxiliary variables p_k for each threshold k
|
||||
// For pb1: p1_1, p1_2, p1_3 where pb1 >= k => p1_k
|
||||
// For pb2: p2_1, p2_2, p2_3 where pb2 >= k => p2_k
|
||||
// Then maximize: p1_1 + p1_2 + p1_3 + p2_1 + p2_2 + p2_3
|
||||
|
||||
expr p1_1 = c.bool_const("p1_1");
|
||||
expr p1_2 = c.bool_const("p1_2");
|
||||
expr p1_3 = c.bool_const("p1_3");
|
||||
expr p2_1 = c.bool_const("p2_1");
|
||||
expr p2_2 = c.bool_const("p2_2");
|
||||
expr p2_3 = c.bool_const("p2_3");
|
||||
|
||||
// Add constraints: pb_i >= k => p_k
|
||||
opt.add(implies(pb1 >= 1, p1_1));
|
||||
opt.add(implies(pb1 >= 2, p1_2));
|
||||
opt.add(implies(pb1 >= 3, p1_3));
|
||||
opt.add(implies(pb2 >= 1, p2_1));
|
||||
opt.add(implies(pb2 >= 2, p2_2));
|
||||
opt.add(implies(pb2 >= 3, p2_3));
|
||||
|
||||
// Maximize auxiliary variables
|
||||
opt.maximize(ite(p1_1, c.int_val(1), c.int_val(0)) + ite(p1_2, c.int_val(1), c.int_val(0)) + ite(p1_3, c.int_val(1), c.int_val(0)) + ite(p2_1, c.int_val(1), c.int_val(0)) + ite(p2_2, c.int_val(1), c.int_val(0)) + ite(p2_3, c.int_val(1), c.int_val(0)));
|
||||
|
||||
std::cout << "check: " << opt.check() << std::endl;
|
||||
|
||||
if (opt.check() == sat) {
|
||||
model m = opt.get_model();
|
||||
std::cout << "Model: " << m << std::endl;
|
||||
|
||||
// Evaluate original PB expressions
|
||||
std::cout << "pb1 = " << m.eval(pb1) << std::endl;
|
||||
std::cout << "pb2 = " << m.eval(pb2) << std::endl;
|
||||
|
||||
std::cout << "Objectives: " << opt.objectives().size() << std::endl;
|
||||
}
|
||||
}
|
||||
|
||||
int main() {
|
||||
test_pb_max_pattern();
|
||||
test_pb_max_with_constraints();
|
||||
return 0;
|
||||
}
|
Loading…
Add table
Add a link
Reference in a new issue