source: vis_dev/zchaff/sat_solver.cpp @ 77

Last change on this file since 77 was 10, checked in by cecile, 13 years ago

Zchaff

File size: 11.2 KB
Line 
1/* =========FOR INTERNAL USE ONLY. NO DISTRIBUTION PLEASE ========== */
2
3/*********************************************************************
4 Copyright 2000-2004, Princeton University.  All rights reserved.
5 By using this software the USER indicates that he or she has read,
6 understood and will comply with the following:
7
8 --- Princeton University hereby grants USER nonexclusive permission
9 to use, copy and/or modify this software for internal, noncommercial,
10 research purposes only. Any distribution, including commercial sale
11 or license, of this software, copies of the software, its associated
12 documentation and/or modifications of either is strictly prohibited
13 without the prior consent of Princeton University.  Title to copyright
14 to this software and its associated documentation shall at all times
15 remain with Princeton University.  Appropriate copyright notice shall
16 be placed on all software copies, and a complete copy of this notice
17 shall be included in all copies of the associated documentation. 
18 No right is  granted to use in advertising, publicity or otherwise
19 any trademark,  service mark, or the name of Princeton University.
20
21
22 --- This software and any associated documentation is provided "as is"
23
24 PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
25 OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
26 PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR
27 ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
28 TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. 
29
30 Princeton University shall not be liable under any circumstances for
31 any direct, indirect, special, incidental, or consequential damages
32 with respect to any claim by USER or any third party on account of
33 or arising from the use, or inability to use, this software or its
34 associated documentation, even if Princeton University has been advised
35 of the possibility of those damages.
36*********************************************************************/
37#include <iostream>
38#include <fstream>
39#include <cstdlib>
40#include <cstdio>
41#include <cstring>
42
43#include <set>
44#include <vector>
45#include <dirent.h>
46#include "SAT.h"
47
48using namespace std;
49
50const int MAX_LINE_LENGTH       = 65536;
51const int MAX_WORD_LENGTH       = 64;
52
53//This cnf parser function is based on the GRASP code by Joao Marques Silva
54void read_cnf(SAT_Manager mng, char * filename )
55{
56//    cout <<"read cnf "<<endl;
57    char line_buffer[MAX_LINE_LENGTH];
58    char word_buffer[MAX_WORD_LENGTH];
59    set<int> clause_vars;
60    set<int> clause_lits;
61    int line_num = 0;
62   
63    if(opendir(filename)){
64        cerr << "Can't open input file, it's a directory" << endl;
65        exit(1);
66    }
67   
68    ifstream inp (filename, ios::in);
69    if (!inp) {
70        cerr << "Can't open input file" << endl;
71        exit(1);
72    }
73    while (inp.getline(line_buffer, MAX_LINE_LENGTH)) {
74        ++ line_num;
75        if (line_buffer[0] == 'c') { 
76            continue; 
77        }
78        else if (line_buffer[0] == 'p') {
79            int var_num;
80            int cl_num;
81
82            int arg = sscanf (line_buffer, "p cnf %d %d", &var_num, &cl_num);
83            if( arg < 2 ) {
84                cerr << "Unable to read number of variables and clauses"
85                     << "at line " << line_num << endl;
86                exit(3);
87            }
88            SAT_SetNumVariables(mng, var_num); //first element not used.
89        }
90        else {                             // Clause definition or continuation
91            char *lp = line_buffer;
92            do {
93                char *wp = word_buffer;
94                while (*lp && ((*lp == ' ') || (*lp == '\t'))) {
95                    lp++;
96                }
97                while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n')) {
98                    *(wp++) = *(lp++);
99                }
100                *wp = '\0';                                 // terminate string
101
102                if (strlen(word_buffer) != 0) {     // check if number is there
103                    int var_idx = atoi (word_buffer);
104                    int sign = 0;
105
106                    if( var_idx != 0) {
107                        if( var_idx < 0)  { var_idx = -var_idx; sign = 1; }
108                        clause_vars.insert(var_idx);
109                        clause_lits.insert( (var_idx << 1) + sign);
110                    }         
111                    else {
112                        //add this clause
113                        if (clause_vars.size() != 0 && (clause_vars.size() == clause_lits.size())) { //yeah, can add this clause
114                            vector <int> temp;
115                            for (set<int>::iterator itr = clause_lits.begin();
116                                 itr != clause_lits.end(); ++itr)
117                                temp.push_back (*itr);
118                            SAT_AddClause(mng, & temp.begin()[0], temp.size() );
119                        }
120                        else {} //it contain var of both polarity, so is automatically satisfied, just skip it
121                        clause_lits.clear();
122                        clause_vars.clear();
123                    }
124                }
125            }
126            while (*lp);
127        }
128    }
129    if (!inp.eof()) {
130        cerr << "Input line " << line_num <<  " too long. Unable to continue..." << endl;
131        exit(2);
132    }
133//    assert (clause_vars.size() == 0);         //some benchmark has no 0 in the last clause
134    if (clause_lits.size() && clause_vars.size()==clause_lits.size() ) {
135        vector <int> temp;
136        for (set<int>::iterator itr = clause_lits.begin();
137             itr != clause_lits.end(); ++itr)
138            temp.push_back (*itr);
139        SAT_AddClause(mng, & temp.begin()[0], temp.size() );
140    }
141    clause_lits.clear();
142    clause_vars.clear();
143//    cout <<"done read cnf"<<endl;
144}
145
146
147void handle_result(SAT_Manager mng, int outcome, char * filename )
148{
149    string result = "UNKNOWN";
150    switch (outcome) {
151    case SATISFIABLE:
152        cout << "Instance Satisfiable" << endl;
153//following lines will print out a solution if a solution exist
154        for (int i=1, sz = SAT_NumVariables(mng); i<= sz; ++i) {
155            switch(SAT_GetVarAsgnment(mng, i)) {
156            case -1:       
157                cout <<"("<< i<<")"; break;
158            case 0:
159                cout << "-" << i; break;
160            case 1:
161                cout << i ; break;
162            default:
163                cerr << "Unknown variable value state"<< endl;
164                exit(4);
165            }
166            cout << " ";
167        }
168        result  = "SAT";
169        break;
170    case UNSATISFIABLE:
171        result  = "UNSAT";
172        cout << "Instance Unsatisfiable" << endl;
173        break; 
174    case TIME_OUT:
175        result  = "ABORT : TIME OUT"; 
176        cout << "Time out, unable to determine the satisfiability of the instance"<<endl;
177        break;
178    case MEM_OUT:
179        result  = "ABORT : MEM OUT"; 
180        cout << "Memory out, unable to determine the satisfiability of the instance"<<endl;
181        break;
182    default:
183        cerr << "Unknown outcome" << endl;
184    }
185    cout << "Random Seed Used\t\t\t\t" << SAT_Random_Seed(mng) << endl;
186    cout << "Max Decision Level\t\t\t\t" << SAT_MaxDLevel(mng) << endl;
187    cout << "Num. of Decisions\t\t\t\t" << SAT_NumDecisions(mng)<< endl;
188    cout << "( Stack + Vsids + Shrinking Decisions )\t\t" <<SAT_NumDecisionsStackConf(mng);
189    cout << " + " <<SAT_NumDecisionsVsids(mng)<<" + "<<SAT_NumDecisionsShrinking(mng)<<endl;
190    cout << "Original Num Variables\t\t\t\t" << SAT_NumVariables(mng) << endl;
191    cout << "Original Num Clauses\t\t\t\t" << SAT_InitNumClauses(mng) << endl;
192    cout << "Original Num Literals\t\t\t\t" << SAT_InitNumLiterals(mng) << endl;
193    cout << "Added Conflict Clauses\t\t\t\t" << SAT_NumAddedClauses(mng)- SAT_InitNumClauses(mng)<< endl;
194    cout << "Num of Shrinkings\t\t\t\t" << SAT_NumShrinkings(mng)<< endl;
195    cout << "Deleted Conflict Clauses\t\t\t" << SAT_NumDeletedClauses(mng)-SAT_NumDelOrigCls(mng) <<endl;
196    cout << "Deleted Clauses\t\t\t\t\t" << SAT_NumDeletedClauses(mng) <<endl;
197    cout << "Added Conflict Literals\t\t\t\t" << SAT_NumAddedLiterals(mng) - SAT_InitNumLiterals(mng) << endl;
198    cout << "Deleted (Total) Literals\t\t\t" << SAT_NumDeletedLiterals(mng) <<endl;
199    cout << "Number of Implication\t\t\t\t" << SAT_NumImplications(mng)<< endl;
200    //other statistics comes here
201    cout << "Total Run Time\t\t\t\t\t" << SAT_GetCPUTime(mng) << endl;
202//    cout << "RESULT:\t" << filename << " " << result << " RunTime: " << SAT_GetCPUTime(mng)<< endl;
203    cout  << "RESULT:\t"<<result << endl;
204
205
206}
207
208void output_status(SAT_Manager mng)
209{
210    cout << "Dec: " << SAT_NumDecisions(mng)<< "\t ";
211    cout << "AddCl: " << SAT_NumAddedClauses(mng) <<"\t";
212    cout << "AddLit: " << SAT_NumAddedLiterals(mng)<<"\t";
213    cout << "DelCl: " << SAT_NumDeletedClauses(mng) <<"\t";
214    cout << "DelLit: " << SAT_NumDeletedLiterals(mng)<<"\t";
215    cout << "NumImp: " << SAT_NumImplications(mng) <<"\t";
216    cout << "AveBubbleMove: " << SAT_AverageBubbleMove(mng) <<"\t";
217    //other statistics comes here
218    cout << "RunTime:" << SAT_GetElapsedCPUTime(mng) << endl;
219}
220
221void verify_solution(SAT_Manager mng)
222{
223    int num_verified = 0;
224    for ( int cl_idx = SAT_GetFirstClause (mng); cl_idx >= 0; 
225          cl_idx = SAT_GetNextClause(mng, cl_idx)) {
226        int len = SAT_GetClauseNumLits(mng, cl_idx);
227        int * lits = new int[len+1];
228        SAT_GetClauseLits( mng, cl_idx, lits);
229        int i;
230        for (i=0; i< len; ++i) {
231            int v_idx = lits[i] >> 1;
232            int sign = lits[i] & 0x1;
233            int var_value = SAT_GetVarAsgnment( mng, v_idx);
234            if( (var_value == 1 && sign == 0) ||
235                (var_value == 0 && sign == 1) ) break;
236        }
237        if (i >= len) {
238            cerr << "Verify Satisfiable solution failed, please file a bug report, thanks. " << endl;
239            exit(6);
240        }
241        delete [] lits;
242        ++ num_verified;
243    }
244    cout <<"c "<< num_verified << " Clauses are true, Verify Solution successful."<<endl;;
245}
246
247int main(int argc, char ** argv)
248{
249    SAT_Manager mng = SAT_InitManager();
250    if (argc < 2) {
251        cerr << "Z-Chaff: Accelerated SAT Solver from Princeton. " << endl;
252        cerr << "Copyright 2000-2004, Princeton University." << endl << endl;;
253        cerr << "Usage: "<< argv[0] << " cnf_file [time_limit]" << endl;
254        return 2;
255    }
256    cout << "Z-Chaff Version: " << SAT_Version(mng) << endl;
257    cout << "Solving " << argv[1] << " ......" << endl;
258    if (argc == 2) {
259        read_cnf (mng, argv[1] );
260    }
261    else {
262        read_cnf (mng, argv[1] );
263        SAT_SetTimeLimit(mng, atoi(argv[2]));
264    }
265
266/* if you want some statistics during the solving, uncomment following line */
267//    SAT_AddHookFun(mng,output_status, 5000);
268
269/* you can set all your parameters here, following values are the defaults*/ 
270//    SAT_SetMaxUnrelevance(mng, 20);
271//    SAT_SetMinClsLenForDelete(mng, 100);
272//    SAT_SetMaxConfClsLenAllowed(mng, 5000);
273
274/* randomness may help sometimes, by default, there is no randomness */
275//    SAT_SetRandomness (mng, 10);
276//    SAT_SetRandSeed (mng, -1);
277    int result = SAT_Solve(mng);
278    if (result == SATISFIABLE) 
279        verify_solution(mng);
280    handle_result (mng, result,  argv[1]);
281    return 0;
282}
Note: See TracBrowser for help on using the repository browser.