simpsolver.c

多核环境下运行了可满足性分析的工具软件

    for (int i = 0; i < c.size(); i++)
      if (var(c[i]) != v && value(c[i]) != l_False)
	uncheckedEnqueue(~c[i]);
      else
	l = c[i];
    
    if (propagate() != NULL){
      cancelUntil(0);
      asymm_lits++;
      if (!strengthenClause(c, l))
	return false;
    }else
      cancelUntil(0);
    
    return true;
  }
  

  bool SimpSolver::asymmVar(Var v)
  {
    assert(!frozen[v]);
    assert(use_simplification);
    
    vec<Clause*>  pos, neg;
    const vec<Clause*>& cls = getOccurs(v);
    
    if (value(v) != l_Undef || cls.size() == 0)
      return true;
    
    for (int i = 0; i < cls.size(); i++)
      if (!asymm(v, *cls[i]))
	return false;
    
    return backwardSubsumptionCheck();
  }

  void SaveError(char* CNFFile)
  { 		
    printf("\n\n  MiniSat2 Preprocessor: Verify Solution Error \n\n");
    FILE* error = fopen("error.txt","a");
    fprintf(error," %s - MiniSat2 Preprocessor: Verify Solution Error \n",CNFFile);
    fclose(error); 
  }
  
  void SimpSolver::verifyModel(int* Belegung, char* CNFFile)
  {
    bool failed = false;
    int  cnt    = 0;
    
    // NOTE: elimtable.size() might be lower than nVars() at the moment
    
    for (int i = 0; i < elimtable.size(); i++)
      if (elimtable[i].order > 0)
	for (int j = 0; j < elimtable[i].eliminated.size(); j++){
	  cnt++;
	  Clause& c = *elimtable[i].eliminated[j];
	  for (int k = 0; k < c.size(); k++){
	    if(value(c[k])!=l_Undef) {
	      if(value(var(c[k]))==l_True) Belegung[var(c[k])+1]=((var(c[k])+1)<< 1);
	      if(value(var(c[k]))==l_False) Belegung[var(c[k])+1]=((var(c[k])+1)<< 1)+1;
	    }
	    if ((((Belegung[var(c[k])+1])& 1) ^ sign(c[k]))==0)
	      goto next;
	  }
	  
	  SaveError(CNFFile);

	  failed = true;
	next:;
	}
  }
 
  bool SimpSolver::eliminateVar(Var v, bool fail)
  {
    if (!fail && asymm_mode && !asymmVar(v))    return false;
    
    const vec<Clause*>& cls = getOccurs(v);
    
    if (value(v) != l_Undef) return true;

    // Split the occurrences into positive and negative:  Menge der Klauseln in der v 
    // positiv und Menge in der v negativ vorkommt
    vec<Clause*>  pos, neg;
    for (int i = 0; i < cls.size(); i++)
      (find(*cls[i], Lit(v)) ? pos : neg).push(cls[i]);
    
    // Check if number of clauses decreases:
    int cnt = 0;
    for (int i = 0; i < pos.size(); i++)
      for (int j = 0; j < neg.size(); j++)
	if (merge(*pos[i], *neg[j], v) && ++cnt > cls.size() + grow) 
	  return true;
    
    // Delete and store old clauses:
    setDecisionVar(v, false); 
    elimtable[v].order = elimorder++;
    assert(elimtable[v].eliminated.size() == 0);
    for (int i = 0; i < cls.size(); i++){
      elimtable[v].eliminated.push(Clause_new(*cls[i]));
      removeClause(*cls[i]); }
    
    // Produce clauses in cross product:
    int top = clauses.size();
    vec<Lit> resolvent;
    for (int i = 0; i < pos.size(); i++)
      for (int j = 0; j < neg.size(); j++)
	if (merge(*pos[i], *neg[j], v, resolvent) && !addClause(resolvent))
	  return false;
    
    // DEBUG: For checking that a clause set is saturated (gesätigt) with respect to variable elimination.
    //        If the clause set is expected to be saturated at this point, this constitutes an
    //        error.
    if (fail){
      reportf("eliminated var %d, %d <= %d\n", v+1, cnt, cls.size());
      reportf("previous clauses:\n");
      for (int i = 0; i < cls.size(); i++){
	printClause(*cls[i]); reportf("\n"); }
      reportf("new clauses:\n");
      for (int i = top; i < clauses.size(); i++){
	printClause(*clauses[i]); reportf("\n"); }
      assert(0); }
    
    return backwardSubsumptionCheck();
  }


  void SimpSolver::remember(Var v)
  {
    assert(decisionLevel() == 0);
    assert(isEliminated(v));
    
    vec<Lit> clause;
    
    // Re-activate variable:
    elimtable[v].order = 0;
    setDecisionVar(v, true); 

    if (use_simplification)
      updateElimHeap(v);

    // Reintroduce all old clauses which may implicitly remember other clauses:
    for (int i = 0; i < elimtable[v].eliminated.size(); i++){
      Clause& c = *elimtable[v].eliminated[i];
      clause.clear();
      for (int j = 0; j < c.size(); j++)
	clause.push(c[j]);
      
      remembered_clauses++;
      check(addClause(clause));
      free(&c);
    }
    
    elimtable[v].eliminated.clear();
  }
  
  void SimpSolver::extendModel(int* Belegung)
  {
    vec<Var> vs;
    
    // NOTE: elimtable.size() might be lower than nVars() at the moment

    for (int v = 0; v < elimtable.size(); v++)
      if (elimtable[v].order > 0)
	vs.push(v);
    
    sort(vs, ElimOrderLt(elimtable));
    
    minisat::vec<lbool> mmodel;
    mmodel.growTo(nVars());
    
    for (int i = 0; i < vs.size(); i++){
      Var v = vs[i];
      Lit l = lit_Undef;
      mmodel[v]=l_Undef;
      
      for (int j = 0; j < elimtable[v].eliminated.size(); j++){
	Clause& c = *elimtable[v].eliminated[j];
	
	for (int k = 0; k < c.size(); k++){
	  if(value(c[k])==l_Undef) {
	    ((Belegung[var(c[k])+1])&1)  ? mmodel[var(c[k])]=l_False : mmodel[var(c[k])]=l_True;}
	  else { mmodel[var(c[k])]=value(c[k]);
	  if(value(var(c[k]))==l_True) Belegung[var(c[k])+1]=((var(c[k])+1)<< 1);
	  if(value(var(c[k]))==l_False) Belegung[var(c[k])+1]=((var(c[k])+1)<< 1)+1;
	  }
	  
	  if (var(c[k]) == v)
	    l = c[k]; 
	  else if ((((Belegung[var(c[k])+1])& 1) ^ sign(c[k])) == 0){
	    goto next;
	  }
	}
  
	assert(l != lit_Undef);
	mmodel[v] = lbool(!sign(l));
	if (mmodel[v]==l_False){
	  Belegung[v+1]=((v+1)<< 1)+1;
	}
	else if (mmodel[v]==l_True){
	  Belegung[v+1]=((v+1)<< 1);
	}
	break;
	
      next:;
      } 
      if (mmodel[v] == l_Undef){
	Belegung[v+1]=((v+1) << 1);
      }
    }
  }

  bool SimpSolver::eliminate(bool turn_off_elim)
  {
    // Main simplification loop:
    while (subsumption_queue.size() > 0 || elim_heap.size() > 0){ 
      
      if (!backwardSubsumptionCheck(true))
	return false;
      
      for (int cnt = 0; !elim_heap.empty(); cnt++){
	Var elim = elim_heap.removeMin(); 
	
	if (!frozen[elim] && !eliminateVar(elim))
	  return false;
      }
      
      assert(subsumption_queue.size() == 0);
      gatherTouchedClauses();
    }
    
    // Cleanup:
    cleanUpClauses();
    order_heap.filter(VarFilter(*this));

#ifdef INVARIANTS

    // Check that no more subsumption is possible:
    reportf("Checking that no more subsumption is possible\n");
    for (int i = 0; i < clauses.size(); i++){
      if (i % 1000 == 0)
	reportf("left %10d\r", clauses.size() - i);
      
      assert(clauses[i]->mark() == 0);
      for (int j = 0; j < i; j++)
	assert(clauses[i]->subsumes(*clauses[j]) == lit_Error);
    }
    reportf("done.\n");
    
    // Check that no more elimination is possible:
    reportf("Checking that no more elimination is possible\n");
    for (int i = 0; i < nVars(); i++)
      if (!frozen[i]) eliminateVar(i, true);
    reportf("done.\n");
    checkLiteralCount();

#endif
    
    // If no more simplification is needed, free all simplification-related data structures:
    if (turn_off_elim){
      use_simplification = false;
      touched.clear(true);
      occurs.clear(true);
      n_occ.clear(true);
      subsumption_queue.clear(true);
      elim_heap.clear(true);
      remove_satisfied = true;
    }
    
    return true;
  }


  void SimpSolver::cleanUpClauses()
  {
    int      i , j;
    vec<Var> dirty;
    for (i = 0; i < clauses.size(); i++)
      if (clauses[i]->mark() == 1){
	Clause& c = *clauses[i];
	for (int k = 0; k < c.size(); k++)
	  if (!seen[var(c[k])]){
	    seen[var(c[k])] = 1;
	    dirty.push(var(c[k]));
	  } }
    
    for (i = 0; i < dirty.size(); i++){
      cleanOcc(dirty[i]);
      seen[dirty[i]] = 0; }
    
    for (i = j = 0; i < clauses.size(); i++)
      if (clauses[i]->mark() == 1)
	free(clauses[i]);
      else
	clauses[j++] = clauses[i];
    clauses.shrink(i - j);
  }
  

  //=================================================================================================
  // Convert to DIMACS:
  

  void SimpSolver::toDimacs(FILE* f, Clause& c)
  {
    if (satisfied(c)) return;
    
    for (int i = 0; i < c.size(); i++)
      if (value(c[i]) != l_False)
	fprintf(f, "%s%d ", sign(c[i])? "-" : "", var(c[i])+1);
    fprintf(f, "0\n");
  }
  

  void SimpSolver::toDimacs(const char* file)
  {
    assert(decisionLevel() == 0);
    FILE* f = fopen(file, "wr");
    if (f != NULL){
      
      // Cannot use removeClauses here because it is not safe
      // to deallocate them at this point. Could be improved.
      int cnt = 0;
      for (int i = 0; i < clauses.size(); i++)
	if (satisfied(*clauses[i]))
	  cnt++;
      
      fprintf(f, "p cnf %d %d\n", nVars(), clauses.size());
      
      for (int i = 0; i < clauses.size(); i++)
	toDimacs(f,(*clauses[i]));
      
      fprintf(stderr, "Wrote %d clauses...\n", clauses.size());
    }else
      fprintf(stderr, "could not open file %s\n", file);
  }
  
  
  void  SimpSolver::litToint(){
    for (int i = 0; i < clauses.size(); i++){
      Clause& c = *clauses[i];
      for (int i = 0; i < c.size(); i++){
	toInt(c[i]);
      }
    }
  }
  

} // end namespace minisat