cnf.nw - Data structures and algorithms to manipulate CNF instances

<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.

[Table of contents]

Introduction

This file describes data structures and input-output algorithms to manipulate CNF instance of satisfiability problems.

The following terms are used throughout:

variable
a boolean variable x_i allowed to take on the values true or false
literal
a variable (x_i) or its negation (x_i)
clause
a disjunction of literals (x_1 x_2 ...), or a single literal (x_3)
unit clause
a clause containing a single literal
CNF instance
Conjunctive Normal Form instance, a conjunction of clauses, forming a boolean expression C_1 C_2 ...C_n
satisfiability
given a CNF instance, determine if there is some assignment to its variables such that the boolean expression evaluates to true

Root nodes

The root node defines the global structure of the program file. The prototypes for all file local functions should be collected in the module local function prototypes. The bodies of the functions will be collected in functions. We import "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 */
Defines FAILURE, FALSE, SUCCESS, TRUE, UNKNOWN (links are to index).

Internal representation

The CNF instance is internally stored in the following manner. Variables subscripts are used as keys to a table of variable structures, containing pointers to clause lists and weight nodes. A clause list is a linked list of pointers to clause entries representing the clauses each variable is present in. Each clause entry in turn has a clause ID and a literal list, a list of pointers to the literals it contains. The weight node is a structure that holds the heuristic weight of the variable, these will be stored in a heap, to organize the processing of the computation tree.

<CNF data structures>= (<-U)
<Literal list>
<Clause list>
<Variable table>
<Clause table>
<CNF Instance>

Variable table

The variable table is an array of variable entries, to be accessed using the subscript of the variable as a key. We will simply allocate an array. Each variable entry in the table stores the current value of the variable, a pointer to a list of clauses in which there is a positive occurrence of the variable, another for a list of negative occurrences, a third for unit clauses, and a pointer to the variable's weight node.

<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;
Defines VariableNode, variablenode, VariableTable, variabletable (links are to index).

CreateVarTable()

The function 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)
Defines CreateVarTable (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()

This function deallocates the memory assigned to a variable table and cleans up all associated datastructures.

<DeleteVarTable prototype>= (U-> U->)
void DeleteVarTable (VariableTable *vartable_p)
Defines DeleteVarTable (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 node

Each clause node contains an ID, a count of the number of active literals in the clause, and pointers to linked lists of active and unlinked literals in the clause.

<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;
Defines ClauseNode, clausenode (links are to index).

CreateClause()

The function CreateClause() will allocate and initialize an empty clause node.

<CreateClause prototype>= (U-> U->)
ClauseNode * CreateClause (void)
Defines CreateClause (links are to index).

<local function prototypes>+= (<-U) [<-D->]
<CreateClause prototype>;

<functions>+= (<-U) [<-D->]
<CreateClause prototype>
{
  return (ClauseNode *) calloc (1, sizeof (ClauseNode));
}

DeleteClause()

Delete the memory associated with a clause node.

<DeleteClause prototype>= (U-> U->)
void DeleteClause (ClauseNode * clause_p)
Defines DeleteClause (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

A clause list is a linked list of pointers to clause nodes. Like Lisp (car cdr) pairs. Each literal in an instance produces a clause list node. Several list nodes point at the same clause.

<Clause list>+= (<-U) [<-D]
typedef struct clauselist {
    struct clausenode *clause_ptr;
    struct clauselist *next;
} ClauseList;
Defines ClauseList, clauselist (links are to index).

CreateClauseList()

Create a clause list element for tracking clauses.

<CreateClauseList prototype>= (U-> U->)
ClauseList * CreateClauseList (void)
Defines CreateClauseList (links are to index).

<local function prototypes>+= (<-U) [<-D->]
<CreateClauseList prototype>;

<functions>+= (<-U) [<-D->]
<CreateClauseList prototype>
{
  return (ClauseList *) calloc (1, sizeof (ClauseList));
}

DeleteClauseList()

Deallocates the memory associated with a ClauseList. Each node in the list must be freed separately.

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)
Defines DeleteClauseList (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

The clause table is an array of pointers to clauses, used to access each clause in an instance quickly. NOTE: The entire clause should actually be stored here.

<Clause table>= (<-U)
typedef struct clausetable {
  int size;
  struct clausenode **table;   /* pointer to an array of clausenode pointers */
} ClauseTable;
Defines ClauseTable, clausetable (links are to index).

CreateClauseTable()

Dynamically allocates and initializes an empty ClauseTable of size size, and returns a pointer to the new storage.

<CreateClauseTable prototype>= (U-> U->)
ClauseTable *
CreateClauseTable (size_t size)
Defines CreateClauseTable (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()

Deallocates the space reserved for a clause table. Also frees the associated clauses.

<DeleteClauseTable prototype>= (U-> U->)
void DeleteClauseTable (ClauseTable *clause_table_p)
Defines DeleteClauseTable (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

A literal list is a linked list of literal entries, each containing a variable pointer, flag for negation.

<Literal list>= (<-U)
typedef struct literalnode {
  boolean negated;
  struct variablenode *var_ptr;
  struct literalnode *next;
} LiteralNode;
Defines LiteralNode, literalnode (links are to index).

CreateLiteral()

The function CreateLiteral() will allocate and initialize a LiteralNode.

<CreateLiteral prototype>= (U-> U->)
LiteralNode * CreateLiteral (void)
Defines CreateLiteral (links are to index).

<local function prototypes>+= (<-U) [<-D->]
<CreateLiteral prototype>;

<functions>+= (<-U) [<-D->]
<CreateLiteral prototype>
{
  return (LiteralNode *) calloc (1, sizeof (LiteralNode));
}

DeleteLiteralList()

Deallocates the chain of literals starting at the head. Do not use the recursive solution, it is a pig on the inductive inference problems.

<DeleteLiteralList prototype>= (U-> U->)
void DeleteLiteralList (LiteralNode *head)
Defines DeleteLiteralList (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

An actual CNF instance will have a count of the number of active clauses and active variables. In addition, we store a pointer to the variable table and to the clause table.

<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;
Defines cnf, CNFInstance (links are to index).

CreateCNF()

The function 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)
Defines CreateCNFInstance (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;
}

DeleteCNFInstance()

This function disposes the allocated memory of a CNFInstance, freeing all associated data structures.

<DeleteCNFInstance prototype>= (U-> U->)
void DeleteCNFInstance (CNFInstance *instance)
Defines DeleteCNFInstance (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);
  }
}

External representation

The following routines read and write CNF instances of satisfiability problems and translate them to and from our internal data structures.

BuildInstance()

Reads a cnf instance in DIMACS cnf format from a file, using the UCSC parser, then builds a CNFInstance from the parsed instance in the global variable cnf.

The structure cnf is defined in the header file "cnfparse.h".

<BuildInstance prototype>= (U-> U->)
CNFInstance *
BuildInstance (FILE *cnffile)
Defines BuildInstance (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 */
    <traverse clause_p lit list, link clause_p into instance>
    /* 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.

<traverse clause_p lit list, link clause_p into instance>= (<-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;
  }
}

BuildClause()

Given a CNFInstance and a clause number, extract the clause from the global 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)
Defines BuildClause (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;
}

BuildLiteral()

Construct and initialize a literal for the index variable in instance.

<BuildLiteral prototype>= (U-> U->)
LiteralNode * BuildLiteral (CNFInstance *instance, int index)
Defines BuildLiteral (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()

Write out the DIMACS cnf form of an instance.

<WriteInstance prototype>= (U-> U->)
void WriteInstance (FILE *outfile, CNFInstance *instance)
Defines WriteInstance (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()

Write out an individual clause in DIMACS cnf format.

<WriteClause prototype>= (U-> U->)
void WriteClause (FILE *outfile, ClauseNode *clause_p, 
                  VariableNode *base_address)
Defines WriteClause (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");
}

FreeCnf()

Free the memory allocated by the cnf format parser. The global structure 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)
Defines FreeCnf (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;
  }
}

Testing

TestInstance()

Verify that the assignments to the variables in 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)
Defines TestInstance (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;
}

TestClause ()

Verify that at least one literal in a clause_p is satisfied. Return FALSE if none of them are.

<TestClause prototype>= (U-> U->)
boolean TestClause (CNFInstance *instance, long *clause_offset)
Defines TestClause (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;
}

List of code chunks

Keyword index


Troglodita approved!

Humberto Ortiz Zuazaga
humberto@hpcf.upr.edu

Most recent change: 2005/1/2 at 21:07
Generated with GTML