mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

initial pass

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-22 14:57:25 -08:00
parent 748ada2acc
commit 43ddad0ecd
5 changed files with 139 additions and 148 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/sat/card_extension.cpp
View file

@ -739,7 +739,8 @@ namespace sat {
void card_extension::add_at_least(bool_var v, literal_vector const& lits, unsigned k) {
unsigned index = 2*m_cards.size();
card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(index, literal(v, false), lits, k);
literal lit = v == null_bool_var ? null_literal : literal(v, false);
card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(index, lit, lits, k);
m_cards.push_back(c);
if (v == null_bool_var) {
// it is an axiom.

130
src/sat/sat_local_search.cpp
View file

@ -24,21 +24,40 @@
namespace sat {
void local_search::init() {
constraint_slack.resize(num_constraints + 1);
cur_solution.resize(num_vars + 1);
// etc. initialize other vectors.
init_greedy();
constraint_slack.resize(num_constraints(), 0);
cur_solution.resize(num_vars(), false);
m_index_in_unsat_stack.resize(num_constraints(), 0);
coefficient_in_ob_constraint.resize(num_vars(), 0);
var_neighbor.reset();
for (bool_var v = 0; v < num_vars(); ++v) {
bool_vector is_neighbor(num_vars(), false);
var_neighbor.push_back(bool_var_vector());
for (unsigned i = 0; i < var_term[v].size(); ++ i) {
unsigned c = var_term[v][i].constraint_id;
for (unsigned j = 0; j < constraint_term[c].size(); ++j) {
bool_var w = constraint_term[c][j].var_id;
if (w == v || is_neighbor[w]) continue;
is_neighbor[w] = true;
var_neighbor.back().push_back(w);
}
}
}
}
void local_search::reinit() {
reinit_greedy();
}
void local_search::init_cur_solution() {
for (unsigned v = 1; v <= num_vars; ++v) {
cur_solution.resize(num_vars() + 1, false);
for (unsigned v = 0; v < num_vars(); ++v) {
cur_solution[v] = (rand() % 2 == 1);
}
}
// figure out slack, and init unsat stack
void local_search::init_slack() {
for (unsigned c = 1; c <= num_constraints; ++c) {
for (unsigned c = 0; c < num_constraints(); ++c) {
for (unsigned i = 0; i < constraint_term[c].size(); ++i) {
unsigned v = constraint_term[c][i].var_id;
if (cur_solution[v] == constraint_term[c][i].sense)
@ -53,7 +72,7 @@ namespace sat {
// figure out variables scores, pscores and sscores
void local_search::init_scores() {
for (unsigned v = 1; v <= num_vars; ++v) {
for (unsigned v = 0; v < num_vars(); ++v) {
for (unsigned i = 0; i < var_term[v].size(); ++i) {
int c = var_term[v][i].constraint_id;
if (cur_solution[v] != var_term[v][i].sense) {
@ -81,8 +100,8 @@ namespace sat {
// init goodvars and okvars stack
void local_search::init_goodvars() {
goodvar_stack.reset();
already_in_goodvar_stack.resize(num_vars+1, false);
for (unsigned v = 1; v <= num_vars; ++v) {
already_in_goodvar_stack.resize(num_vars(), false);
for (unsigned v = 0; v < num_vars(); ++v) {
if (score[v] > 0) { // && conf_change[v] == true
already_in_goodvar_stack[v] = true;
goodvar_stack.push_back(v);
@ -90,7 +109,7 @@ namespace sat {
}
}
void local_search::init_orig() {
void local_search::reinit_orig() {
constraint_slack = constraint_k;
// init unsat stack
@ -102,18 +121,24 @@ namespace sat {
// init varibale information
// variable 0 is the virtual variable
score.resize(num_vars+1, 0); score[0] = INT_MIN;
sscore.resize(num_vars+1, 0); sscore[0] = INT_MIN;
time_stamp.resize(num_vars+1, 0); time_stamp[0] = max_steps;
conf_change.resize(num_vars+1, true); conf_change[0] = false;
cscc.resize(num_vars+1, 1); cscc[0] = 0;
score.reset();
sscore.reset();
time_stamp.reset();
conf_change.reset();
cscc.reset();
score.resize(num_vars(), 0); score[0] = INT_MIN;
sscore.resize(num_vars(), 0); sscore[0] = INT_MIN;
time_stamp.resize(num_vars(), 0); time_stamp[0] = max_steps;
conf_change.resize(num_vars(), true); conf_change[0] = false;
cscc.resize(num_vars(), 1); cscc[0] = 0;
init_slack();
init_scores();
init_goodvars();
}
void local_search::init_greedy() {
void local_search::reinit_greedy() {
constraint_slack = constraint_k;
// init unsat stack
@ -125,14 +150,20 @@ namespace sat {
// init varibale information
// variable 0 is the virtual variable
score.resize(num_vars+1, 0); score[0] = INT_MIN;
sscore.resize(num_vars+1, 0); sscore[0] = INT_MIN;
time_stamp.resize(num_vars+1, 0); time_stamp[0] = max_steps;
conf_change.resize(num_vars+1, true); conf_change[0] = false;
cscc.resize(num_vars+1, 1); cscc[0] = 0;
for (unsigned v = 1; v <= num_vars; ++v) {
score.reset();
sscore.reset();
time_stamp.reset();
conf_change.reset();
cscc.reset();
score.resize(num_vars(), 0); score[0] = INT_MIN;
sscore.resize(num_vars(), 0); sscore[0] = INT_MIN;
time_stamp.resize(num_vars(), 0); time_stamp[0] = max_steps;
conf_change.resize(num_vars(), true); conf_change[0] = false;
cscc.resize(num_vars(), 1); cscc[0] = 0;
for (unsigned v = 0; v < num_vars(); ++v) {
// greedy here!!
if (coefficient_in_ob_constraint[v] != 0)
if (coefficient_in_ob_constraint.get(v, 0) != 0)
cur_solution[v] = (coefficient_in_ob_constraint[v] > 0);
}
@ -162,6 +193,7 @@ namespace sat {
unsigned id = constraint_term.size();
constraint_term.push_back(svector<term>());
for (unsigned i = 0; i < sz; ++i) {
var_term.resize(c[i].var() + 1);
term t;
t.constraint_id = id;
t.var_id = c[i].var();
@ -173,6 +205,7 @@ namespace sat {
}
local_search::local_search(solver& s) {
// copy units
unsigned trail_sz = s.init_trail_size();
for (unsigned i = 0; i < trail_sz; ++i) {
@ -242,10 +275,6 @@ namespace sat {
//
SASSERT(ext->m_xors.empty());
}
num_vars = s.num_vars();
num_constraints = constraint_term.size();
}
local_search::~local_search() {
@ -256,17 +285,18 @@ namespace sat {
}
lbool local_search::operator()() {
bool reach_cutoff_time = false;
bool reach_known_best_value = false;
bool_var flipvar;
init();
bool reach_cutoff_time = false;
bool reach_known_best_value = false;
bool_var flipvar;
double elapsed_time = 0;
clock_t start = clock(), stop; // TBD, use stopwatch facility
srand(0); // TBD, use random facility and parameters to set random seed.
set_parameters();
// ################## start ######################
//cout << "Start initialize and local search, restart in every " << max_steps << " steps" << endl;
for (unsigned tries = 0; ; ++tries) {
init();
srand(0); // TBD, use random facility and parameters to set random seed.
set_parameters();
// ################## start ######################
//cout << "Start initialize and local search, restart in every " << max_steps << " steps" << endl;
for (unsigned tries = 0; ; ++tries) {
reinit();
for (int step = 1; step <= max_steps; ++step) {
// feasible
if (m_unsat_stack.empty()) {
@ -287,11 +317,11 @@ namespace sat {
reach_cutoff_time = true;
if (reach_known_best_value || reach_cutoff_time)
break;
}
if (reach_known_best_value) {
}
if (reach_known_best_value) {
std::cout << elapsed_time << "\n";
}
else
}
else
std::cout << -1 << "\n";
//print_solution();
@ -311,8 +341,8 @@ namespace sat {
// update related clauses and neighbor vars
svector<term> const& constraints = var_term[flipvar];
unsigned num_constraints = constraints.size();
for (unsigned i = 0; i < num_constraints; ++i) {
unsigned num_cs = constraints.size();
for (unsigned i = 0; i < num_cs; ++i) {
c = constraints[i].constraint_id;
if (cur_solution[flipvar] == constraints[i].sense) {
//++true_terms_count[c];
@ -427,8 +457,8 @@ namespace sat {
bool local_search::tie_breaker_sat(bool_var v, bool_var best_var) {
// most improvement on objective value
int v_imp = cur_solution[v] ? -coefficient_in_ob_constraint[v] : coefficient_in_ob_constraint[v];
int b_imp = cur_solution[best_var] ? -coefficient_in_ob_constraint[best_var] : coefficient_in_ob_constraint[best_var];
int v_imp = cur_solution[v] ? -coefficient_in_ob_constraint.get(v, 0) : coefficient_in_ob_constraint.get(v, 0);
int b_imp = cur_solution[best_var] ? -coefficient_in_ob_constraint.get(best_var, 0) : coefficient_in_ob_constraint.get(best_var, 0);
// break tie 1: max imp
// break tie 2: conf_change
// break tie 3: time_stamp
@ -458,7 +488,7 @@ namespace sat {
bool_var local_search::pick_var() {
int c, v;
bool_var best_var = null_bool_var;
bool_var best_var = num_vars()-1;
// SAT Mode
if (m_unsat_stack.empty()) {
@ -498,15 +528,15 @@ namespace sat {
void local_search::set_parameters() {
if (s_id == 0)
max_steps = num_vars;
max_steps = num_vars();
else if (s_id == 1)
max_steps = (int) (1.5 * num_vars);
max_steps = (int) (1.5 * num_vars());
else if (s_id == 1)
max_steps = 2 * num_vars;
max_steps = 2 * num_vars();
else if (s_id == 2)
max_steps = (int) (2.5 * num_vars);
max_steps = (int) (2.5 * num_vars());
else if (s_id == 3)
max_steps = 3 * num_vars;
max_steps = 3 * num_vars();
else {
std::cout << "Invalid strategy id!" << std::endl;
exit(-1);

19
src/sat/sat_local_search.h
View file

@ -42,9 +42,6 @@ namespace sat {
//int coefficient; // all constraints are cardinality: coefficient=1
};
// parameters of the instance
unsigned num_vars; // var index from 1 to num_vars
unsigned num_constraints; // constraint index from 1 to num_constraint
// objective function: maximize
svector<ob_term> ob_constraint; // the objective function *constraint*, sorted in decending order
@ -53,6 +50,11 @@ namespace sat {
// terms arrays
vector<svector<term> > var_term; // var_term[i][j] means the j'th term of var i
vector<svector<term> > constraint_term; // constraint_term[i][j] means the j'th term of constraint i
// parameters of the instance
unsigned num_vars() const { return var_term.size(); } // var index from 1 to num_vars
unsigned num_constraints() const { return constraint_term.size(); } // constraint index from 1 to num_constraint
// information about the variable
int_vector coefficient_in_ob_constraint; // initialized to be 0
@ -62,7 +64,7 @@ namespace sat {
int_vector time_stamp; // the flip time stamp
bool_vector conf_change; // whether its configure changes since its last flip
int_vector cscc; // how many times its constraint state configure changes since its last flip
vector<int_vector> var_neighbor; // all of its neighborhoods variable
vector<bool_var_vector> var_neighbor; // all of its neighborhoods variable
/* TBD: other scores */
// information about the constraints
@ -94,10 +96,12 @@ namespace sat {
// for tuning
int s_id = 0; // strategy id
void init();
void init_orig();
void init_greedy();
void reinit();
void reinit_orig();
void reinit_greedy();
void init_cur_solution();
void init_slack();
@ -124,7 +128,6 @@ namespace sat {
void add_clause(unsigned sz, literal const* c);
void add_cardinality(unsigned sz, literal const* c, unsigned k);
// swap the deleted one with the last one and pop
void sat(int c) {
@ -141,6 +144,8 @@ namespace sat {
~local_search();
void add_soft(literal l, double weight);
void add_cardinality(unsigned sz, literal const* c, unsigned k);
lbool operator()();

5
src/sat/tactic/goal2sat.cpp
View file

@ -447,14 +447,15 @@ struct goal2sat::imp {
lits[i].neg();
}
sat::bool_var v = m_solver.mk_var(true);
sat::literal lit(v, sign);
m_ext->add_at_least(v, lits, lits.size() - k.get_unsigned());
if (root) {
m_result_stack.reset();
mk_clause(sat::literal(v, sign));
mk_clause(lit);
}
else {
m_result_stack.shrink(sz - t->get_num_args());
m_result_stack.push_back(sat::literal(v, sign));
m_result_stack.push_back(lit);
}
}

130
src/test/sat_local_search.cpp
View file

@ -1,18 +1,18 @@
#include "sat_local_search.h"
#include "sat_solver.h"
static int build_instance(char *filename, sat::solver& s, sat::local_search& ls)
static bool build_instance(char const * filename, sat::solver& s, sat::local_search& local_search)
{
char line[16383];
int cur_term;
// for temperally storage
int temp[16383];
int temp_count;
std::ifstream infile(filename);
//if (infile == NULL) //linux
if (!infile)
return 0;
if (!infile) {
std::cout << "File not found " << filename << "\n";
return false;
}
infile.getline(line, 16383);
int num_vars, num_constraints;
sscanf_s(line, "%d %d", &num_vars, &num_constraints);
@ -20,44 +20,36 @@ static int build_instance(char *filename, sat::solver& s, sat::local_search& ls)
//cout << "number of constraints: " << num_constraints << endl;
// write in the objective function
temp_count = 0;
infile >> cur_term;
while (cur_term != 0) {
temp[temp_count++] = cur_term;
infile >> cur_term;
}
int ob_num_terms = temp_count;
#if 0
TBD make this compile:
ob_constraint = new ob_term[ob_num_terms + 1];
// coefficient
ob_constraint[0].coefficient = 0; // virtual var: all variables not in ob are pointed to this var
for (i = 1; i <= ob_num_terms; ++i) {
ob_constraint[i].coefficient = temp[i - 1];
}
unsigned_vector coefficients;
sat::literal_vector lits;
// ob variable
temp_count = 0;
// process objective function:
// read coefficents
infile >> cur_term;
while (cur_term != 0) {
temp[temp_count++] = cur_term;
coefficients.push_back(cur_term);
infile >> cur_term;
}
if (temp_count != ob_num_terms) {
cout << "Objective function format error." << endl;
exit(-1);
// read variables
infile >> cur_term;
while (cur_term != 0) {
lits.push_back(sat::literal(abs(cur_term), cur_term < 0));
infile >> cur_term;
}
for (i = 1; i <= ob_num_terms; ++i) {
ob_constraint[i].var_id = temp[i - 1];
coefficient_in_ob_constraint[ob_constraint[i].var_id] = ob_constraint[i].coefficient;
if (lits.size() != coefficients.size()) {
std::cout << "Objective function format error. They have different lenghts.\n";
return false;
}
for (unsigned i = 0; i < lits.size(); ++i) {
local_search.add_soft(lits[i], coefficients[i]);
}
// read the constraints, one at a time
card_extension* ext = 0;
int k;
for (c = 1; c <= num_constraints; ++c) {
for (int c = 1; c <= num_constraints; ++c) {
lits.reset();
infile >> cur_term;
while (cur_term != 0) {
@ -65,63 +57,11 @@ static int build_instance(char *filename, sat::solver& s, sat::local_search& ls)
infile >> cur_term;
}
infile >> k;
ext->add_at_least(null_bool_var, lits, lits.size() - k);
local_search.add_cardinality(lits.size(), lits.c_ptr(), static_cast<unsigned>(lits.size() - k));
}
#endif
infile.close();
#if 0
Move all of this to initialization code for local search solver:
// create var_term array
for (v = 1; v <= num_vars; ++v) {
var_term[v] = new term[var_term_count[v]];
var_term_count[v] = 0; // reset to 0, for building up the array
}
// scan all constraints to build up var term arrays
for (c = 1; c <= num_constraints; ++c) {
for (i = 0; i < constraint_term_count[c]; ++i) {
v = constraint_term[c][i].var_id;
var_term[v][var_term_count[v]++] = constraint_term[c][i];
}
}
// build neighborhood relationship
bool *is_neighbor;
is_neighbor = new bool[num_vars + 1];
for (v = 1; v <= num_vars; ++v) {
// init as not neighbor
for (i = 1; i <= num_vars; ++i) {
is_neighbor[i] = false;
}
temp_count = 0;
// for each constraint v appears
for (i = 0; i < var_term_count[v]; ++i) {
c = var_term[v][i].constraint_id;
for (j = 0; j < constraint_term_count[c]; ++j) {
if (constraint_term[c][j].var_id == v)
continue;
// not neighbor yet
if (!is_neighbor[constraint_term[c][j].var_id]) {
is_neighbor[constraint_term[c][j].var_id] = true;
temp[temp_count++] = constraint_term[c][j].var_id;
}
}
}
// create and build neighbor
var_neighbor_count[v] = temp_count;
var_neighbor[v] = new int[var_neighbor_count[v]];
for (i = 0; i < var_neighbor_count[v]; ++i) {
var_neighbor[v][i] = temp[i];
}
}
delete[] is_neighbor;
#endif
return 1;
return true;
}
void tst_sat_local_search(char ** argv, int argc, int& i) {
@ -129,6 +69,20 @@ void tst_sat_local_search(char ** argv, int argc, int& i) {
std::cout << "require dimacs file name\n";
return;
}
reslimit limit;
params_ref params;
sat::solver solver(params, limit);
sat::local_search local_search(solver);
char const* file_name = argv[i + 1];
++i;
if (!build_instance(file_name, solver, local_search)) {
return;
}
std::cout << "local instance built\n";
local_search();
// sat::solver s;
// populate the sat solver with clauses and cardinality consrtaints from the input
// call the lookahead solver.