Re: [Fwd: Enabling MiniSat for 64 bit?]
Chris Matrakidis <[email protected]>
| Newsgroups | gmane.comp.gnu.glpk |
|---|---|
| Message-ID | <CAEaJ3S5S9v2bjh12dVceveU-FhzTR_ba-nuzVd3h=XB2tQzqzg@mail.gmail.com> |
Hi Andrew, > Could you please post me the entire files (not diff's)? Here they are. Best Regards, Chris Matrakidis _______________________________________________ Help-glpk mailing list [email protected] https://lists.gnu.org/mailman/listinfo/help-glpk
minisat1.c
(text/x-csrc, 4.8 KB)
/* minisat1.c (driver to MiniSat solver) */ /*********************************************************************** * This code is part of GLPK (GNU Linear Programming Kit). * * Copyright (C) 2011-2016 Andrew Makhorin, Department for Applied * Informatics, Moscow Aviation Institute, Moscow, Russia. All rights * reserved. E-mail: <[email protected]>. * * GLPK is free software: you can redistribute it and/or modify it * under the terms of the GNU General Public License as published by * the Free Software Foundation, either version 3 of the License, or * (at your option) any later version. * * GLPK is distributed in the hope that it will be useful, but WITHOUT * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY * or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public * License for more details. * * You should have received a copy of the GNU General Public License * along with GLPK. If not, see <http://www.gnu.org/licenses/>. ***********************************************************************/ #include "env.h" #include "minisat.h" #include "prob.h" int glp_minisat1(glp_prob *P) { /* solve CNF-SAT problem with MiniSat solver */ solver *s; GLPAIJ *aij; int i, j, len, ret, *ind; double sum; #if 0 /* 04/IV-2016 */ /* check problem object */ if (P == NULL || P->magic != GLP_PROB_MAGIC) xerror("glp_minisat1: P = %p; invalid problem object\n", P); #endif if (P->tree != NULL) xerror("glp_minisat1: operation not allowed\n"); /* integer solution is currently undefined */ P->mip_stat = GLP_UNDEF; P->mip_obj = 0.0; /* check that problem object encodes CNF-SAT instance */ if (glp_check_cnfsat(P) != 0) { xprintf("glp_minisat1: problem object does not encode CNF-SAT " "instance\n"); ret = GLP_EDATA; goto done; } #if 1 /* 07/XI-2015 */ if (sizeof(void *) != sizeof(size_t)) { xprintf("glp_minisat1: sorry, MiniSat solver is not supported " "on this platform\n"); ret = GLP_EFAIL; goto done; } #endif /* solve CNF-SAT problem */ xprintf("Solving CNF-SAT problem...\n"); xprintf("Instance has %d variable%s, %d clause%s, and %d literal%" "s\n", P->n, P->n == 1 ? "" : "s", P->m, P->m == 1 ? "" : "s", P->nnz, P->nnz == 1 ? "" : "s"); /* if CNF-SAT has no clauses, it is satisfiable */ if (P->m == 0) { P->mip_stat = GLP_OPT; for (j = 1; j <= P->n; j++) P->col[j]->mipx = 0.0; goto fini; } /* if CNF-SAT has an empty clause, it is unsatisfiable */ for (i = 1; i <= P->m; i++) { if (P->row[i]->ptr == NULL) { P->mip_stat = GLP_NOFEAS; goto fini; } } /* prepare input data for the solver */ s = solver_new(); solver_setnvars(s, P->n); ind = xcalloc(1+P->n, sizeof(int)); for (i = 1; i <= P->m; i++) { len = 0; for (aij = P->row[i]->ptr; aij != NULL; aij = aij->r_next) { ind[++len] = toLit(aij->col->j-1); if (aij->val < 0.0) ind[len] = lit_neg(ind[len]); } xassert(len > 0); if (!solver_addclause(s, &ind[1], &ind[1+len])) { /* found trivial conflict */ xfree(ind); solver_delete(s); P->mip_stat = GLP_NOFEAS; goto fini; } } xfree(ind); /* call the solver */ s->verbosity = 1; if (solver_solve(s, 0, 0)) { /* instance is reported as satisfiable */ P->mip_stat = GLP_OPT; /* copy solution to the problem object */ xassert(s->model.size == P->n); for (j = 1; j <= P->n; j++) { P->col[j]->mipx = s->model.ptr[j-1] == l_True ? 1.0 : 0.0; } /* compute row values */ for (i = 1; i <= P->m; i++) { sum = 0; for (aij = P->row[i]->ptr; aij != NULL; aij = aij->r_next) sum += aij->val * aij->col->mipx; P->row[i]->mipx = sum; } /* check integer feasibility */ for (i = 1; i <= P->m; i++) { if (P->row[i]->mipx < P->row[i]->lb) { /* solution is wrong */ P->mip_stat = GLP_UNDEF; break; } } } else { /* instance is reported as unsatisfiable */ P->mip_stat = GLP_NOFEAS; } solver_delete(s); fini: /* report the instance status */ if (P->mip_stat == GLP_OPT) { xprintf("SATISFIABLE\n"); ret = 0; } else if (P->mip_stat == GLP_NOFEAS) { xprintf("UNSATISFIABLE\n"); ret = 0; } else { xprintf("glp_minisat1: solver failed\n"); ret = GLP_EFAIL; } done: return ret; } /* eof */
intfeas1.c
(text/x-csrc, 9.6 KB)
/* intfeas1.c (solve integer feasibility problem) */ /*********************************************************************** * This code is part of GLPK (GNU Linear Programming Kit). * * Copyright (C) 2011-2016 Andrew Makhorin, Department for Applied * Informatics, Moscow Aviation Institute, Moscow, Russia. All rights * reserved. E-mail: <[email protected]>. * * GLPK is free software: you can redistribute it and/or modify it * under the terms of the GNU General Public License as published by * the Free Software Foundation, either version 3 of the License, or * (at your option) any later version. * * GLPK is distributed in the hope that it will be useful, but WITHOUT * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY * or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public * License for more details. * * You should have received a copy of the GNU General Public License * along with GLPK. If not, see <http://www.gnu.org/licenses/>. ***********************************************************************/ #include "env.h" #include "glpnpp.h" int glp_intfeas1(glp_prob *P, int use_bound, int obj_bound) { /* solve integer feasibility problem */ NPP *npp = NULL; glp_prob *mip = NULL; int *obj_ind = NULL; double *obj_val = NULL; int obj_row = 0; int i, j, k, obj_len, temp, ret; #if 0 /* 04/IV-2016 */ /* check the problem object */ if (P == NULL || P->magic != GLP_PROB_MAGIC) xerror("glp_intfeas1: P = %p; invalid problem object\n", P); #endif if (P->tree != NULL) xerror("glp_intfeas1: operation not allowed\n"); /* integer solution is currently undefined */ P->mip_stat = GLP_UNDEF; P->mip_obj = 0.0; /* check columns (variables) */ for (j = 1; j <= P->n; j++) { GLPCOL *col = P->col[j]; #if 0 /* binarization is not yet implemented */ if (!(col->kind == GLP_IV || col->type == GLP_FX)) { xprintf("glp_intfeas1: column %d: non-integer non-fixed var" "iable not allowed\n", j); #else if (!((col->kind == GLP_IV && col->lb == 0.0 && col->ub == 1.0) || col->type == GLP_FX)) { xprintf("glp_intfeas1: column %d: non-binary non-fixed vari" "able not allowed\n", j); #endif ret = GLP_EDATA; goto done; } temp = (int)col->lb; if ((double)temp != col->lb) { if (col->type == GLP_FX) xprintf("glp_intfeas1: column %d: fixed value %g is non-" "integer or out of range\n", j, col->lb); else xprintf("glp_intfeas1: column %d: lower bound %g is non-" "integer or out of range\n", j, col->lb); ret = GLP_EDATA; goto done; } temp = (int)col->ub; if ((double)temp != col->ub) { xprintf("glp_intfeas1: column %d: upper bound %g is non-int" "eger or out of range\n", j, col->ub); ret = GLP_EDATA; goto done; } if (col->type == GLP_DB && col->lb > col->ub) { xprintf("glp_intfeas1: column %d: lower bound %g is greater" " than upper bound %g\n", j, col->lb, col->ub); ret = GLP_EBOUND; goto done; } } /* check rows (constraints) */ for (i = 1; i <= P->m; i++) { GLPROW *row = P->row[i]; GLPAIJ *aij; for (aij = row->ptr; aij != NULL; aij = aij->r_next) { temp = (int)aij->val; if ((double)temp != aij->val) { xprintf("glp_intfeas1: row = %d, column %d: constraint c" "oefficient %g is non-integer or out of range\n", i, aij->col->j, aij->val); ret = GLP_EDATA; goto done; } } temp = (int)row->lb; if ((double)temp != row->lb) { if (row->type == GLP_FX) xprintf("glp_intfeas1: row = %d: fixed value %g is non-i" "nteger or out of range\n", i, row->lb); else xprintf("glp_intfeas1: row = %d: lower bound %g is non-i" "nteger or out of range\n", i, row->lb); ret = GLP_EDATA; goto done; } temp = (int)row->ub; if ((double)temp != row->ub) { xprintf("glp_intfeas1: row = %d: upper bound %g is non-inte" "ger or out of range\n", i, row->ub); ret = GLP_EDATA; goto done; } if (row->type == GLP_DB && row->lb > row->ub) { xprintf("glp_intfeas1: row %d: lower bound %g is greater th" "an upper bound %g\n", i, row->lb, row->ub); ret = GLP_EBOUND; goto done; } } /* check the objective function if a bound is requested */ if (use_bound) { temp = (int)P->c0; if ((double)temp != P->c0) { xprintf("glp_intfeas1: objective constant term %g is non-integ" "er or out of range\n", P->c0); ret = GLP_EDATA; goto done; } for (j = 1; j <= P->n; j++) { temp = (int)P->col[j]->coef; if ((double)temp != P->col[j]->coef) { xprintf("glp_intfeas1: column %d: objective coefficient is " "non-integer or out of range\n", j, P->col[j]->coef); ret = GLP_EDATA; goto done; } } } /* save the objective function and set it to zero */ obj_ind = xcalloc(1+P->n, sizeof(int)); obj_val = xcalloc(1+P->n, sizeof(double)); obj_len = 0; obj_ind[0] = 0; obj_val[0] = P->c0; P->c0 = 0.0; for (j = 1; j <= P->n; j++) { if (P->col[j]->coef != 0.0) { obj_len++; obj_ind[obj_len] = j; obj_val[obj_len] = P->col[j]->coef; P->col[j]->coef = 0.0; } } /* add inequality to bound the objective function, if required */ if (!use_bound) xprintf("Will search for ANY feasible solution\n"); else { xprintf("Will search only for solution not worse than %d\n", obj_bound); obj_row = glp_add_rows(P, 1); glp_set_mat_row(P, obj_row, obj_len, obj_ind, obj_val); if (P->dir == GLP_MIN) glp_set_row_bnds(P, obj_row, GLP_UP, 0.0, (double)obj_bound - obj_val[0]); else if (P->dir == GLP_MAX) glp_set_row_bnds(P, obj_row, GLP_LO, (double)obj_bound - obj_val[0], 0.0); else xassert(P != P); } /* create preprocessor workspace */ xprintf("Translating to CNF-SAT...\n"); xprintf("Original problem has %d row%s, %d column%s, and %d non-z" "ero%s\n", P->m, P->m == 1 ? "" : "s", P->n, P->n == 1 ? "" : "s", P->nnz, P->nnz == 1 ? "" : "s"); npp = npp_create_wksp(); /* load the original problem into the preprocessor workspace */ npp_load_prob(npp, P, GLP_OFF, GLP_MIP, GLP_OFF); /* perform translation to SAT-CNF problem instance */ ret = npp_sat_encode_prob(npp); if (ret == 0) ; else if (ret == GLP_ENOPFS) xprintf("PROBLEM HAS NO INTEGER FEASIBLE SOLUTION\n"); else if (ret == GLP_ERANGE) xprintf("glp_intfeas1: translation to SAT-CNF failed because o" "f integer overflow\n"); else xassert(ret != ret); if (ret != 0) goto done; /* build SAT-CNF problem instance and try to solve it */ mip = glp_create_prob(); npp_build_prob(npp, mip); ret = glp_minisat1(mip); /* only integer feasible solution can be postprocessed */ if (!(mip->mip_stat == GLP_OPT || mip->mip_stat == GLP_FEAS)) { P->mip_stat = mip->mip_stat; goto done; } /* postprocess the solution found */ npp_postprocess(npp, mip); /* the transformed problem is no longer needed */ glp_delete_prob(mip), mip = NULL; /* store solution to the original problem object */ npp_unload_sol(npp, P); /* change the solution status to 'integer feasible' */ P->mip_stat = GLP_FEAS; /* check integer feasibility */ for (i = 1; i <= P->m; i++) { GLPROW *row; GLPAIJ *aij; double sum; row = P->row[i]; sum = 0.0; for (aij = row->ptr; aij != NULL; aij = aij->r_next) sum += aij->val * aij->col->mipx; xassert(sum == row->mipx); if (row->type == GLP_LO || row->type == GLP_DB || row->type == GLP_FX) xassert(sum >= row->lb); if (row->type == GLP_UP || row->type == GLP_DB || row->type == GLP_FX) xassert(sum <= row->ub); } /* compute value of the original objective function */ P->mip_obj = obj_val[0]; for (k = 1; k <= obj_len; k++) P->mip_obj += obj_val[k] * P->col[obj_ind[k]]->mipx; xprintf("Objective value = %17.9e\n", P->mip_obj); done: /* delete the transformed problem, if it exists */ if (mip != NULL) glp_delete_prob(mip); /* delete the preprocessor workspace, if it exists */ if (npp != NULL) npp_delete_wksp(npp); /* remove inequality used to bound the objective function */ if (obj_row > 0) { int ind[1+1]; ind[1] = obj_row; glp_del_rows(P, 1, ind); } /* restore the original objective function */ if (obj_ind != NULL) { P->c0 = obj_val[0]; for (k = 1; k <= obj_len; k++) P->col[obj_ind[k]]->coef = obj_val[k]; xfree(obj_ind); xfree(obj_val); } return ret; } /* eof */
minisat.c
(text/x-csrc, 37.1 KB)
/* minisat.c */ /* Modified by Andrew Makhorin <[email protected]>, August 2011 */ /*********************************************************************** * MiniSat -- Copyright (c) 2005, Niklas Sorensson * http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ * * Permission is hereby granted, free of charge, to any person * obtaining a copy of this software and associated documentation files * (the "Software"), to deal in the Software without restriction, * including without limitation the rights to use, copy, modify, merge, * publish, distribute, sublicense, and/or sell copies of the Software, * and to permit persons to whom the Software is furnished to do so, * subject to the following conditions: * * The above copyright notice and this permission notice shall be * included in all copies or substantial portions of the Software. * * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE * SOFTWARE. ***********************************************************************/ /* Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko */ #include "env.h" #include "minisat.h" #if 1 /* by mao */ static void *ymalloc(int size) { void *ptr; xassert(size > 0); ptr = malloc(size); if (ptr == NULL) xerror("MiniSat: no memory available\n"); return ptr; } static void *yrealloc(void *ptr, int size) { xassert(size > 0); if (ptr == NULL) ptr = malloc(size); else ptr = realloc(ptr, size); if (ptr == NULL) xerror("MiniSat: no memory available\n"); return ptr; } static void yfree(void *ptr) { xassert(ptr != NULL); free(ptr); return; } #define assert xassert #define printf xprintf #define fflush(f) /* nop */ #define malloc ymalloc #define realloc yrealloc #define free yfree #define inline /* empty */ #endif /*====================================================================*/ /* Debug: */ #if 0 #define VERBOSEDEBUG 1 #endif /* For derivation output (verbosity level 2) */ #define L_IND "%-*d" #define L_ind solver_dlevel(s)*3+3,solver_dlevel(s) #define L_LIT "%sx%d" #define L_lit(p) lit_sign(p)?"~":"", (lit_var(p)) #if 0 /* by mao */ /* Just like 'assert()' but expression will be evaluated in the release version as well. */ static inline void check(int expr) { assert(expr); } #endif #if 0 /* by mao */ static void printlits(lit* begin, lit* end) { int i; for (i = 0; i < end - begin; i++) printf(L_LIT" ",L_lit(begin[i])); } #endif /*====================================================================*/ /* Random numbers: */ /* Returns a random float 0 <= x < 1. Seed must never be 0. */ static inline double drand(double* seed) { int q; *seed *= 1389796; q = (int)(*seed / 2147483647); *seed -= (double)q * 2147483647; return *seed / 2147483647; } /* Returns a random integer 0 <= x < size. Seed must never be 0. */ static inline int irand(double* seed, int size) { return (int)(drand(seed) * size); } /*====================================================================*/ /* Predeclarations: */ static void sort(void** array, int size, int(*comp)(const void *, const void *)); /*====================================================================*/ /* Clause datatype + minor functions: */ #if 0 /* by mao; see minisat.h */ struct clause_t { int size_learnt; lit lits[0]; }; #endif #define clause_size(c) ((c)->size_learnt >> 1) #define clause_begin(c) ((c)->lits) #define clause_learnt(c) ((c)->size_learnt & 1) #define clause_activity(c) \ (*((float*)&(c)->lits[(c)->size_learnt>>1])) #define clause_setactivity(c, a) \ (void)(*((float*)&(c)->lits[(c)->size_learnt>>1]) = (a)) /*====================================================================*/ /* Encode literals in clause pointers: */ #define clause_from_lit(l) \ (clause*)((size_t)(l) + (size_t)(l) + 1) #define clause_is_lit(c) \ ((size_t)(c) & 1) #define clause_read_lit(c) \ (lit)((size_t)(c) >> 1) /*====================================================================*/ /* Simple helpers: */ #define solver_dlevel(s) \ (int)veci_size(&(s)->trail_lim) #define solver_read_wlist(s, l) \ (vecp *)(&(s)->wlists[l]) static inline void vecp_remove(vecp* v, void* e) { void** ws = vecp_begin(v); int j = 0; for (; ws[j] != e ; j++); assert(j < vecp_size(v)); for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1]; vecp_resize(v,vecp_size(v)-1); } /*====================================================================*/ /* Variable order functions: */ static inline void order_update(solver* s, int v) { /* updateorder */ int* orderpos = s->orderpos; double* activity = s->activity; int* heap = veci_begin(&s->order); int i = orderpos[v]; int x = heap[i]; int parent = (i - 1) / 2; assert(s->orderpos[v] != -1); while (i != 0 && activity[x] > activity[heap[parent]]){ heap[i] = heap[parent]; orderpos[heap[i]] = i; i = parent; parent = (i - 1) / 2; } heap[i] = x; orderpos[x] = i; } #define order_assigned(s, v) /* nop */ static inline void order_unassigned(solver* s, int v) { /* undoorder */ int* orderpos = s->orderpos; if (orderpos[v] == -1){ orderpos[v] = veci_size(&s->order); veci_push(&s->order,v); order_update(s,v); } } static int order_select(solver* s, float random_var_freq) { /* selectvar */ int* heap; double* activity; int* orderpos; lbool* values = s->assigns; /* Random decision: */ if (drand(&s->random_seed) < random_var_freq){ int next = irand(&s->random_seed,s->size); assert(next >= 0 && next < s->size); if (values[next] == l_Undef) return next; } /* Activity based decision: */ heap = veci_begin(&s->order); activity = s->activity; orderpos = s->orderpos; while (veci_size(&s->order) > 0){ int next = heap[0]; int size = veci_size(&s->order)-1; int x = heap[size]; veci_resize(&s->order,size); orderpos[next] = -1; if (size > 0){ double act = activity[x]; int i = 0; int child = 1; while (child < size){ if (child+1 < size && activity[heap[child]] < activity[heap[child+1]]) child++; assert(child < size); if (act >= activity[heap[child]]) break; heap[i] = heap[child]; orderpos[heap[i]] = i; i = child; child = 2 * child + 1; } heap[i] = x; orderpos[heap[i]] = i; } if (values[next] == l_Undef) return next; } return var_Undef; } /*====================================================================*/ /* Activity functions: */ static inline void act_var_rescale(solver* s) { double* activity = s->activity; int i; for (i = 0; i < s->size; i++) activity[i] *= 1e-100; s->var_inc *= 1e-100; } static inline void act_var_bump(solver* s, int v) { double* activity = s->activity; if ((activity[v] += s->var_inc) > 1e100) act_var_rescale(s); /* printf("bump %d %f\n", v-1, activity[v]); */ if (s->orderpos[v] != -1) order_update(s,v); } static inline void act_var_decay(solver* s) { s->var_inc *= s->var_decay; } static inline void act_clause_rescale(solver* s) { clause** cs = (clause**)vecp_begin(&s->learnts); int i; for (i = 0; i < vecp_size(&s->learnts); i++){ float a = clause_activity(cs[i]); clause_setactivity(cs[i], a * (float)1e-20); } s->cla_inc *= (float)1e-20; } static inline void act_clause_bump(solver* s, clause *c) { float a = clause_activity(c) + s->cla_inc; clause_setactivity(c,a); if (a > 1e20) act_clause_rescale(s); } static inline void act_clause_decay(solver* s) { s->cla_inc *= s->cla_decay; } /*====================================================================*/ /* Clause functions: */ /* pre: size > 1 && no variable occurs twice */ static clause* clause_new(solver* s, lit* begin, lit* end, int learnt) { int size; clause* c; int i; assert(end - begin > 1); assert(learnt >= 0 && learnt < 2); size = end - begin; c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); c->size_learnt = (size << 1) | learnt; #if 1 /* by mao & cmatraki; non-portable check that is a fundamental * assumption of minisat code: bit 0 is used as a flag (zero * for pointer, one for shifted int) so allocated memory should * be at least 16-bit aligned */ assert(((size_t)c & 1) == 0); #endif for (i = 0; i < size; i++) c->lits[i] = begin[i]; if (learnt) *((float*)&c->lits[size]) = 0.0; assert(begin[0] >= 0); assert(begin[0] < s->size*2); assert(begin[1] >= 0); assert(begin[1] < s->size*2); assert(lit_neg(begin[0]) < s->size*2); assert(lit_neg(begin[1]) < s->size*2); /* vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)c); */ /* vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)c); */ vecp_push(solver_read_wlist(s,lit_neg(begin[0])), (void*)(size > 2 ? c : clause_from_lit(begin[1]))); vecp_push(solver_read_wlist(s,lit_neg(begin[1])), (void*)(size > 2 ? c : clause_from_lit(begin[0]))); return c; } static void clause_remove(solver* s, clause* c) { lit* lits = clause_begin(c); assert(lit_neg(lits[0]) < s->size*2); assert(lit_neg(lits[1]) < s->size*2); /* vecp_remove(solver_read_wlist(s,lit_neg(lits[0])),(void*)c); */ /* vecp_remove(solver_read_wlist(s,lit_neg(lits[1])),(void*)c); */ assert(lits[0] < s->size*2); vecp_remove(solver_read_wlist(s,lit_neg(lits[0])), (void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1]))); vecp_remove(solver_read_wlist(s,lit_neg(lits[1])), (void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0]))); if (clause_learnt(c)){ s->stats.learnts--; s->stats.learnts_literals -= clause_size(c); }else{ s->stats.clauses--; s->stats.clauses_literals -= clause_size(c); } free(c); } static lbool clause_simplify(solver* s, clause* c) { lit* lits = clause_begin(c); lbool* values = s->assigns; int i; assert(solver_dlevel(s) == 0); for (i = 0; i < clause_size(c); i++){ lbool sig = !lit_sign(lits[i]); sig += sig - 1; if (values[lit_var(lits[i])] == sig) return l_True; } return l_False; } /*====================================================================*/ /* Minor (solver) functions: */ void solver_setnvars(solver* s,int n) { int var; if (s->cap < n){ while (s->cap < n) s->cap = s->cap*2+1; s->wlists = (vecp*) realloc(s->wlists, sizeof(vecp)*s->cap*2); s->activity = (double*) realloc(s->activity, sizeof(double)*s->cap); s->assigns = (lbool*) realloc(s->assigns, sizeof(lbool)*s->cap); s->orderpos = (int*) realloc(s->orderpos, sizeof(int)*s->cap); s->reasons = (clause**)realloc(s->reasons, sizeof(clause*)*s->cap); s->levels = (int*) realloc(s->levels, sizeof(int)*s->cap); s->tags = (lbool*) realloc(s->tags, sizeof(lbool)*s->cap); s->trail = (lit*) realloc(s->trail, sizeof(lit)*s->cap); } for (var = s->size; var < n; var++){ vecp_new(&s->wlists[2*var]); vecp_new(&s->wlists[2*var+1]); s->activity [var] = 0; s->assigns [var] = l_Undef; s->orderpos [var] = veci_size(&s->order); s->reasons [var] = (clause*)0; s->levels [var] = 0; s->tags [var] = l_Undef; /* does not hold because variables enqueued at top level will not be reinserted in the heap assert(veci_size(&s->order) == var); */ veci_push(&s->order,var); order_update(s, var); } s->size = n > s->size ? n : s->size; } static inline bool enqueue(solver* s, lit l, clause* from) { lbool* values = s->assigns; int v = lit_var(l); lbool val = values[v]; lbool sig; #ifdef VERBOSEDEBUG printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l)); #endif /* lbool */ sig = !lit_sign(l); sig += sig - 1; if (val != l_Undef){ return val == sig; }else{ /* New fact -- store it. */ int* levels; clause** reasons; #ifdef VERBOSEDEBUG printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l)); #endif /* int* */ levels = s->levels; /* clause** */ reasons = s->reasons; values [v] = sig; levels [v] = solver_dlevel(s); reasons[v] = from; s->trail[s->qtail++] = l; order_assigned(s, v); return true; } } static inline void assume(solver* s, lit l){ assert(s->qtail == s->qhead); assert(s->assigns[lit_var(l)] == l_Undef); #ifdef VERBOSEDEBUG printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l)); #endif veci_push(&s->trail_lim,s->qtail); enqueue(s,l,(clause*)0); } static inline void solver_canceluntil(solver* s, int level) { lit* trail; lbool* values; clause** reasons; int bound; int c; if (solver_dlevel(s) <= level) return; trail = s->trail; values = s->assigns; reasons = s->reasons; bound = (veci_begin(&s->trail_lim))[level]; for (c = s->qtail-1; c >= bound; c--) { int x = lit_var(trail[c]); values [x] = l_Undef; reasons[x] = (clause*)0; } for (c = s->qhead-1; c >= bound; c--) order_unassigned(s,lit_var(trail[c])); s->qhead = s->qtail = bound; veci_resize(&s->trail_lim,level); } static void solver_record(solver* s, veci* cls) { lit* begin = veci_begin(cls); lit* end = begin + veci_size(cls); clause* c = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0; enqueue(s,*begin,c); assert(veci_size(cls) > 0); if (c != 0) { vecp_push(&s->learnts,c); act_clause_bump(s,c); s->stats.learnts++; s->stats.learnts_literals += veci_size(cls); } } static double solver_progress(solver* s) { lbool* values = s->assigns; int* levels = s->levels; int i; double progress = 0; double F = 1.0 / s->size; for (i = 0; i < s->size; i++) if (values[i] != l_Undef) progress += pow(F, levels[i]); return progress / s->size; } /*====================================================================*/ /* Major methods: */ static bool solver_lit_removable(solver* s, lit l, int minl) { lbool* tags = s->tags; clause** reasons = s->reasons; int* levels = s->levels; int top = veci_size(&s->tagged); assert(lit_var(l) >= 0 && lit_var(l) < s->size); assert(reasons[lit_var(l)] != 0); veci_resize(&s->stack,0); veci_push(&s->stack,lit_var(l)); while (veci_size(&s->stack) > 0){ clause* c; int v = veci_begin(&s->stack)[veci_size(&s->stack)-1]; assert(v >= 0 && v < s->size); veci_resize(&s->stack,veci_size(&s->stack)-1); assert(reasons[v] != 0); c = reasons[v]; if (clause_is_lit(c)){ int v = lit_var(clause_read_lit(c)); if (tags[v] == l_Undef && levels[v] != 0){ if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ veci_push(&s->stack,v); tags[v] = l_True; veci_push(&s->tagged,v); }else{ int* tagged = veci_begin(&s->tagged); int j; for (j = top; j < veci_size(&s->tagged); j++) tags[tagged[j]] = l_Undef; veci_resize(&s->tagged,top); return false; } } }else{ lit* lits = clause_begin(c); int i, j; for (i = 1; i < clause_size(c); i++){ int v = lit_var(lits[i]); if (tags[v] == l_Undef && levels[v] != 0){ if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ veci_push(&s->stack,lit_var(lits[i])); tags[v] = l_True; veci_push(&s->tagged,v); }else{ int* tagged = veci_begin(&s->tagged); for (j = top; j < veci_size(&s->tagged); j++) tags[tagged[j]] = l_Undef; veci_resize(&s->tagged,top); return false; } } } } } return true; } static void solver_analyze(solver* s, clause* c, veci* learnt) { lit* trail = s->trail; lbool* tags = s->tags; clause** reasons = s->reasons; int* levels = s->levels; int cnt = 0; lit p = lit_Undef; int ind = s->qtail-1; lit* lits; int i, j, minl; int* tagged; veci_push(learnt,lit_Undef); do{ assert(c != 0); if (clause_is_lit(c)){ lit q = clause_read_lit(c); assert(lit_var(q) >= 0 && lit_var(q) < s->size); if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){ tags[lit_var(q)] = l_True; veci_push(&s->tagged,lit_var(q)); act_var_bump(s,lit_var(q)); if (levels[lit_var(q)] == solver_dlevel(s)) cnt++; else veci_push(learnt,q); } }else{ if (clause_learnt(c)) act_clause_bump(s,c); lits = clause_begin(c); /* printlits(lits,lits+clause_size(c)); printf("\n"); */ for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){ lit q = lits[j]; assert(lit_var(q) >= 0 && lit_var(q) < s->size); if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){ tags[lit_var(q)] = l_True; veci_push(&s->tagged,lit_var(q)); act_var_bump(s,lit_var(q)); if (levels[lit_var(q)] == solver_dlevel(s)) cnt++; else veci_push(learnt,q); } } } while (tags[lit_var(trail[ind--])] == l_Undef); p = trail[ind+1]; c = reasons[lit_var(p)]; cnt--; }while (cnt > 0); *veci_begin(learnt) = lit_neg(p); lits = veci_begin(learnt); minl = 0; for (i = 1; i < veci_size(learnt); i++){ int lev = levels[lit_var(lits[i])]; minl |= 1 << (lev & 31); } /* simplify (full) */ for (i = j = 1; i < veci_size(learnt); i++){ if (reasons[lit_var(lits[i])] == 0 || !solver_lit_removable(s,lits[i],minl)) lits[j++] = lits[i]; } /* update size of learnt + statistics */ s->stats.max_literals += veci_size(learnt); veci_resize(learnt,j); s->stats.tot_literals += j; /* clear tags */ tagged = veci_begin(&s->tagged); for (i = 0; i < veci_size(&s->tagged); i++) tags[tagged[i]] = l_Undef; veci_resize(&s->tagged,0); #ifdef DEBUG for (i = 0; i < s->size; i++) assert(tags[i] == l_Undef); #endif #ifdef VERBOSEDEBUG printf(L_IND"Learnt {", L_ind); for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i])); #endif if (veci_size(learnt) > 1){ int max_i = 1; int max = levels[lit_var(lits[1])]; lit tmp; for (i = 2; i < veci_size(learnt); i++) if (levels[lit_var(lits[i])] > max){ max = levels[lit_var(lits[i])]; max_i = i; } tmp = lits[1]; lits[1] = lits[max_i]; lits[max_i] = tmp; } #ifdef VERBOSEDEBUG { int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0; printf(" } at level %d\n", lev); } #endif } clause* solver_propagate(solver* s) { lbool* values = s->assigns; clause* confl = (clause*)0; lit* lits; /* printf("solver_propagate\n"); */ while (confl == 0 && s->qtail - s->qhead > 0){ lit p = s->trail[s->qhead++]; vecp* ws = solver_read_wlist(s,p); clause **begin = (clause**)vecp_begin(ws); clause **end = begin + vecp_size(ws); clause **i, **j; s->stats.propagations++; s->simpdb_props--; /* printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p)); */ for (i = j = begin; i < end; ){ if (clause_is_lit(*i)){ *j++ = *i; if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){ confl = s->binary; (clause_begin(confl))[1] = lit_neg(p); (clause_begin(confl))[0] = clause_read_lit(*i++); /* Copy the remaining watches: */ while (i < end) *j++ = *i++; } }else{ lit false_lit; lbool sig; lits = clause_begin(*i); /* Make sure the false literal is data[1]: */ false_lit = lit_neg(p); if (lits[0] == false_lit){ lits[0] = lits[1]; lits[1] = false_lit; } assert(lits[1] == false_lit); /* printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n"); */ /* If 0th watch is true, then clause is already satisfied. */ sig = !lit_sign(lits[0]); sig += sig - 1; if (values[lit_var(lits[0])] == sig){ *j++ = *i; }else{ /* Look for new watch: */ lit* stop = lits + clause_size(*i); lit* k; for (k = lits + 2; k < stop; k++){ lbool sig = lit_sign(*k); sig += sig - 1; if (values[lit_var(*k)] != sig){ lits[1] = *k; *k = false_lit; vecp_push(solver_read_wlist(s, lit_neg(lits[1])),*i); goto next; } } *j++ = *i; /* Clause is unit under assignment: */ if (!enqueue(s,lits[0], *i)){ confl = *i++; /* Copy the remaining watches: */ while (i < end) *j++ = *i++; } } } next: i++; } s->stats.inspects += j - (clause**)vecp_begin(ws); vecp_resize(ws,j - (clause**)vecp_begin(ws)); } return confl; } static inline int clause_cmp (const void* x, const void* y) { return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; } void solver_reducedb(solver* s) { int i, j; double extra_lim = s->cla_inc / vecp_size(&s->learnts); /* Remove any clause below this activity */ clause** learnts = (clause**)vecp_begin(&s->learnts); clause** reasons = s->reasons; sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), clause_cmp); for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){ if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i]) clause_remove(s,learnts[i]); else learnts[j++] = learnts[i]; } for (; i < vecp_size(&s->learnts); i++){ if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim) clause_remove(s,learnts[i]); else learnts[j++] = learnts[i]; } /* printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j); */ vecp_resize(&s->learnts,j); } static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) { int* levels = s->levels; double var_decay = 0.95; double clause_decay = 0.999; double random_var_freq = 0.02; int conflictC = 0; veci learnt_clause; assert(s->root_level == solver_dlevel(s)); s->stats.starts++; s->var_decay = (float)(1 / var_decay ); s->cla_decay = (float)(1 / clause_decay); veci_resize(&s->model,0); veci_new(&learnt_clause); for (;;){ clause* confl = solver_propagate(s); if (confl != 0){ /* CONFLICT */ int blevel; #ifdef VERBOSEDEBUG printf(L_IND"**CONFLICT**\n", L_ind); #endif s->stats.conflicts++; conflictC++; if (solver_dlevel(s) == s->root_level){ veci_delete(&learnt_clause); return l_False; } veci_resize(&learnt_clause,0); solver_analyze(s, confl, &learnt_clause); blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level; blevel = s->root_level > blevel ? s->root_level : blevel; solver_canceluntil(s,blevel); solver_record(s,&learnt_clause); act_var_decay(s); act_clause_decay(s); }else{ /* NO CONFLICT */ int next; if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ /* Reached bound on number of conflicts: */ s->progress_estimate = solver_progress(s); solver_canceluntil(s,s->root_level); veci_delete(&learnt_clause); return l_Undef; } if (solver_dlevel(s) == 0) /* Simplify the set of problem clauses: */ solver_simplify(s); if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts) /* Reduce the set of learnt clauses: */ solver_reducedb(s); /* New variable decision: */ s->stats.decisions++; next = order_select(s,(float)random_var_freq); if (next == var_Undef){ /* Model found: */ lbool* values = s->assigns; int i; for (i = 0; i < s->size; i++) veci_push(&s->model,(int)values[i]); solver_canceluntil(s,s->root_level); veci_delete(&learnt_clause); /* veci apa; veci_new(&apa); for (i = 0; i < s->size; i++) veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i)))); printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n"); veci_delete(&apa); */ return l_True; } assume(s,lit_neg(toLit(next))); } } #if 0 /* by mao; unreachable code */ return l_Undef; /* cannot happen */ #endif } /*====================================================================*/ /* External solver functions: */ solver* solver_new(void) { solver* s = (solver*)malloc(sizeof(solver)); /* initialize vectors */ vecp_new(&s->clauses); vecp_new(&s->learnts); veci_new(&s->order); veci_new(&s->trail_lim); veci_new(&s->tagged); veci_new(&s->stack); veci_new(&s->model); /* initialize arrays */ s->wlists = 0; s->activity = 0; s->assigns = 0; s->orderpos = 0; s->reasons = 0; s->levels = 0; s->tags = 0; s->trail = 0; /* initialize other vars */ s->size = 0; s->cap = 0; s->qhead = 0; s->qtail = 0; s->cla_inc = 1; s->cla_decay = 1; s->var_inc = 1; s->var_decay = 1; s->root_level = 0; s->simpdb_assigns = 0; s->simpdb_props = 0; s->random_seed = 91648253; s->progress_estimate = 0; s->binary = (clause*)malloc(sizeof(clause) + sizeof(lit)*2); s->binary->size_learnt = (2 << 1); s->verbosity = 0; s->stats.starts = 0; s->stats.decisions = 0; s->stats.propagations = 0; s->stats.inspects = 0; s->stats.conflicts = 0; s->stats.clauses = 0; s->stats.clauses_literals = 0; s->stats.learnts = 0; s->stats.learnts_literals = 0; s->stats.max_literals = 0; s->stats.tot_literals = 0; return s; } void solver_delete(solver* s) { int i; for (i = 0; i < vecp_size(&s->clauses); i++) free(vecp_begin(&s->clauses)[i]); for (i = 0; i < vecp_size(&s->learnts); i++) free(vecp_begin(&s->learnts)[i]); /* delete vectors */ vecp_delete(&s->clauses); vecp_delete(&s->learnts); veci_delete(&s->order); veci_delete(&s->trail_lim); veci_delete(&s->tagged); veci_delete(&s->stack); veci_delete(&s->model); free(s->binary); /* delete arrays */ if (s->wlists != 0){ int i; for (i = 0; i < s->size*2; i++) vecp_delete(&s->wlists[i]); /* if one is different from null, all are */ free(s->wlists); free(s->activity ); free(s->assigns ); free(s->orderpos ); free(s->reasons ); free(s->levels ); free(s->trail ); free(s->tags ); } free(s); } bool solver_addclause(solver* s, lit* begin, lit* end) { lit *i,*j; int maxvar; lbool* values; lit last; if (begin == end) return false; /* printlits(begin,end); printf("\n"); */ /* insertion sort */ maxvar = lit_var(*begin); for (i = begin + 1; i < end; i++){ lit l = *i; maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar; for (j = i; j > begin && *(j-1) > l; j--) *j = *(j-1); *j = l; } solver_setnvars(s,maxvar+1); /* printlits(begin,end); printf("\n"); */ values = s->assigns; /* delete duplicates */ last = lit_Undef; for (i = j = begin; i < end; i++){ /* printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)])); */ lbool sig = !lit_sign(*i); sig += sig - 1; if (*i == lit_neg(last) || sig == values[lit_var(*i)]) return true; /* tautology */ else if (*i != last && values[lit_var(*i)] == l_Undef) last = *j++ = *i; } /* printf("final: "); printlits(begin,j); printf("\n"); */ if (j == begin) /* empty clause */ return false; else if (j - begin == 1) /* unit clause */ return enqueue(s,*begin,(clause*)0); /* create new clause */ vecp_push(&s->clauses,clause_new(s,begin,j,0)); s->stats.clauses++; s->stats.clauses_literals += j - begin; return true; } bool solver_simplify(solver* s) { clause** reasons; int type; assert(solver_dlevel(s) == 0); if (solver_propagate(s) != 0) return false; if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0) return true; reasons = s->reasons; for (type = 0; type < 2; type++){ vecp* cs = type ? &s->learnts : &s->clauses; clause** cls = (clause**)vecp_begin(cs); int i, j; for (j = i = 0; i < vecp_size(cs); i++){ if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] && clause_simplify(s,cls[i]) == l_True) clause_remove(s,cls[i]); else cls[j++] = cls[i]; } vecp_resize(cs,j); } s->simpdb_assigns = s->qhead; /* (shouldn't depend on 'stats' really, but it will do for now) */ s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals); return true; } bool solver_solve(solver* s, lit* begin, lit* end) { double nof_conflicts = 100; double nof_learnts = solver_nclauses(s) / 3; lbool status = l_Undef; lbool* values = s->assigns; lit* i; /* printf("solve: "); printlits(begin, end); printf("\n"); */ for (i = begin; i < end; i++){ switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){ case 1: /* l_True: */ break; case 0: /* l_Undef */ assume(s, *i); if (solver_propagate(s) == NULL) break; /* falltrough */ case -1: /* l_False */ solver_canceluntil(s, 0); return false; } } s->root_level = solver_dlevel(s); if (s->verbosity >= 1){ printf("==================================[MINISAT]============" "=======================\n"); printf("| Conflicts | ORIGINAL | LEARNT " " | Progress |\n"); printf("| | Clauses Literals | Limit Clauses Litera" "ls Lit/Cl | |\n"); printf("=======================================================" "=======================\n"); } while (status == l_Undef){ double Ratio = (s->stats.learnts == 0)? 0.0 : s->stats.learnts_literals / (double)s->stats.learnts; if (s->verbosity >= 1){ printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %" "6.3f %% |\n", (double)s->stats.conflicts, (double)s->stats.clauses, (double)s->stats.clauses_literals, (double)nof_learnts, (double)s->stats.learnts, (double)s->stats.learnts_literals, Ratio, s->progress_estimate*100); fflush(stdout); } status = solver_search(s,(int)nof_conflicts, (int)nof_learnts); nof_conflicts *= 1.5; nof_learnts *= 1.1; } if (s->verbosity >= 1) printf("=======================================================" "=======================\n"); solver_canceluntil(s,0); return status != l_False; } int solver_nvars(solver* s) { return s->size; } int solver_nclauses(solver* s) { return vecp_size(&s->clauses); } int solver_nconflicts(solver* s) { return (int)s->stats.conflicts; } /*====================================================================*/ /* Sorting functions (sigh): */ static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *)) { int i, j, best_i; void* tmp; for (i = 0; i < size-1; i++){ best_i = i; for (j = i+1; j < size; j++){ if (comp(array[j], array[best_i]) < 0) best_i = j; } tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; } } static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed) { if (size <= 15) selectionsort(array, size, comp); else{ void* pivot = array[irand(seed, size)]; void* tmp; int i = -1; int j = size; for(;;){ do i++; while(comp(array[i], pivot)<0); do j--; while(comp(pivot, array[j])<0); if (i >= j) break; tmp = array[i]; array[i] = array[j]; array[j] = tmp; } sortrnd(array , i , comp, seed); sortrnd(&array[i], size-i, comp, seed); } } static void sort(void** array, int size, int(*comp)(const void *, const void *)) { double seed = 91648253; sortrnd(array,size,comp,&seed); } /* eof */