/* \noweboptions{longchunks}       % Get page numbers in chunk list.        */
/* \newcommand{\bnot}{\lnot}                                                */
/* \newcommand{\band}{\wedge}                                               */
/* \newcommand{\bor}{\vee}                                                  */
/* \tableofcontents                                                         */
/* \section{Introduction}                                                   */
/* This file describes data structures and input-output                     */
/* algorithms to manipulate CNF instance of satisfiability problems.        */
/*                                                                          */
/* The following terms are used throughout:                                 */
/* \begin{description}                                                      */
/* \item[variable] a boolean variable $x_i$ allowed to take on the values   */
/*   {\it true } or {\it false}                                             */
/* \item[literal] a variable ($x_i$) or its negation ($\bnot x_i$)          */
/* \item[clause] a disjunction of literals $(x_1 \bor \bnot x_2 \bor        */
/*   \cdots)$, or a single literal $(x_3)$                                  */
/* \item[unit clause] a clause containing a single literal                  */
/* \item[CNF instance] Conjunctive Normal Form instance, a conjunction of   */
/*   clauses, forming a boolean expression $C_1 \band C_2 \band \cdots      */
/*   \band C_n$                                                             */
/* \item[satisfiability] given a CNF instance, determine if there is some   */
/*   assignment to its variables such that the boolean expression           */
/*   evaluates to true                                                      */
/* \end{description}                                                        */
/*                                                                          */
/*                                                                          */
/* \section{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 {\em local function prototypes\/}.  The       */
/* bodies of the functions will be collected in {\em 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.                               */
/*                                                                          */
/*                                                                          */
/* <*>=                                                                     */
/* \title{cnf.nw - Data structures and algorithms to manipulate CNF         */
   /*   instances}                                                             */
   /* \author{}                                                                */
   /* \maketitle                                                               */
   /*                                                                          */
   /* <Copyright notice>=                                                      
   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. */
#include <assert.h>
#include <ctype.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "cnf.h"
#include "cnfparse.h"

/* <local function prototypes>=                                             */
/* \subsubsection{\tt 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>=                                              */
VariableTable * CreateVarTable (size_t size);

/* <local function prototypes>=                                             */
/* \subsubsection{\tt DeleteVarTable()}  This function deallocates the      */
/* memory assigned to a variable table and cleans up all associated         */
/* datastructures.                                                          */
/*                                                                          */
/*                                                                          */
/* <DeleteVarTable prototype>=                                              */
void DeleteVarTable (VariableTable *vartable_p);

/* <local function prototypes>=                                             */
/* \subsubsection{\tt CreateClause()} The function [[CreateClause()]]       */
/* will allocate and initialize an empty clause node.                       */
/*                                                                          */
/*                                                                          */
/* <CreateClause prototype>=                                                */
ClauseNode * CreateClause (void);

/* <local function prototypes>=                                             */
/* \subsubsection{\tt DeleteClause()}  Delete the memory associated         */
/* with a clause node.                                                      */
/*                                                                          */
/*                                                                          */
/* <DeleteClause prototype>=                                                */
void DeleteClause (ClauseNode * clause_p);

/* <local function prototypes>=                                             */
/* \subsubsection{\tt CreateClauseList()} Create a clause list element      */
/* for tracking clauses.                                                    */
/*                                                                          */
/*                                                                          */
/* <CreateClauseList prototype>=                                            */
ClauseList * CreateClauseList (void);

/* <local function prototypes>=                                             */
/* \subsubsection{\tt 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>=                                            */
void DeleteClauseList (ClauseList *head);

/* <local function prototypes>=                                             */
/* \subsubsection{\tt CreateClauseTable()} Dynamically allocates and        */
/* initializes an empty [[ClauseTable]] of size [[size]], and returns a     */
/* pointer to the new storage.                                              */
/*                                                                          */
/*                                                                          */
/* <CreateClauseTable prototype>=                                           */
ClauseTable *
CreateClauseTable (size_t size);

/* <local function prototypes>=                                             */
/* \subsubsection{\tt CreateLiteral()} The function [[CreateLiteral()]]     */
/* will allocate and initialize a [[LiteralNode]].                          */
/*                                                                          */
/*                                                                          */
/* <CreateLiteral prototype>=                                               */
LiteralNode * CreateLiteral (void);

/* <local function prototypes>=                                             */
/* \subsubsection{\tt 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>=                                           */
void DeleteLiteralList (LiteralNode *head);

/* <local function prototypes>=                                             */
/* \subsubsection{\tt 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>=                                                   */
CNFInstance * CreateCNF (size_t vars, size_t clauses);

/* <local function prototypes>=                                             */
/* \subsubsection{\tt 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>=                                                 */
ClauseNode * BuildClause (CNFInstance *instance, int clause_num);

/* <local function prototypes>=                                             */
/* \subsubsection{\tt BuildLiteral()} Construct and initialize a            */
/* literal for the [[index]] variable in [[instance]].                      */
/*                                                                          */
/*                                                                          */
/* <BuildLiteral prototype>=                                                */
LiteralNode * BuildLiteral (CNFInstance *instance, int index);

/* <local function prototypes>=                                             */
/* \subsubsection{\tt WriteClause()} Write out an individual clause in      */
/* DIMACS cnf format.                                                       */
/*                                                                          */
/*                                                                          */
/* <WriteClause prototype>=                                                 */
void WriteClause (FILE *outfile, ClauseNode *clause_p, 
                  VariableNode *base_address);


/* <functions>=                                                             */
/* \subsubsection{\tt 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>=                                              */
VariableTable * CreateVarTable (size_t size)
{
  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;
}

/* <functions>=                                                             */
/* \subsubsection{\tt DeleteVarTable()}  This function deallocates the      */
/* memory assigned to a variable table and cleans up all associated         */
/* datastructures.                                                          */
/*                                                                          */
/*                                                                          */
/* <DeleteVarTable prototype>=                                              */
void DeleteVarTable (VariableTable *vartable_p)
{
  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);
  }
}

/* <functions>=                                                             */
/* \subsubsection{\tt CreateClause()} The function [[CreateClause()]]       */
/* will allocate and initialize an empty clause node.                       */
/*                                                                          */
/*                                                                          */
/* <CreateClause prototype>=                                                */
ClauseNode * CreateClause (void)
{
  return (ClauseNode *) calloc (1, sizeof (ClauseNode));
}

/* <functions>=                                                             */
/* \subsubsection{\tt DeleteClause()}  Delete the memory associated         */
/* with a clause node.                                                      */
/*                                                                          */
/*                                                                          */
/* <DeleteClause prototype>=                                                */
void DeleteClause (ClauseNode * clause_p)
{
  if (NULL != clause_p) {
    DeleteLiteralList (clause_p->lit_head);
    DeleteLiteralList (clause_p->unlinked_literal_head);
    free (clause_p);
  }
}

/* <functions>=                                                             */
/* \subsubsection{\tt CreateClauseList()} Create a clause list element      */
/* for tracking clauses.                                                    */
/*                                                                          */
/*                                                                          */
/* <CreateClauseList prototype>=                                            */
ClauseList * CreateClauseList (void)
{
  return (ClauseList *) calloc (1, sizeof (ClauseList));
}

/* <functions>=                                                             */
/* \subsubsection{\tt 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>=                                            */
void DeleteClauseList (ClauseList *head)
{
  ClauseList *back, *next;

  back = head;
  while (NULL != back) {
    next = back->next;
    free (back);
    back = next;
  }
}

/* <functions>=                                                             */
/* \subsubsection{\tt CreateClauseTable()} Dynamically allocates and        */
/* initializes an empty [[ClauseTable]] of size [[size]], and returns a     */
/* pointer to the new storage.                                              */
/*                                                                          */
/*                                                                          */
/* <CreateClauseTable prototype>=                                           */
ClauseTable *
CreateClauseTable (size_t size)
{
  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;
}

/* <functions>=                                                             */
/* \subsubsection{\tt DeleteClauseTable()} Deallocates the space            */
/* reserved for a clause table.  Also frees the associated clauses.         */
/*                                                                          */
/*                                                                          */
/* <DeleteClauseTable prototype>=                                           */
void DeleteClauseTable (ClauseTable *clause_table_p)
{
  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);
  }
}

/* <functions>=                                                             */
/* \subsubsection{\tt CreateLiteral()} The function [[CreateLiteral()]]     */
/* will allocate and initialize a [[LiteralNode]].                          */
/*                                                                          */
/*                                                                          */
/* <CreateLiteral prototype>=                                               */
LiteralNode * CreateLiteral (void)
{
  return (LiteralNode *) calloc (1, sizeof (LiteralNode));
}

/* <functions>=                                                             */
/* \subsubsection{\tt 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>=                                           */
void DeleteLiteralList (LiteralNode *head)
{
  LiteralNode *back, *next;

  back = head;
  while (NULL != back) {
    next = back->next;
    free (back);
    back = next;
  }
}

/* <functions>=                                                             */
/* \subsubsection{\tt 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>=                                                   */
CNFInstance * CreateCNF (size_t vars, size_t clauses)
{
  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;
}

/* <functions>=                                                             */
/* \subsubsection{\tt DeleteCNFInstance()} This function disposes the       */
/* allocated memory of a [[CNFInstance]], freeing all associated data       */
/* structures.                                                              */
/*                                                                          */
/*                                                                          */
/* <DeleteCNFInstance prototype>=                                           */
void DeleteCNFInstance (CNFInstance *instance)
{
  if (NULL != instance) {
    DeleteClauseTable (instance->clause_table);
    DeleteVarTable (instance->var_table);
    free (instance);
  }
}

/* <functions>=                                                             */
/* \section{External representation} The following routines read and        */
/* write CNF instances of satisfiability problems and translate them to     */
/* and from our internal data structures.                                   */
/*                                                                          */
/* \subsection{\tt 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>=                                               */
CNFInstance *
BuildInstance (FILE *cnffile)
{
  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 */
    /* 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]]>=   */
    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;
      }
    }

    /* Update clause table entry */
    instance->clause_table->table[i] = clause_p;
  }

  return instance;
}

/* <functions>=                                                             */
/* \subsubsection{\tt 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>=                                                 */
ClauseNode * BuildClause (CNFInstance *instance, int clause_num)
{
  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;
}

/* <functions>=                                                             */
/* \subsubsection{\tt BuildLiteral()} Construct and initialize a            */
/* literal for the [[index]] variable in [[instance]].                      */
/*                                                                          */
/*                                                                          */
/* <BuildLiteral prototype>=                                                */
LiteralNode * BuildLiteral (CNFInstance *instance, int index)
{
  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;
}

/* <functions>=                                                             */
/* \subsection{\tt WriteInstance()} Write out the DIMACS cnf form of an     */
/* instance.                                                                */
/*                                                                          */
/*                                                                          */
/* <WriteInstance prototype>=                                               */
void WriteInstance (FILE *outfile, CNFInstance *instance)
{
  int i;
  ClauseNode *clause_p;

  assert (NULL != outfile);
  assert (NULL != instance);

  fprintf (outfile, "c DIMACS cnf format instance.\n\
c Generated by WriteInstance(), cnf.nw.\n\
p 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);
    }
  }
}

/* <functions>=                                                             */
/* \subsubsection{\tt WriteClause()} Write out an individual clause in      */
/* DIMACS cnf format.                                                       */
/*                                                                          */
/*                                                                          */
/* <WriteClause prototype>=                                                 */
void WriteClause (FILE *outfile, ClauseNode *clause_p, 
                  VariableNode *base_address)
{
  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");
}

/* <functions>=                                                             */
/* \subsection{\tt 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>=                                                     */
void FreeCnf (void)
{
  if (NULL != cnf.clauseSpace) {
    free (cnf.clauseSpace);
    cnf.clauseSpace = NULL;
  }
  if (NULL != cnf.offsets) {
    free (cnf.offsets);
    cnf.offsets = NULL;
  }
}

/* <functions>=                                                             */
/* \section{Testing}                                                        */
/*                                                                          */
/* \subsection{\tt 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>=                                                */
boolean TestInstance (CNFInstance *instance)
{
  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;
}

/* <functions>=                                                             */
/* \subsection{\tt TestClause ()}  Verify that at least one literal in      */
/* a [[clause_p]] is satisfied.  Return [[FALSE]] if none of them are.      */
/*                                                                          */
/*                                                                          */
/* <TestClause prototype>=                                                  */
boolean TestClause (CNFInstance *instance, long *clause_offset)
{
  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;
}


