hill.nw - Hill climbing routines for solving satisfiabilty problems.

<Copyright notice>= (U-> 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.

Introduction

Hill climbing or local search procedures for solving instances of satisfiability seem to perform well on satisfiable instances. This module implements the basic GSAT like procedures to work on instances as defined in cnf.nw.

Root modules

The structure of the source files is typical. The root module imports all header files and defines the function bodies. It expands into the hill.c file.

<*>=
/* <Copyright notice> */
#include <stdio.h>
#include <stdlib.h>
#include <time.h>
#include "cnf.h"
#include "hill.h"

<local definitions>

<local function prototypes>

<functions>

The header module collects exported definitions, it expands into the hill.h file.

<header>=
#ifndef HILL_H
#define HILL_H
/* <Copyright notice> */

<external function prototypes>

#endif

LocalSearch()

The general algorithm is quite simple:

<LocalSearch prototype>= (U-> U->)
boolean LocalSearch (CNFInstance *instance)
Defines LocalSearch (links are to index).

<external function prototypes>= (<-U)
<LocalSearch prototype>;

<functions>= (<-U) [D->]
<LocalSearch prototype> {
  <LocalSearch local variables>
  boolean done = FALSE;
  boolean solved = FALSE;

  <pick an initial assignment>
  <prepare for search>
  while (!done) {
    <pick a variable>
    <flip the variable's assignment>
    <check instance>
  }
  return solved;
}
Defines done, solved (links are to index).

The simplest way to pick the assignment is at random. Unfortuately, Sun's rand() sucks raw eggs. We redefine it to random() which is better.

<local definitions>= (<-U) [D->]
#ifndef __linux__
#define rand random
#define srand srandom
#endif

<LocalSearch local variables>= (<-U) [D->]
int var;

<pick an initial assignment>= (<-U)
srand ((unsigned) time (NULL));
for (var = 1; var <= instance->var_cnt; var++) {
  instance->var_table->table[var].value = (rand() % 2) ? TRUE : FALSE;
}

After making our assignment, add up all the satisfied clauses. Then as we work, update this count until we're done.

<LocalSearch local variables>+= (<-U) [<-D->]
int sat_clause_count;
int next_var;
int num_iterations;
Defines next_var, num_iterations, sat_clause_count (links are to index).

<prepare for search>= (<-U)
<count satisfied clauses>
done = solved = (sat_clause_count >= instance->clause_cnt);
next_var = 0;
num_iterations = 0;

We can just cycle through all the variables in order, picking one if it meets our conditions. Chose any varible that improves our score, or if a zero improvement is found first, chose it 10%of the time. We could get trapped in an infinite loop if not careful.

<local definitions>+= (<-U) [<-D->]
#define ZEROCHANGE_FRACTION 10 /* 1 out of 10 chosen */

<LocalSearch local variables>+= (<-U) [<-D->]
int next_score;
Defines next_score (links are to index).

<pick a variable>= (<-U)
while (1) {
  if (instance->var_cnt <= next_var) {
    next_var = 0;
  }
  next_var++;
  next_score = Score (instance, next_var);
  if (0 < next_score)
    break; /* improved */
  else if ((0 == next_score) && (0 == rand() % ZEROCHANGE_FRACTION))
    break; /* not improved */
}

<flip the variable's assignment>= (<-U)
Flip (instance, next_var);
sat_clause_count += next_score;

We'll terminate if either the instance is solved, or the loop counter maxes out.

<local definitions>+= (<-U) [<-D]
#define MAX_ITERATIONS 100000
Defines MAX_ITERATIONS (links are to index).

<check instance>= (<-U)
num_iterations++;
done = solved = (sat_clause_count >= instance->clause_cnt);
if (!solved) {
  if (0 == (num_iterations % 1000)) {
    printf ("%d: variable %d scored %d, count is %d.\n", num_iterations,
            next_var, next_score, sat_clause_count);
  }
  done = (MAX_ITERATIONS <= num_iterations);
}

Counting clauses

When we initialize the instance, we can count up the number of ``redundant literals'' in a clause, and use this number to determine if flipping a literal will change the status of the count. This should be done while performing the assignment, but we can just do it here.

<LocalSearch local variables>+= (<-U) [<-D]
int clause;
ClauseNode *clause_p;
LiteralNode *lit_p;

<count satisfied clauses>= (<-U)
sat_clause_count = 0;
for (clause = 1; clause <= instance->clause_cnt; clause++) {
  clause_p = instance->clause_table->table[clause];
  lit_p = clause_p->lit_head;
  while (NULL != lit_p) {
    if (TRUE == lit_p->negated) {
      if (FALSE == lit_p->var_ptr->value)
        clause_p->sat_count++;
    } else {
      if (TRUE == lit_p->var_ptr->value) {
        clause_p->sat_count++;
      }
    }
    lit_p = lit_p->next;
  }
  if (0 < clause_p->sat_count) {
    sat_clause_count++;
  }
}
printf ("initial assignment satisfies %d clauses.\n", sat_clause_count);

Score()

Return the number of clauses affected by a possible flip of a variable. Negative numbers mean more clauses were falsified, positive mean more clauses were satisfied.

<Score prototype>= (U-> U->)
int Score (CNFInstance *instance, int variable)
Defines Score (links are to index).

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

<functions>+= (<-U) [<-D->]
<Score prototype> {
  ClauseList *pos_list, *neg_list;
  int score = 0;
  
  if (TRUE == instance->var_table->table[variable].value) {
    pos_list = instance->var_table->table[variable].neg_head;
    neg_list = instance->var_table->table[variable].pos_head;
  } else {
    pos_list = instance->var_table->table[variable].pos_head;
    neg_list = instance->var_table->table[variable].neg_head;
  }
  while (NULL != pos_list) {
    if (0 == pos_list->clause_ptr->sat_count) {
      score++;
    }
    pos_list = pos_list->next;
  }
  while (NULL != neg_list) {
    if (1 == neg_list->clause_ptr->sat_count) {
      score--;
    }
    neg_list = neg_list->next;
  }
  return score;
}

Flip()

Flip a variable, and update the instance.

<Flip prototype>= (U-> U->)
void Flip (CNFInstance *instance, int variable)

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

<functions>+= (<-U) [<-D]
<Flip prototype> {
  ClauseList *pos_list, *neg_list;
  boolean next_value;

  if (TRUE == instance->var_table->table[variable].value) {
    pos_list = instance->var_table->table[variable].neg_head;
    neg_list = instance->var_table->table[variable].pos_head;
    next_value = FALSE;
  } else {
    pos_list = instance->var_table->table[variable].pos_head;
    neg_list = instance->var_table->table[variable].neg_head;
    next_value = TRUE;
  }
  while (NULL != pos_list) {
    pos_list->clause_ptr->sat_count++;
    pos_list = pos_list->next;
  }
  while (NULL != neg_list) {
    if (0 < neg_list->clause_ptr->sat_count)
      neg_list->clause_ptr->sat_count--;
    neg_list = neg_list->next;
  }
  instance->var_table->table[variable].value = next_value;
}

Test harness

To test the operation of LocalSearch() we need to construct an instance and feed it to the function. This code must be linked with cnf.o and hill.o (See the Makefile).

<testhill.c>=
/* <Copyright notice> */
#include <assert.h>
#include <stdio.h>
#include <stdlib.h>
#include "cnfparse.h"
#include "cnf.h"
#include "hill.h"

int main (int, char**);

int main (int argc, char *argv[]) {
  FILE *infile;
  CNFInstance *instance;

  if (2 != argc) {
    fprintf (stderr,
"    Testhill version 0.1, Copyright (C) 1993 Fred Annexstein,\n    John Franco, Humberto Ortiz-Zuazaga, and Manian Swaminathan.\n    Testhill comes with ABSOLUTELY NO WARRANTY; for details see\n    the file COPYING.\n    This is free software, and you are welcome to redistribute it\n    under certain conditions; see the file COPYING for details.\n\nUsage: testhill {inputfile}\n");
    exit (1);
  }

  printf ("    Testhill version 0.1, Copyright (C) 1993 Fred Annexstein,\n    John Franco, Humberto Ortiz-Zuazaga, and Manian Swaminathan.\n\n");

  if (NULL == (infile = fopen (argv[1], "r"))) {
    fprintf (stderr, "Cannot open file %s\n", argv[1]);
    exit (1);
  }
  
  instance = BuildInstance (infile);
  assert (NULL != instance);

  fclose (infile);

  printf ("Clauses:  %d, Variables:  %d, Longest:  %d\n",
          instance->clause_cnt, instance->var_cnt, instance->longest_clause);

  if (TRUE == LocalSearch (instance)) {
    if (TRUE == TestInstance (instance)) {
      printf ("Solved!.\n");
    }
    else {
      printf ("Error: LocalSearch returned true for unsatisfied instance.\n");
    }
  }

  DeleteCNFInstance (instance);
  FreeCnf ();

  exit (0);
}

List of code chunks

Keyword index


Troglodita approved!

Humberto Ortiz Zuazaga
humberto@hpcf.upr.edu

Most recent change: 2005/1/6 at 12:18
Generated with GTML