Andrew, Here are three patches for MiniSat related issues. The first one is a small modification (better comment) of my original patch [1] to restore MiniSat on 64 bit systems. The second is a resend of [2] that handle the case where MiniSat detects trivial conflicts. The third patch allows running intfeas1() on problems without integer objective coefficients, if no bound is specified. All patches are relative to version 4.61.
Somewhat related: There are C bindings for the C++ MiniSat [3], so it may be possible to hook a more recent version to GLPK. Best Regards, Chris Matrakidis PS. Erik, your mail had to be forwarded manually because you are not subscribed to the list. [1] http://lists.gnu.org/archive/html/bug-glpk/2015-11/msg00004.html [2] http://lists.gnu.org/archive/html/bug-glpk/2015-11/msg00009.html [3] https://github.com/niklasso/minisat-c-bindings
From 2d9b6c7c4d800dc8f4c8e4c4ba6fabf2857fa110 Mon Sep 17 00:00:00 2001 From: Chris Matrakidis <[email protected]> Date: Sun, 8 Jan 2017 22:13:26 +0200 Subject: [PATCH 1/3] less restrictive minisat 64-bit portability check diff --git a/src/api/minisat1.c b/src/api/minisat1.c index cb4148d..2244493 100644 --- a/src/api/minisat1.c +++ b/src/api/minisat1.c @@ -50,9 +50,9 @@ int glp_minisat1(glp_prob *P) goto done; } #if 1 /* 07/XI-2015 */ - if (sizeof(void *) != sizeof(int)) + if (sizeof(void *) != sizeof(size_t)) { xprintf("glp_minisat1: sorry, MiniSat solver is not supported " - "on 64-bit platforms\n"); + "on this platform\n"); ret = GLP_EFAIL; goto done; } diff --git a/src/minisat/minisat.c b/src/minisat/minisat.c index f242d83..47cf920 100644 --- a/src/minisat/minisat.c +++ b/src/minisat/minisat.c @@ -143,13 +143,13 @@ struct clause_t /* Encode literals in clause pointers: */ #define clause_from_lit(l) \ - (clause*)((unsigned long)(l) + (unsigned long)(l) + 1) + (clause*)((size_t)(l) + (size_t)(l) + 1) #define clause_is_lit(c) \ - ((unsigned long)(c) & 1) + ((size_t)(c) & 1) #define clause_read_lit(c) \ - (lit)((unsigned long)(c) >> 1) + (lit)((size_t)(c) >> 1) /*====================================================================*/ /* Simple helpers: */ @@ -332,8 +332,11 @@ static clause* clause_new(solver* s, lit* begin, lit* end, int learnt) c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); c->size_learnt = (size << 1) | learnt; -#if 0 /* by mao; meaningless non-portable check */ - assert(((unsigned int)c & 1) == 0); +#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++) -- 2.7.4
From c8155b7c33eaaa1894df7d9be26e493428121a6b Mon Sep 17 00:00:00 2001 From: Chris Matrakidis <[email protected]> Date: Sun, 8 Jan 2017 21:41:58 +0200 Subject: [PATCH 2/3] remove assert where minisat detects trivial conflicts diff --git a/src/api/minisat1.c b/src/api/minisat1.c index 2244493..1b7ea91 100644 --- a/src/api/minisat1.c +++ b/src/api/minisat1.c @@ -88,7 +88,13 @@ int glp_minisat1(glp_prob *P) ind[len] = lit_neg(ind[len]); } xassert(len > 0); - xassert(solver_addclause(s, &ind[1], &ind[1+len])); + 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 */ -- 2.7.4
From b232c5f7ae1ccd16b2b9aa2ddc1ca8c0c8ef2b62 Mon Sep 17 00:00:00 2001 From: Chris Matrakidis <[email protected]> Date: Sun, 8 Jan 2017 23:31:03 +0200 Subject: [PATCH 3/3] intfeas1 needs to check objective only when bound specified diff --git a/src/api/intfeas1.c b/src/api/intfeas1.c index c2e5989..f440984 100644 --- a/src/api/intfeas1.c +++ b/src/api/intfeas1.c @@ -123,22 +123,24 @@ int glp_intfeas1(glp_prob *P, int use_bound, int obj_bound) goto done; } } - /* check the objective function */ - 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); + /* 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)); -- 2.7.4
_______________________________________________ Help-glpk mailing list [email protected] https://lists.gnu.org/mailman/listinfo/help-glpk
