/* \tableofcontents                                                         */
/* \noweboptions{longchunks}       % Get page numbers in chunk list.        */
/* \section{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]].                                                */
/*                                                                          */
/* \section{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.                                                         */
/*                                                                          */
/*                                                                          */
/* <*>=                                                                     */
/* \title{hill.nw - Hill climbing routines for solving satisfiabilty problems.} */
   /* \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 <stdio.h>
#include <stdlib.h>
#include <time.h>
#include "cnf.h"
#include "hill.h"

/* 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>=                                                     */
#ifndef __linux__
#define rand random
#define srand srandom
#endif

/* 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>=                                                     */
#define ZEROCHANGE_FRACTION 10 /* 1 out of 10 chosen */

/* We'll terminate if either the instance is solved, or the loop            */
/* counter maxes out.                                                       */
/*                                                                          */
/*                                                                          */
/* <local definitions>=                                                     */
#define MAX_ITERATIONS 100000

/* <local function prototypes>=                                             */
/* \subsection{\tt 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>=                                                       */
int Score (CNFInstance *instance, int variable);

/* <local function prototypes>=                                             */
/* \subsection{\tt Flip()} Flip a variable, and update the instance.        */
/*                                                                          */
/*                                                                          */
/* <Flip prototype>=                                                        */
void Flip (CNFInstance *instance, int variable)
;


/* <functions>=                                                             */
/* \section{\tt LocalSearch()}                                              */
/* The general algorithm is quite simple:                                   */
/*                                                                          */
/*                                                                          */
/* <LocalSearch prototype>=                                                 */
boolean LocalSearch (CNFInstance *instance) {
  /* <LocalSearch local variables>=                                           */
  int var;

  /* After making our assignment, add up all the satisfied clauses.  Then     */
  /* as we work, update this count until we're done.                          */
  /*                                                                          */
  /*                                                                          */
  /* <LocalSearch local variables>=                                           */
  int sat_clause_count;
  int next_var;
  int num_iterations;
  /* <LocalSearch local variables>=                                           */
  int next_score;
  /* \section{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>=                                           */
  int clause;
  ClauseNode *clause_p;
  LiteralNode *lit_p;

  boolean done = FALSE;
  boolean solved = FALSE;

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

  /* <prepare for search>=                                                    */
  /* <count satisfied clauses>=                                               */
  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);

  done = solved = (sat_clause_count >= instance->clause_cnt);
  next_var = 0;
  num_iterations = 0;

  while (!done) {
    /* <pick a variable>=                                                       */
    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>=                                        */
    Flip (instance, next_var);
    sat_clause_count += next_score;

    /* <check instance>=                                                        */
    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);
    }

  }
  return solved;
}
/* <functions>=                                                             */
/* \subsection{\tt 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>=                                                       */
int Score (CNFInstance *instance, int variable) {
  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;
}

/* <functions>=                                                             */
/* \subsection{\tt Flip()} Flip a variable, and update the instance.        */
/*                                                                          */
/*                                                                          */
/* <Flip prototype>=                                                        */
void Flip (CNFInstance *instance, int variable)
 {
  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;
}


