<Copyright notice>= (U-> U->) Copyright (C) 1993 by Fred Annexstein, John Franco, Humberto Ortiz-Zuazaga, Manian Swaminathan This program 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 2 of the License, or (at your option) any later version. This program 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 this program; if not, write to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
The following terms are used throughout:
"cnf.h"
to make sure all the exported functions are correctly
declared. "heap.h"
is required for the definitions of the weight node
structures. "cnfparse.h"
is the interface file for the UCSC
parser for DIMACS cnf format problems. It defines a global structure
called cnf
that contains the instance.
<*>= /* <Copyright notice> */ #include <assert.h> #include <ctype.h> #include <stdio.h> #include <stdlib.h> #include <string.h> #include "cnf.h" #include "cnfparse.h" <local function prototypes> <functions>
The header node is used to generate the "cnf.h"
include file.
All functions to be exported must have their prototypes collected in
the module external function prototypes. All externally
visible data types must also be exported.
<header>= /* <Copyright notice> */ #ifndef CNF_H #define CNF_H enum {FAILURE, SUCCESS}; typedef enum {FALSE, TRUE, UNKNOWN} boolean; <CNF data structures> <external function prototypes> #endif /* CNF_H */
DefinesFAILURE
,FALSE
,SUCCESS
,TRUE
,UNKNOWN
(links are to index).
<CNF data structures>= (<-U) <Literal list> <Clause list> <Variable table> <Clause table> <CNF Instance>
<Variable table>= (<-U) typedef struct variablenode { boolean value; struct clauselist *pos_head; struct clauselist *neg_head; struct clauselist *unit_head; struct clauselist *satisfied_clauselist; struct clauselist *unlinked_clauselist_nodes; struct weightnode *weight_ptr; } VariableNode; typedef struct variabletable { int size; struct variablenode *table; } VariableTable;
DefinesVariableNode
,variablenode
,VariableTable
,variabletable
(links are to index).
CreateVarTable()
builds a contiguous array of variables, using
dynamic allocation. During runtime we should test to see if we run
out of space. By using calloc()
we ensure all pointers are set to
NULL
before starting. The zero'th element is unused.
<CreateVarTable prototype>= (U-> U->) VariableTable * CreateVarTable (size_t size)
DefinesCreateVarTable
(links are to index).
<local function prototypes>= (<-U) [D->] <CreateVarTable prototype>;
<functions>= (<-U) [D->] <CreateVarTable prototype> { VariableTable *vartable; int i; vartable = calloc (1, sizeof(VariableTable)); if (NULL != vartable) { vartable->size = size; vartable->table = (VariableNode *) calloc (size + 1, sizeof (VariableNode)); if (NULL == vartable->table) { free (vartable); vartable = NULL; } else for (i = 1; i <= size; i++) vartable->table[i].value = UNKNOWN; } return vartable; }
<DeleteVarTable prototype>= (U-> U->) void DeleteVarTable (VariableTable *vartable_p)
DefinesDeleteVarTable
(links are to index).
<local function prototypes>+= (<-U) [<-D->] <DeleteVarTable prototype>;
<functions>+= (<-U) [<-D->] <DeleteVarTable prototype> { int i; if (NULL != vartable_p) { if (NULL != vartable_p->table) { for (i = 1; i <= vartable_p->size; i++) { DeleteClauseList (vartable_p->table[i].pos_head); DeleteClauseList (vartable_p->table[i].neg_head); DeleteClauseList (vartable_p->table[i].unit_head); DeleteClauseList (vartable_p->table[i].satisfied_clauselist); DeleteClauseList (vartable_p->table[i].unlinked_clauselist_nodes); } free (vartable_p->table); } free (vartable_p); } }
<Clause list>= (<-U) [D->] typedef struct clausenode { int ID; int lit_cnt; int sat_count; /* count of ``redundant'' literals */ boolean satisfied; struct literalnode *lit_head; struct literalnode *unlinked_literal_head; } ClauseNode;
DefinesClauseNode
,clausenode
(links are to index).
CreateClause()
will allocate and initialize an empty clause node.
<CreateClause prototype>= (U-> U->) ClauseNode * CreateClause (void)
DefinesCreateClause
(links are to index).
<local function prototypes>+= (<-U) [<-D->] <CreateClause prototype>;
<functions>+= (<-U) [<-D->] <CreateClause prototype> { return (ClauseNode *) calloc (1, sizeof (ClauseNode)); }
<DeleteClause prototype>= (U-> U->) void DeleteClause (ClauseNode * clause_p)
DefinesDeleteClause
(links are to index).
<local function prototypes>+= (<-U) [<-D->] <DeleteClause prototype>;
<functions>+= (<-U) [<-D->] <DeleteClause prototype> { if (NULL != clause_p) { DeleteLiteralList (clause_p->lit_head); DeleteLiteralList (clause_p->unlinked_literal_head); free (clause_p); } }
<Clause list>+= (<-U) [<-D] typedef struct clauselist { struct clausenode *clause_ptr; struct clauselist *next; } ClauseList;
DefinesClauseList
,clauselist
(links are to index).
<CreateClauseList prototype>= (U-> U->) ClauseList * CreateClauseList (void)
DefinesCreateClauseList
(links are to index).
<local function prototypes>+= (<-U) [<-D->] <CreateClauseList prototype>;
<functions>+= (<-U) [<-D->] <CreateClauseList prototype> { return (ClauseList *) calloc (1, sizeof (ClauseList)); }
DO NOT DELETE CLAUSES, there are many clauselist nodes pointing at each clause.
NOTE: this was originally implemented as a recursive solution, which
sucked up memory when we may need it most. Replaced it with an
iterative version similar to Dr. Annexstein's loop in "gsat.c"
.
<DeleteClauseList prototype>= (U-> U->) void DeleteClauseList (ClauseList *head)
DefinesDeleteClauseList
(links are to index).
<local function prototypes>+= (<-U) [<-D->] <DeleteClauseList prototype>;
<functions>+= (<-U) [<-D->] <DeleteClauseList prototype> { ClauseList *back, *next; back = head; while (NULL != back) { next = back->next; free (back); back = next; } }
<Clause table>= (<-U) typedef struct clausetable { int size; struct clausenode **table; /* pointer to an array of clausenode pointers */ } ClauseTable;
DefinesClauseTable
,clausetable
(links are to index).
ClauseTable
of size size
, and returns a
pointer to the new storage.
<CreateClauseTable prototype>= (U-> U->) ClauseTable * CreateClauseTable (size_t size)
DefinesCreateClauseTable
(links are to index).
<local function prototypes>+= (<-U) [<-D->] <CreateClauseTable prototype>;
<functions>+= (<-U) [<-D->] <CreateClauseTable prototype> { ClauseTable *clausetable; clausetable = (ClauseTable *) malloc (sizeof (ClauseTable)); if (NULL != clausetable) { clausetable->size = size; clausetable->table = (ClauseNode **) calloc (size + 1, sizeof (ClauseNode *)); if (NULL == clausetable->table) { free (clausetable); } } return clausetable; }
<DeleteClauseTable prototype>= (U-> U->) void DeleteClauseTable (ClauseTable *clause_table_p)
DefinesDeleteClauseTable
(links are to index).
<external function prototypes>= (<-U) [D->] <DeleteClauseTable prototype>;
<functions>+= (<-U) [<-D->] <DeleteClauseTable prototype> { int i; if (NULL != clause_table_p) { if (NULL != clause_table_p->table) { for (i = 1; i <= clause_table_p->size; i++) DeleteClause (clause_table_p->table[i]); free (clause_table_p->table); } free (clause_table_p); } }
<Literal list>= (<-U) typedef struct literalnode { boolean negated; struct variablenode *var_ptr; struct literalnode *next; } LiteralNode;
DefinesLiteralNode
,literalnode
(links are to index).
CreateLiteral()
will allocate and initialize a LiteralNode
.
<CreateLiteral prototype>= (U-> U->) LiteralNode * CreateLiteral (void)
DefinesCreateLiteral
(links are to index).
<local function prototypes>+= (<-U) [<-D->] <CreateLiteral prototype>;
<functions>+= (<-U) [<-D->] <CreateLiteral prototype> { return (LiteralNode *) calloc (1, sizeof (LiteralNode)); }
<DeleteLiteralList prototype>= (U-> U->) void DeleteLiteralList (LiteralNode *head)
DefinesDeleteLiteralList
(links are to index).
<local function prototypes>+= (<-U) [<-D->] <DeleteLiteralList prototype>;
<functions>+= (<-U) [<-D->] <DeleteLiteralList prototype> { LiteralNode *back, *next; back = head; while (NULL != back) { next = back->next; free (back); back = next; } }
<CNF Instance>= (<-U) typedef struct cnf { size_t clause_cnt; size_t var_cnt; size_t longest_clause; size_t number_literals; VariableTable *var_table; ClauseTable *clause_table; } CNFInstance;
Definescnf
,CNFInstance
(links are to index).
CreateCNF()
allocates and initializes a CNFInstance
, it calls
CreateVarTable()
to build the variable table, of size
vars
.
The clause table is also constructed here. The instance returned is
valid, but empty. BuildInstance()
needs to add in the literals
and fill in the pointers according to the actual instance read from disk.
<CreateCNF prototype>= (U-> U->) CNFInstance * CreateCNF (size_t vars, size_t clauses)
DefinesCreateCNFInstance
(links are to index).
<local function prototypes>+= (<-U) [<-D->] <CreateCNF prototype>;
<functions>+= (<-U) [<-D->] <CreateCNF prototype> { CNFInstance *instance; instance = (CNFInstance *) malloc (sizeof (CNFInstance)); if (NULL != instance) { instance->clause_cnt = clauses; instance->clause_table = CreateClauseTable (clauses); instance->var_cnt = vars; instance->var_table = CreateVarTable (vars); if ((NULL == instance->var_table) || (NULL == instance->clause_table)) { free (instance); instance = NULL; } } return instance; }
CNFInstance
, freeing all associated data
structures.
<DeleteCNFInstance prototype>= (U-> U->) void DeleteCNFInstance (CNFInstance *instance)
DefinesDeleteCNFInstance
(links are to index).
<external function prototypes>+= (<-U) [<-D->] <DeleteCNFInstance prototype>;
<functions>+= (<-U) [<-D->] <DeleteCNFInstance prototype> { if (NULL != instance) { DeleteClauseTable (instance->clause_table); DeleteVarTable (instance->var_table); free (instance); } }
cnf
.
The structure cnf
is defined in the header file "cnfparse.h"
.
<BuildInstance prototype>= (U-> U->) CNFInstance * BuildInstance (FILE *cnffile)
DefinesBuildInstance
(links are to index).
<external function prototypes>+= (<-U) [<-D->] <BuildInstance prototype>;
<functions>+= (<-U) [<-D->] <BuildInstance prototype> { int i; CNFInstance *instance; LiteralNode *lit_p; ClauseNode *clause_p; ClauseList *clp; assert (NULL != cnffile); if (0 > loadCnf (cnffile, stdout)) /* read the cnf file, prepare [[cnf]] */ return NULL; /* parser failed */ /* global cnf structure has been filled */ instance = CreateCNF ((size_t) cnf.numVars, (size_t) cnf.numClauses); if (NULL == instance) return NULL; instance->longest_clause = cnf.longest; instance->number_literals = cnf.numLitOccs; for (i = 1; i <= cnf.numClauses; i++) { clause_p = BuildClause (instance, i); if (NULL == clause_p) return NULL; /* should destroy instance */ <traverseclause_p
lit list, linkclause_p
intoinstance
> /* Update clause table entry */ instance->clause_table->table[i] = clause_p; } return instance; }
As each clause is processed, the varaiables associated with each literal in the clause must be set to point to the new clause through their clause lists. The nodes are just pushed onto a stack, to keep it fast and simple. None of the other routines depends on the order of the clauses.
<traverseclause_p
lit list, linkclause_p
intoinstance
>= (<-U) for (lit_p = clause_p->lit_head; lit_p; lit_p = lit_p->next) { clp = CreateClauseList(); if (NULL == clp) return NULL; clp->clause_ptr = clause_p; /* should test for unit clauses */ if (lit_p->negated) { clp->next = lit_p->var_ptr->neg_head; lit_p->var_ptr->neg_head = clp; } else { clp->next = lit_p->var_ptr->pos_head; lit_p->var_ptr->pos_head = clp; } }
cnf
and merge it into
the instance. Returns clause_p
on sucessfull completion,
NULL
on failure. The structure cnf
is described in
"Cnfparse/cnfparse.h"
. This routine should be modified to use a
single block of storage for the clauses, most likely the
ClauseTable
.
<BuildClause prototype>= (U-> U->) ClauseNode * BuildClause (CNFInstance *instance, int clause_num)
DefinesBuildClause
(links are to index).
<local function prototypes>+= (<-U) [<-D->] <BuildClause prototype>;
<functions>+= (<-U) [<-D->] <BuildClause prototype> { int i; long *cnfClauseSpace; ClauseNode *clause_p; LiteralNode *literal_p; assert (NULL != instance); assert (0 < clause_num); assert (cnf.numClauses >= clause_num); clause_p = CreateClause (); if (NULL == clause_p) return NULL; cnfClauseSpace = cnf.clauseSpace + cnf.offsets[clause_num]; clause_p->ID = clause_num; clause_p->lit_cnt = cnfClauseSpace[0]; for (i = 1; i <= clause_p->lit_cnt; i++) { literal_p = BuildLiteral (instance, cnfClauseSpace[i]); if (NULL == literal_p) return NULL; literal_p->next = clause_p->lit_head; clause_p->lit_head = literal_p; } return clause_p; }
index
variable in instance
.
<BuildLiteral prototype>= (U-> U->) LiteralNode * BuildLiteral (CNFInstance *instance, int index)
DefinesBuildLiteral
(links are to index).
<local function prototypes>+= (<-U) [<-D->] <BuildLiteral prototype>;
<functions>+= (<-U) [<-D->] <BuildLiteral prototype> { LiteralNode *lit_p; assert (NULL != instance); lit_p = CreateLiteral (); if (NULL == lit_p) return NULL; if (0 > index) { lit_p->negated = TRUE; index = 0 - index; /* make index positive */ } lit_p->var_ptr = instance->var_table->table + index; return lit_p; }
<WriteInstance prototype>= (U-> U->) void WriteInstance (FILE *outfile, CNFInstance *instance)
DefinesWriteInstance
(links are to index).
<external function prototypes>+= (<-U) [<-D->] <WriteInstance prototype>;
<functions>+= (<-U) [<-D->] <WriteInstance prototype> { int i; ClauseNode *clause_p; assert (NULL != outfile); assert (NULL != instance); fprintf (outfile, "c DIMACS cnf format instance.\nc Generated by WriteInstance(), cnf.nw.\np cnf %d %d\n", instance->var_table->size, instance->clause_cnt); for (i = 1; i <= instance->clause_table->size; i++) { if (NULL != (clause_p = instance->clause_table->table[i])) { WriteClause (outfile, clause_p, instance->var_table->table); } } }
<WriteClause prototype>= (U-> U->) void WriteClause (FILE *outfile, ClauseNode *clause_p, VariableNode *base_address)
DefinesWriteClause
(links are to index).
<local function prototypes>+= (<-U) [<-D] <WriteClause prototype>;
<functions>+= (<-U) [<-D->] <WriteClause prototype> { LiteralNode *lit_p; assert (NULL != outfile); assert (NULL != clause_p); assert (NULL != base_address); /* test for empty clause here first, or not? */ if (TRUE == clause_p->satisfied) return; for (lit_p = clause_p->lit_head; NULL != lit_p; lit_p = lit_p->next) { if (UNKNOWN == lit_p->var_ptr->value) { /* ignore variables that have been set */ if (TRUE == lit_p->negated) fprintf (outfile, "-"); fprintf (outfile, "%d ", lit_p->var_ptr - base_address); } } fprintf (outfile, "0\n"); }
cnf
has pointers to two
dynamically allocated arrays which must be reclaimed before exiting.
The actual cnf structure may not be freed, as it is declared global in
the UCSC parser. (why?)
<FreeCnf prototype>= (U-> U->) void FreeCnf (void)
DefinesFreeCnf
(links are to index).
<external function prototypes>+= (<-U) [<-D->] <FreeCnf prototype>;
<functions>+= (<-U) [<-D->] <FreeCnf prototype> { if (NULL != cnf.clauseSpace) { free (cnf.clauseSpace); cnf.clauseSpace = NULL; } if (NULL != cnf.offsets) { free (cnf.offsets); cnf.offsets = NULL; } }
instance
do indeed satisfy the instance as read from
the disk file, and stored in the cnf
global structure. All the
clauses in the instance must be true. Return FALSE
if not.
<TestInstance prototype>= (U-> U->) boolean TestInstance (CNFInstance *instance)
DefinesTestInstance
(links are to index).
<external function prototypes>+= (<-U) [<-D->] <TestInstance prototype>;
<functions>+= (<-U) [<-D->] <TestInstance prototype> { int i; long *clause_offset; assert (NULL != instance); assert (NULL != cnf.clauseSpace); assert (NULL != cnf.offsets); for (i = 1; i <= cnf.numClauses; i++) { clause_offset = cnf.clauseSpace + cnf.offsets[i]; if (FALSE == TestClause (instance, clause_offset)) return FALSE; } return TRUE; }
clause_p
is satisfied. Return FALSE
if none of them are.
<TestClause prototype>= (U-> U->) boolean TestClause (CNFInstance *instance, long *clause_offset)
DefinesTestClause
(links are to index).
<external function prototypes>+= (<-U) [<-D] <TestClause prototype>;
<functions>+= (<-U) [<-D] <TestClause prototype> { int i, literal_count; assert (NULL != instance); assert (NULL != clause_offset); literal_count = clause_offset[0]; for (i = 1; i <= literal_count; i++) { if (clause_offset[i] < 0) { /* literal is negated */ if (FALSE == instance->var_table->table[-clause_offset[i]].value) return TRUE; } else { if (TRUE == instance->var_table->table[clause_offset[i]].value) return TRUE; } } return FALSE; }
clause_p
lit list, link clause_p
into instance
>: U1, D2
Most recent change: 2005/1/2 at 21:07
Generated with GTML