Add graph references
This commit is contained in:
Abdelrahman Said
@@ -0,0 +1,20 @@
|
||||
MiniSat -- Copyright (c) 2005, Niklas Sorensson
|
||||
|
||||
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.
|
||||
@@ -0,0 +1,22 @@
|
||||
NOTE: Files in this subdirectory are NOT part of the GLPK package, but
|
||||
are used with GLPK.
|
||||
|
||||
The original code was modified according to GLPK requirements by
|
||||
Andrew Makhorin <mao@gnu.org>.
|
||||
************************************************************************
|
||||
MiniSat-C v1.14.1
|
||||
========================================
|
||||
|
||||
* Fixed some serious bugs.
|
||||
* Tweaked to be Visual Studio friendly (by Alan Mishchenko).
|
||||
This disabled reading of gzipped DIMACS files and signal handling,
|
||||
but none of these features are essential (and easy to re-enable, if
|
||||
wanted).
|
||||
|
||||
MiniSat-C v1.14
|
||||
========================================
|
||||
|
||||
Ok, we get it. You hate C++. You hate templates. We agree; C++ is a
|
||||
seriously messed up language. Although we are more pragmatic about the
|
||||
quirks and maldesigns in C++, we sympathize with you. So here is a
|
||||
pure C version of MiniSat, put together by Niklas Sorensson.
|
||||
+1315
File diff suppressed because it is too large
Load Diff
@@ -0,0 +1,235 @@
|
||||
/* minisat.h */
|
||||
|
||||
/* Modified by Andrew Makhorin <mao@gnu.org>, 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 */
|
||||
|
||||
#ifndef MINISAT_H
|
||||
#define MINISAT_H
|
||||
|
||||
/*====================================================================*/
|
||||
/* Simple types: */
|
||||
|
||||
/* Changed in igraph: do not try to redefine the standard 'bool',
|
||||
* needed for C23 compatibility. */
|
||||
/*
|
||||
typedef int bool;
|
||||
|
||||
#define true 1
|
||||
#define false 0
|
||||
*/
|
||||
#include <stdbool.h>
|
||||
|
||||
typedef int lit;
|
||||
#if 0 /* by mao */
|
||||
typedef char lbool;
|
||||
#else
|
||||
typedef int lbool;
|
||||
#endif
|
||||
|
||||
#define var_Undef (int)(-1)
|
||||
#define lit_Undef (lit)(-2)
|
||||
|
||||
#define l_Undef (lbool)0
|
||||
#define l_True (lbool)1
|
||||
#define l_False (lbool)(-1)
|
||||
|
||||
#define toLit(v) (lit)((v) + (v))
|
||||
#define lit_neg(l) (lit)((l) ^ 1)
|
||||
#define lit_var(l) (int)((l) >> 1)
|
||||
#define lit_sign(l) (int)((l) & 1)
|
||||
|
||||
/*====================================================================*/
|
||||
/* Vectors: */
|
||||
|
||||
/* vector of 32-bit intergers (added for 64-bit portability) */
|
||||
typedef struct /* veci_t */ {
|
||||
int size;
|
||||
int cap;
|
||||
int* ptr;
|
||||
} veci;
|
||||
|
||||
#define veci_new(v) \
|
||||
{ (v)->size = 0; \
|
||||
(v)->cap = 4; \
|
||||
(v)->ptr = (int*)malloc(sizeof(int)*(v)->cap); \
|
||||
}
|
||||
|
||||
#define veci_delete(v) free((v)->ptr)
|
||||
|
||||
#define veci_begin(v) ((v)->ptr)
|
||||
|
||||
#define veci_size(v) ((v)->size)
|
||||
|
||||
#define veci_resize(v, k) (void)((v)->size = (k))
|
||||
/* only safe to shrink !! */
|
||||
|
||||
#define veci_push(v, e) \
|
||||
{ if ((v)->size == (v)->cap) \
|
||||
{ int newsize = (v)->cap * 2+1; \
|
||||
(v)->ptr = (int*)realloc((v)->ptr,sizeof(int)*newsize); \
|
||||
(v)->cap = newsize; \
|
||||
} \
|
||||
(v)->ptr[(v)->size++] = (e); \
|
||||
}
|
||||
|
||||
/* vector of 32- or 64-bit pointers */
|
||||
typedef struct /* vecp_t */ {
|
||||
int size;
|
||||
int cap;
|
||||
void** ptr;
|
||||
} vecp;
|
||||
|
||||
#define vecp_new(v) \
|
||||
{ (v)->size = 0; \
|
||||
(v)->cap = 4; \
|
||||
(v)->ptr = (void**)malloc(sizeof(void*)*(v)->cap); \
|
||||
}
|
||||
|
||||
#define vecp_delete(v) free((v)->ptr)
|
||||
|
||||
#define vecp_begin(v) ((v)->ptr)
|
||||
|
||||
#define vecp_size(v) ((v)->size)
|
||||
|
||||
#define vecp_resize(v, k) (void)((v)->size = (k))
|
||||
/* only safe to shrink !! */
|
||||
|
||||
#define vecp_push(v, e) \
|
||||
{ if ((v)->size == (v)->cap) \
|
||||
{ int newsize = (v)->cap * 2+1; \
|
||||
(v)->ptr = (void**)realloc((v)->ptr,sizeof(void*)*newsize); \
|
||||
(v)->cap = newsize; \
|
||||
} \
|
||||
(v)->ptr[(v)->size++] = (e); \
|
||||
}
|
||||
|
||||
/*====================================================================*/
|
||||
/* Solver representation: */
|
||||
|
||||
typedef struct /* clause_t */
|
||||
{
|
||||
int size_learnt;
|
||||
lit lits[1];
|
||||
} clause;
|
||||
|
||||
typedef struct /* stats_t */
|
||||
{
|
||||
double starts, decisions, propagations, inspects, conflicts;
|
||||
double clauses, clauses_literals, learnts, learnts_literals,
|
||||
max_literals, tot_literals;
|
||||
} stats;
|
||||
|
||||
typedef struct /* solver_t */
|
||||
{
|
||||
int size; /* nof variables */
|
||||
int cap; /* size of varmaps */
|
||||
int qhead; /* Head index of queue. */
|
||||
int qtail; /* Tail index of queue. */
|
||||
|
||||
/* clauses */
|
||||
vecp clauses; /* List of problem constraints.
|
||||
(contains: clause*) */
|
||||
vecp learnts; /* List of learnt clauses.
|
||||
(contains: clause*) */
|
||||
|
||||
/* activities */
|
||||
double var_inc; /* Amount to bump next variable with. */
|
||||
double var_decay; /* INVERSE decay factor for variable
|
||||
activity: stores 1/decay. */
|
||||
float cla_inc; /* Amount to bump next clause with. */
|
||||
float cla_decay; /* INVERSE decay factor for clause
|
||||
activity: stores 1/decay. */
|
||||
|
||||
vecp* wlists;
|
||||
double* activity; /* A heuristic measurement of the activity
|
||||
of a variable. */
|
||||
lbool* assigns; /* Current values of variables. */
|
||||
int* orderpos; /* Index in variable order. */
|
||||
clause** reasons;
|
||||
int* levels;
|
||||
lit* trail;
|
||||
|
||||
clause* binary; /* A temporary binary clause */
|
||||
lbool* tags;
|
||||
veci tagged; /* (contains: var) */
|
||||
veci stack; /* (contains: var) */
|
||||
|
||||
veci order; /* Variable order. (heap) (contains: var) */
|
||||
veci trail_lim; /* Separator indices for different decision
|
||||
levels in 'trail'. (contains: int) */
|
||||
veci model; /* If problem is solved, this vector
|
||||
contains the model (contains: lbool). */
|
||||
|
||||
int root_level; /* Level of first proper decision. */
|
||||
int simpdb_assigns;/* Number of top-level assignments at last
|
||||
'simplifyDB()'. */
|
||||
int simpdb_props; /* Number of propagations before next
|
||||
'simplifyDB()'. */
|
||||
double random_seed;
|
||||
double progress_estimate;
|
||||
int verbosity; /* Verbosity level.
|
||||
0=silent,
|
||||
1=some progress report,
|
||||
2=everything */
|
||||
|
||||
stats stats;
|
||||
} solver;
|
||||
|
||||
/*====================================================================*/
|
||||
/* Public interface: */
|
||||
|
||||
#if 1 /* by mao; to keep namespace clean */
|
||||
#define solver_new _glp_minisat_new
|
||||
#define solver_delete _glp_minisat_delete
|
||||
#define solver_addclause _glp_minisat_addclause
|
||||
#define solver_simplify _glp_minisat_simplify
|
||||
#define solver_solve _glp_minisat_solve
|
||||
#define solver_nvars _glp_minisat_nvars
|
||||
#define solver_nclauses _glp_minisat_nclauses
|
||||
#define solver_nconflicts _glp_minisat_nconflicts
|
||||
#define solver_setnvars _glp_minisat_setnvars
|
||||
#define solver_propagate _glp_minisat_propagate
|
||||
#define solver_reducedb _glp_minisat_reducedb
|
||||
#endif
|
||||
|
||||
solver* solver_new(void);
|
||||
void solver_delete(solver* s);
|
||||
|
||||
bool solver_addclause(solver* s, lit* begin, lit* end);
|
||||
bool solver_simplify(solver* s);
|
||||
bool solver_solve(solver* s, lit* begin, lit* end);
|
||||
|
||||
int solver_nvars(solver* s);
|
||||
int solver_nclauses(solver* s);
|
||||
int solver_nconflicts(solver* s);
|
||||
|
||||
void solver_setnvars(solver* s,int n);
|
||||
|
||||
#endif
|
||||
|
||||
/* eof */
|
||||
Reference in New Issue
Block a user