<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.
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
.
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 prototype>= (U-> U->) boolean LocalSearch (CNFInstance *instance)
DefinesLocalSearch
(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; }
Definesdone
,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;
Definesnext_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;
Definesnext_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
DefinesMAX_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); }
<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 prototype>= (U-> U->) int Score (CNFInstance *instance, int variable)
DefinesScore
(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 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; }
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); }
Most recent change: 2005/1/6 at 12:18
Generated with GTML