리포트가 영어로 되어 있는 관계로 한국어로 간략하게설명드리겠습니다. 요즘 영어 강의가 늘어나는 추세여서 말이죠.Boolean Satisfiability Problem이라는 것은 n개의 변수가 있는 논리식이있다고 하면 이것을 만족시키기 위한 각 변수들의 논리값들을 구하는문제입니다. 예를 들어서 (A or not B) and (A or C) and (not B) and (not C)라는 식이 있을 때 A가 True, B가 False, C가 False가 되면 저 전체 식이True가 됩니다.입력 형식은 prob1부터 prob10 파일 안에 들어 있는데 이것이 모두 텍스트파일이므로 적당한 텍스트 에디터로 열어서 보시면 되겠습니다. 줄바꿈이 잘안 되면 unix2dos 같은 것을 써 보시구요. (개발은 리눅스에서 했습니다.)일단 입력 파일 형식은 리포트 첫 페이지 보시면 나옵니다. 알파벳으로 적힌것들은 모두 무시하시고 숫자만 보면 됩니다. 두 번째 줄에 있는 숫자는변수의 갯수와 Clause의 갯수입니다. 아, 입력 형식은 CNF로 되어있습니다. 이게 뭐냐 하면 일단 or로 한번 묶고 and로 묶은 겁니다. 저 위에있는 논리식은 CNF가 되겠습니다. not은 하나의 변수에는 붙을 수 있지만Clause에는 붙을 수 없습니다. 즉 아래와 같은 것은 CNF가 아니라는 겁니다. not (A or B) and (B or C)물론 어떤 논리식이라도 CNF 형태로 만들 수 있습니다. 위의 것을 풀어보면 = (not A) and (not B) and (B or C)로 CNF 형태가 나왔습니다. 다음 예제 역시 CNF입니다. (A or not B or not C) and (B or not C or D)여튼 입력 파일의 세 번째 줄부터는 한 줄에 한 Clause씩 들어갑니다. 줄의마지막에는 0이 들어가 있습니다. 그러니까 같은 줄에 있는 것끼리 or로묶인 것이고 서로 다른 줄에 있는 것들끼리 and로 묶인 것이니 모든 라인이다 True가 되어야 전체 식이 참이 되는 겁니다.아, 그리고 변수는 문자로 되어 있는 것이 아니라 숫자로 되어있습니다. 이것은 1부터 시작합니다. 음수는 not이 붙었다는 것을의미합니다. 따라서 방금 전에 살펴본 예제를 입력 파일 형태로 바꾸면아래와 같은 형식이 됩니다. A, B, C, D를 순서대로 1, 2, 3, 4로붙였습니다.c print out cnf filep cnf 4 21 -2 -3 02 -3 4 0출력 형식은 False가 나온 Clause의 수가 첫 줄에 나오고 그 다음부터는각각의 변수의 논리값입니다. 0은 False이고 1은 True입니다. 즉, 첫 줄에나오는 숫자가 0이면 이 문제의 해답을 구한 것이 됩니다.cnf.hh에 보시면 default_kmax라는 것이 있는데 이 값을 고쳐주거나,sat.cc에 있는 메인 함수에서 SimulatedAnnealing을 호출할 때 여기에숫자를 넘겨주면 kmax가 세팅되고, 이 값이 높으면 높을수록 시간이 오래걸리지만 복잡한 문제를 풀 가능성이 높아집니다. 초기값으로 10000000이들어가 있습니다.이 과제가 10개의 문제 중에서 2개만 풀면 만점이라서, 2개가 풀리길래 그냥제출해 버렸는데, 아마 나머지 8개는 안 풀리는 문제 같습니다. 문제는교수님께서 랜덤하게 만드셨다고 하시더라구요. 그럼 안 풀리는 문제가존재할 수 있습니다.여튼 보고서, 주석 전부 영어라서 안구에 습기가 차실 분도 있으시겠지만,이 정도 설명이면 대략 이해하실 수 있으리라고 생각합니다. 아울러리포트나 주석에 영어 틀렸다고 알려주신다면 것은 감사하겠지만 태클걸지는 말아주시기 바랍니다. 그런 것엔 전혀 신경을 안 썼어요.컴파일은 Makefile 쓰실 줄 아시면 그것을 손 봐서 쓰시면 되고, 아니면sat.cc cnf.cc cnf.hh 파일 셋을 한 프로젝트에 넣고 컴파일 하시면됩니다.아, 그리고 윈도에서 실행을 하시려면 명령 프롬프트에서 실행 파일이 있는곳으로 가서 <랑 > 둘다 입력해서 (redirection이므로)sat.exe < 입력파일이름 > 출력파일이름이런 식으로 하면 되고, 그게 싫으시면 코드를 조금 고치시거나 입력 파일내용을 긁어서 붙이시면 됩니다. 입력이 잘 안 되면 unix2dos로 입력 파일변환을 시도해 보십시오.** 이 파일 내용은 README-KOR.txt 파일 안에 담아 두었습니다.** 찾는 분이 별로 없을 듯 해서 가격은 약간 비싸게 책정했습니다.
구조체들입니다.struct linked_list{ struct list_node *head;}; 위의 구조체는 리스트 전체를 관리하는 구조체인데 단지 dummy head node의 포인터만 가지고 있습니다. Dummy head node라는 것은 구현의 편의를 위하여, 첫번째 노드에는 아무런 데이터를 기록하지 않고 그냥 빈 노드를 두는 것을 의미합니다. 이것은 Single Linked List이므로 dummy head만 필요하지만 Double Linked List의 경우에는 구현의 편의를 위하여 dummy tail도 함께 사용하고 있습니다. 물론 바로 첫번째 노드를 head로 포인팅할 수도 있겠지만 여러모로 dummy head node를 쓰는 것이 편리하여 그렇게 하였습니다.struct list_node{ data_type data; struct list_node *next;};이것은 리스트의 각각의 노드들의 구조체입니다. 노드는 데이터를 가지고 있고, 다음 노드를 가리키는 포인터로 이루어져 있습니다.List와 관련하여 외부에서 제공되는 함수들의 목록입니다. 사용 방법은 대체로 리스트 포인터를 첫번쨰 인자로 넘겨주고 필요한 경우에 두번째 인자를 받는 형태입니다.struct linked_list *linked_list_create();리스트를 새로 만들어서 리턴합니다.int linked_list_size(struct linked_list *list);리스트 크기를 리턴합니다.void linked_list_add_first(struct linked_list *list, data_type param_data);리스트 앞에 데이터를 덧붙입니다.void linked_list_add_last(struct linked_list *list, data_type param_data);리스트의 뒤에 데이터를 덧붙입니다.int linked_list_remove_first(struct linked_list *list);첫번째 데이터를 제거하고 리턴합니다.int linked_list_remove_last(struct linked_list *list);마지막 데이터를 제거하고 리턴합니다.data_type linked_list_remove(struct linked_list *list, data_type param_data);특정 데이터를 찾아서 지웁니다.data_type linked_list_get(struct linked_list *list, int index);index 번째의 데이터를 리턴합니다.data_type linked_list_get_first(struct linked_list *list);첫번째 데이터를 리턴합니다.data_type linked_list_get_last(struct linked_list *list);마지막 데이터를 리턴합니다.int linked_list_item_exist(struct linked_list *list, data_type param_data);데이터가 리스트내에 존재하는지 여부를 리턴합니다.int linked_list_is_empty(struct linked_list *list);리스트가 비어 있는지를 리턴합니다.void linked_list_clear(struct linked_list *list);리스트의 내용을 깨끗이 비웁니다.void linked_list_destroy(struct linked_list *list);리스트를 다 사용하고 난 뒤에는 제거합니다.각각의 함수의 자세한 동작은 뒤에 설명되어 있습니다....