1 // *********************************************************************
2 // Copyright 2000-2004, Princeton University. All rights reserved.
3 // By using this software the USER indicates that he or she has read,
4 // understood and will comply with the following:
6 // --- Princeton University hereby grants USER nonexclusive permission
7 // to use, copy and/or modify this software for internal, noncommercial,
8 // research purposes only. Any distribution, including commercial sale
9 // or license, of this software, copies of the software, its associated
10 // documentation and/or modifications of either is strictly prohibited
11 // without the prior consent of Princeton University. Title to copyright
12 // to this software and its associated documentation shall at all times
13 // remain with Princeton University. Appropriate copyright notice shall
14 // be placed on all software copies, and a complete copy of this notice
15 // shall be included in all copies of the associated documentation.
16 // No right is granted to use in advertising, publicity or otherwise
17 // any trademark, service mark, or the name of Princeton University.
20 // --- This software and any associated documentation is provided "as is"
22 // PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
23 // OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
24 // PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR
25 // ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
26 // TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
28 // Princeton University shall not be liable under any circumstances for
29 // any direct, indirect, special, incidental, or consequential damages
30 // with respect to any claim by USER or any third party on account of
31 // or arising from the use, or inability to use, this software or its
32 // associated documentation, even if Princeton University has been advised
33 // of the possibility of those damages.
34 // *********************************************************************
37 #include <sys/resource.h>
46 const int WORD_LEN = 64000;
48 const int MEM_LIMIT = 800000;
50 const int UNKNOWN = 2;
55 double get_cpu_time(void) {
58 getrusage(RUSAGE_SELF, &usage);
59 res = usage.ru_utime.tv_usec + usage.ru_stime.tv_usec;
61 res += usage.ru_utime.tv_sec + usage.ru_stime.tv_sec;
65 void get_line(ifstream* fs, vector<char>* buf) {
70 if (ch == '\n' || ch == '\377')
80 int get_token(char * & lp, char * token) {
82 while (*lp && ((*lp == ' ') || (*lp == '\t'))) {
85 while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n')) {
88 *wp = '\0'; // terminate string
92 int get_mem_usage(void) {
99 snprintf(filename, sizeof(filename), "/proc/%i/status", pid);
100 if ((fp = fopen(filename, "r")) == NULL) {
101 cerr << "Can't open Proc file, are you sure you are using Linux?" << endl;
105 fgets(buffer, 128, fp);
107 get_token(ptr, token);
108 if (strcmp(token, "VmSize:") == 0) {
109 get_token(ptr, token);
114 cerr << "Error in get memeory usage" << endl;
119 int my_a2i(char * str) {
126 else if (str[0] == '+')
128 for (unsigned i = 0; i < strlen(str); ++i) {
129 int d = str[i] - '0';
130 if (d < 0 || d > 9) {
131 cerr << "Abort: Unable to change " << str << " into a number " << endl;
134 result = result * 10 + d;
143 vector<int> literals;
144 vector<int> resolvents;
145 bool is_involved : 1;
160 short in_clause_phase :4;
168 in_clause_phase = UNKNOWN;
169 num_lits[0] = num_lits[1] = 0;
175 struct cmp_var_level {
176 bool operator() (CVariable * v1, CVariable * v2) {
177 if (v1->level > v2->level)
179 else if (v1->level < v2->level)
189 int _current_num_clauses;
190 int _num_init_clauses;
191 vector<CVariable> _variables;
192 vector<CClause> _clauses;
194 vector<int> _conf_clause;
198 _num_init_clauses = 0;
199 _current_num_clauses = 0;
203 int & num_init_clauses(void) {
204 return _num_init_clauses;
207 vector<CVariable> & variables(void) {
211 vector<CClause> & clauses(void) {
215 void read_cnf(char * filename);
216 bool verify(char * filename);
217 bool real_verify(void);
218 int lit_value(int svar) {
219 assert(_variables[svar>>1].value != UNKNOWN);
220 return _variables[svar>>1].value ^ (svar & 0x1);
222 int add_orig_clause_by_lits(vector<int> lits);
223 int add_learned_clause_by_resolvents(vector<int> & resolvents);
224 void set_var_number(int nvar);
225 void set_init_cls_number(int n) {
226 _num_init_clauses = n;
228 void construct_learned_clauses(void);
229 void recursive_construct_clause(int cl_id);
230 void recursive_find_involved(int cl_id);
231 int recursive_find_level(int vid);
235 void CDatabase::dump(void) {
236 cout << "p cnf " << _variables.size() - 1 << " " << _num_init_clauses << endl;
237 for (unsigned i = 0; i < _clauses.size(); ++i) {
238 for (unsigned j = 0; j < _clauses[i].literals.size(); ++j) {
239 int lit = _clauses[i].literals[j];
240 cout << ((lit & 0x1) ? "-" : "") << (lit >> 1) << " ";
246 void CDatabase::set_var_number(int nvar) {
247 _variables.resize(nvar + 1);
248 for (unsigned i = 0; i < _variables.size(); ++i) {
249 _variables[i].value = UNKNOWN;
250 _variables[i].in_clause_phase = UNKNOWN;
254 void check_mem_out(void) {
255 int mem = get_mem_usage();
256 if (mem > MEM_LIMIT) {
257 cerr << "Mem out" << endl;
264 int CDatabase::add_orig_clause_by_lits(vector<int> lits) {
265 static int line_n = 0;
267 if (lits.size() == 0) {
268 cerr << "Empty Clause Encountered " << endl;
271 int cls_id = _clauses.size();
272 _clauses.resize(_clauses.size() + 1);
273 vector<int> temp_cls;
274 for (unsigned i = 0; i < lits.size(); ++i) {
281 if (vid == 0 || vid > (int) _variables.size() - 1) {
282 cerr << "Variable index out of range " << endl;
285 if (_variables[vid].in_clause_phase == UNKNOWN) {
286 _variables[vid].in_clause_phase = phase;
287 temp_cls.push_back(vid + vid + phase);
288 // _clauses[cls_id].my_literals.push_back(vid + vid + phase);
289 ++_variables[vid].num_lits[phase];
291 else if (_variables[vid].in_clause_phase != phase) {
292 cerr << "clause " << line_n << endl;
293 cerr << "A clause contain both literal and its negate " << endl;
297 _clauses[cls_id].literals.resize(temp_cls.size());
298 for (unsigned i = 0; i< temp_cls.size(); ++i) {
299 _clauses[cls_id].literals[i]= temp_cls[i];
301 _clauses[cls_id].is_built = true;
302 // _clauses[cls_id].my_is_built = true;
303 for (unsigned i = 0; i< lits.size(); ++i) {
305 if (vid < 0) vid = -vid;
306 _variables[vid].in_clause_phase = UNKNOWN;
308 ++_current_num_clauses;
309 if (_current_num_clauses%10 == 0)
314 int CDatabase::add_learned_clause_by_resolvents(vector<int> & resolvents) {
315 int cls_id = _clauses.size();
316 _clauses.resize(_clauses.size() + 1);
317 _clauses[cls_id].resolvents.resize(resolvents.size());
318 for (unsigned i = 0; i< resolvents.size(); ++i)
319 _clauses[cls_id].resolvents[i] = resolvents[i];
320 _clauses[cls_id].is_built = false;
324 void CDatabase::read_cnf(char * filename) {
325 cout << "Read in original clauses ... ";
326 ifstream in_file(filename);
328 cerr << "Can't open input CNF file " << filename << endl;
332 vector<int> literals;
333 bool header_encountered = false;
334 char token[WORD_LEN];
335 while (!in_file.eof()) {
336 get_line(&in_file, &buffer);
337 char * ptr = &(*buffer.begin());
338 if (get_token(ptr, token)) {
339 if (strcmp(token, "c") == 0)
341 else if (strcmp(token, "p") == 0) {
342 get_token(ptr, token);
343 if (strcmp(token, "cnf") != 0) {
344 cerr << "Format Error, p cnf NumVar NumCls " << endl;
347 get_token(ptr, token);
348 int nvar = my_a2i(token);
349 set_var_number(nvar);
350 get_token(ptr, token);
351 int ncls = my_a2i(token);
352 set_init_cls_number(ncls);
353 header_encountered = true;
356 int lit = my_a2i(token);
358 literals.push_back(lit);
360 add_orig_clause_by_lits(literals);
365 while (get_token(ptr, token)) {
366 int lit = my_a2i(token);
368 literals.push_back(lit);
370 add_orig_clause_by_lits(literals);
375 if (!literals.empty()) {
376 cerr << "Trailing numbers without termination " << endl;
379 if (clauses().size() != (unsigned)num_init_clauses())
380 cerr << "WARNING : Clause count inconsistant with the header " << endl;
381 cout << num_init_clauses() << " Clauses " << endl;
384 void CDatabase::recursive_find_involved(int cl_id) {
385 if (_clauses[cl_id].is_involved == true)
387 _clauses[cl_id].is_involved = true;
389 recursive_construct_clause(cl_id);
392 for (unsigned i = 0; i < _clauses[cl_id].literals.size(); ++i) {
393 int lit = _clauses[cl_id].literals[i];
395 int sign = (lit & 0x1);
396 assert(_variables[vid].value != UNKNOWN);
397 if ((_variables[vid].value == 1 && sign == 0) ||
398 (_variables[vid].value == 0 && sign == 1)) {
402 cerr << "Clause " << cl_id << " has more than one value 1 literals "
406 } else { // literal value 0, so seek its antecedent
407 int ante = _variables[vid].antecedent;
408 recursive_find_involved(ante);
413 void CDatabase::recursive_construct_clause(int cl_id) {
414 CClause & cl = _clauses[cl_id];
415 if (cl.is_built == true)
418 assert(cl.resolvents.size() > 1);
420 // I have to construct them first because of recursion may
421 // mess up with the in_clause_signs.
422 for (unsigned i = 0; i < cl.resolvents.size(); ++i) {
423 _clauses[cl.resolvents[i]].is_needed = true;
424 recursive_construct_clause(cl.resolvents[i]);
427 // cout << "Constructing clause " << cl_id << endl;
428 vector<int> literals;
431 int cl1 = cl.resolvents[0];
432 assert(_clauses[cl1].is_built);
433 for (unsigned i = 0; i < _clauses[cl1].literals.size(); ++i) {
434 int lit = _clauses[cl1].literals[i];
435 int vid = (lit >> 0x1);
436 int sign = (lit & 0x1);
437 assert(_variables[vid].in_clause_phase == UNKNOWN);
438 _variables[vid].in_clause_phase = sign;
439 literals.push_back(lit);
442 for (unsigned i = 1; i < cl.resolvents.size(); ++i) {
444 int cl1 = cl.resolvents[i];
445 assert(_clauses[cl1].is_built);
446 for (unsigned j = 0; j < _clauses[cl1].literals.size(); ++j) {
447 int lit = _clauses[cl1].literals[j];
448 int vid = (lit >> 0x1);
449 int sign = (lit & 0x1);
450 if (_variables[vid].in_clause_phase == UNKNOWN) {
451 _variables[vid].in_clause_phase = sign;
452 literals.push_back(lit);
454 else if (_variables[vid].in_clause_phase != sign) {
455 // distance 1 literal
457 _variables[vid].in_clause_phase = UNKNOWN;
461 cerr << "Resolve between two clauses with distance larger than 1" << endl;
462 cerr << "The resulting clause is " << cl_id << endl;
463 cerr << "Starting clause is " << cl.resolvents[0] << endl;
464 cerr << "One of the clause involved is " << cl1 << endl;
468 vector<int> temp_cls;
469 for (unsigned i = 0; i < literals.size(); ++i) {
470 int lit = literals[i];
471 int vid = (lit >> 0x1);
472 int sign = (lit & 0x1);
473 if (_variables[vid].in_clause_phase == UNKNOWN)
475 assert(_variables[vid].in_clause_phase == sign);
476 _variables[vid].in_clause_phase = UNKNOWN;
477 temp_cls.push_back(lit);
479 cl.literals.resize(temp_cls.size());
480 for (unsigned i = 0; i < temp_cls.size(); ++i)
481 cl.literals[i] = temp_cls[i];
483 // ::sort(cl.literals.begin(), cl.literals.end());
484 // assert(cl.literals.size()== cl.my_literals.size());
485 // for (unsigned i=0; i< cl.literals.size(); ++i)
486 // assert(cl.literals[i] == cl.my_literals[i]);
488 ++_current_num_clauses;
489 if (_current_num_clauses%10 == 0)
493 int CDatabase::recursive_find_level(int vid) {
494 int ante = _variables[vid].antecedent;
495 assert(_variables[vid].value != UNKNOWN);
496 assert(_variables[vid].antecedent != -1);
497 assert(_clauses[ante].is_involved);
498 if (_variables[vid].level != -1)
499 return _variables[vid].level;
501 for (unsigned i = 0; i <_clauses[ante].literals.size(); ++i) {
502 int v = (_clauses[ante].literals[i] >> 1);
503 int s = (_clauses[ante].literals[i] & 0x1);
505 assert(_variables[v].value != s);
508 assert(_variables[v].value == s);
509 int l = recursive_find_level(v);
514 _variables[vid].level = level + 1;
518 bool CDatabase::real_verify(void) {
519 // 1. If a variable is assigned value at dlevel 0,
520 // either it's pure or it has an antecedent
521 for (unsigned i = 1; i < _variables.size(); ++i) {
522 if (_variables[i].value != UNKNOWN && _variables[i].antecedent == -1) {
523 if ((_variables[i].num_lits[0] == 0 && _variables[i].value == 0) ||
524 (_variables[i].num_lits[1] == 0 && _variables[i].value == 1)) {
525 // cout << "Variable " << i << " is assigned " << _variables[i].value
526 // << " because it is pure literal. " << endl;
528 cerr << "Don't know why variable " << i << " is assigned "
529 << _variables[i].value << " for no reasons" << endl;
534 // 2. Construct the final conflicting clause if needed and find all
535 // the clauses that are involved in making it conflicting
536 cout << "Begin constructing all involved clauses " << endl;
537 _clauses[_conf_id].is_needed = true;
538 recursive_find_involved(_conf_id);
540 for (unsigned i = num_init_clauses(); i< _clauses.size(); ++i)
541 if (_clauses[i].is_built)
543 cout << "Num. Learned Clause:\t\t\t" << _clauses.size() - num_init_clauses()
545 << "Num. Clause Built:\t\t\t" << count << endl
546 << "Constructed all involved clauses " << endl;
548 // 2.5. Verify the literals in the CONF clause
549 // comments this out if it gives error because you give the wrong
550 // CONF clause literals.
551 assert(_clauses[_conf_id].is_built);
552 assert(_clauses[_conf_id].is_involved);
554 for (unsigned i = 0; i <_conf_clause.size(); ++i) {
556 for (unsigned j = 0; j <_clauses[_conf_id].literals.size(); ++j) {
557 if (_conf_clause[i] == _clauses[_conf_id].literals[j]) {
563 cerr << "The conflict clause in trace can't be verified! " << endl;
564 cerr << "Literal " << _conf_clause[i] << " is not found." << endl;
567 cout << "Conflict clause verification finished." << endl;
569 // 3. Levelize the variables that are decided at dlevel 0
570 cout << "Levelize variables...";
571 for (unsigned i = 1; i < _variables.size(); ++i) {
572 int cl_id = _variables[i].antecedent;
573 if (_variables[i].value != UNKNOWN && cl_id != -1) {
574 if (_clauses[cl_id].is_involved) {
575 int level = recursive_find_level(i);
576 // cout << "Var: " << i << " level " << level << endl;
580 cout << "finished"<< endl;
581 // 4. Can we construct an empty clause?
582 cout << "Begin Resolution..." ;
583 set<CVariable *, cmp_var_level> clause_lits;
584 for (unsigned i = 0; i< _clauses[_conf_id].literals.size(); ++i) {
585 assert(lit_value(_clauses[_conf_id].literals[i]) == 0);
586 int vid = (_clauses[_conf_id].literals[i] >> 1);
587 clause_lits.insert(&_variables[vid]);
589 assert(clause_lits.size() == _clauses[_conf_id].literals.size());
591 while (!clause_lits.empty()) {
592 // for (set<CVariable *, cmp_var_level>::iterator itr = clause_lits.begin();
593 // itr != clause_lits.end(); ++itr) {
594 // int vid = (*itr) - &_variables[0];
595 // cout << vid << "(" << (*itr)->level << ") ";
599 int vid = (*clause_lits.begin() - &_variables[0]);
600 int ante = _variables[vid].antecedent;
602 cerr << "Variable " << vid << " has an NULL antecedent ";
605 _clauses[ante].is_needed = true;
606 clause_lits.erase(clause_lits.begin());
607 _variables[vid].in_clause_phase = 1;
608 CClause & cl = _clauses[ante];
610 for (unsigned i = 0; i< cl.literals.size(); ++i) {
611 int l = cl.literals[i];
613 assert(_variables[v].value != UNKNOWN);
614 if (lit_value(l) == 1) {
616 cerr << "The antecedent of the variable is not really an antecedent "
624 clause_lits.insert(&_variables[v]);
626 assert(distance == 1);
628 cout << " Empty clause generated." << endl;
629 cout << "Mem Usage :\t\t\t\t" << get_mem_usage()<< endl;
630 int needed_cls_count = 0;
631 int needed_var_count = 0;
632 for (int i = 0; i < num_init_clauses(); ++i) {
633 if (_clauses[i].is_needed == true) {
635 for (unsigned j = 0; j < _clauses[i].literals.size(); ++j) {
636 int vid = (_clauses[i].literals[j] >> 1);
637 if (_variables[vid].is_needed == false) {
639 _variables[vid].is_needed = true;
644 cout << "Original Num. Clauses:\t\t\t" << num_init_clauses() << endl;
645 cout << "Needed Clauses to Construct Empty:\t"<< needed_cls_count << endl;
646 cout << "Total Variable count:\t\t\t" << _variables.size()-1 << endl;
647 cout << "Variables involved in Empty:\t\t" << needed_var_count << endl;
649 for (unsigned i = 0; i< _clauses.size(); ++i) {
650 if (_clauses[i].is_built)
651 assert(_clauses[i].is_needed || i < (unsigned)num_init_clauses());
653 if (_dump_core == true) {
654 cout << "Unsat Core dumped:\t\t\tunsat_core.cnf" << endl;
655 ofstream dump("unsat_core.cnf");
656 dump << "c Variables Not Involved: ";
658 for (unsigned i = 1; i < _variables.size(); ++i) {
659 if (_variables[i].is_needed == false) {
661 dump << endl << "c ";
667 dump << "p cnf " << _variables.size()-1 << " " << needed_cls_count << endl;
668 for (int i = 0; i < num_init_clauses(); ++i) {
669 if (_clauses[i].is_needed) {
670 dump << "c Original Cls ID: " << i << endl;
671 for (unsigned j = 0; j < _clauses[i].literals.size(); ++j) {
672 dump << ((_clauses[i].literals[j] & 0x1)?" -":" ")
673 << (_clauses[i].literals[j] >> 1);
675 dump << " 0" << endl;
682 bool CDatabase::verify(char * filename) {
684 char token[WORD_LEN];
686 ifstream in_file(filename);
688 cerr << "Can't open input CNF file " << filename << endl;
692 while (!in_file.eof()) {
693 get_line(&in_file, &buffer);
694 char * ptr = &(*buffer.begin());
695 get_token(ptr, token);
696 if (strcmp(token, "CL:") == 0) {
697 vector<int> resolvents;
699 get_token(ptr, token);
700 int cl_id = my_a2i(token);
702 get_token(ptr, token);
703 assert(strcmp(token, "<=") == 0);
705 while (get_token(ptr, token)) {
706 int r = my_a2i(token);
707 resolvents.push_back(r);
709 int c = add_learned_clause_by_resolvents(resolvents);
712 else if (strcmp(token, "VAR:") == 0) {
713 get_token(ptr, token);
714 int vid = my_a2i(token);
716 get_token(ptr, token);
717 assert(strcmp(token, "L:") == 0);
718 get_token(ptr, token); // skip the level
720 get_token(ptr, token);
721 assert(strcmp(token, "V:") == 0);
722 get_token(ptr, token);
723 int value = my_a2i(token);
724 assert(value == 1 || value == 0);
726 get_token(ptr, token);
727 assert(strcmp(token, "A:") == 0);
728 get_token(ptr, token);
729 int ante = my_a2i(token);
731 get_token(ptr, token);
732 assert(strcmp(token, "Lits:") == 0);
734 _variables[vid].value = value;
735 _variables[vid].antecedent = ante;
737 else if (strcmp(token, "CONF:") == 0) {
738 get_token(ptr, token);
739 _conf_id = my_a2i(token);
741 get_token(ptr, token);
742 assert(strcmp(token, "==") == 0);
744 while (get_token(ptr, token)) {
745 int lit = my_a2i(token);
747 assert((lit>>1) < (int)_variables.size());
748 _conf_clause.push_back(lit);
752 if (_conf_id == -1) {
753 cerr << "No final conflicting clause defined " << endl;
756 cout << "Mem Usage After Readin file:\t\t" << get_mem_usage() << endl;
757 return real_verify();
760 int main(int argc, char** argv) {
761 cout << "ZVerify SAT Solver Verifier" << endl;
762 cout << "Copyright Princeton University, 2003-2004. All Right Reseverd."
764 if (argc != 3 && argc !=4) {
765 cerr << "Usage: " << argv[0] << " CNF_File Dump_File [-core]" << endl
766 << "-core: dump the unsat core " << endl;
774 if (strcmp(argv[3], "-core") != 0) {
775 cerr << "Must use -core as the third parameter" << endl;
780 cout << "COMMAND LINE: ";
781 for (int i = 0; i < argc; ++i)
782 cout << argv[i] << " ";
785 _peak_mem = get_mem_usage();
787 double begin_time = get_cpu_time();
788 dbase.read_cnf(argv[1]);
789 if (dbase.verify(argv[2]) == true) {
790 double end_time = get_cpu_time();
791 cout << "CPU Time:\t\t\t\t" << end_time - begin_time << endl;
792 cout << "Peak Mem Usage:\t\t\t\t" << _peak_mem << endl;
793 cout << "Verification Successful " << endl;
795 cout << "Failed to verify the result " << endl;