preencoder.cpp

#include "preencoder.h"

#include <vector>

using namespace PBLib;
using namespace std;
template <class PBCon>
void PreEncoder::init_and_normalize(PBCon const & pbconstraint, ClauseDatabase& formula)
{
  literals = pbconstraint.getWeightedLiterals();
  comparator = pbconstraint.getComparator();
  max_sum = 0;
  max_weight = 0;
  bound_offset = 0;
  type = PB;
  n = literals.size();
  isAMK = false;
  isAMKEqual = false;
  leq = pbconstraint.getLeq();
  geq = pbconstraint.getGeq();
  
  if (comparator == GEQ)
  { // normalize to LEQ by negation
    comparator = LEQ;
    leq = -geq;
    for (int i = 0; i < (int)literals.size(); ++i)
      literals[i].weight = -literals[i].weight;
  }
  
  join_duplicat_literals();
  normalize_variables();
 
  leq += bound_offset;
  geq += bound_offset;
  
  remove_lits_with_w_greater_leq_and_check_isamk(formula);
}


void PreEncoder::remove_lits_with_w_greater_leq_and_check_isamk(ClauseDatabase& formula)
{
  isAMK = true;
  isAMKEqual = true;
  check_amk_equal = 0;
  if (literals.size() > 0)
  {
     check_amk_equal = literals[0].weight;
  }
  else
  {
    isAMKEqual = false;
    isAMK = false;
  }
  
  for (int i = 0; i < (int)literals.size(); ++i)
  {  
    tmpWeight = literals[i].weight;
    
    if(tmpWeight > leq)
    {
      formula.addClause(-literals[i].lit);
      literals[i] = literals[literals.size() - 1];
      literals.pop_back();
      i--;
      n--;
      continue;
    }
    
    max_sum += tmpWeight;
    
    if (isAMK && tmpWeight != 1)
    {
      isAMK = false;
    }
    
    if (isAMKEqual && tmpWeight != check_amk_equal)
    {
      isAMKEqual = false;
    }
    
    if (tmpWeight > max_weight)
      max_weight = tmpWeight;
  }
  
  if (check_amk_equal == 0)
    isAMKEqual = false;
}


void PreEncoder::normalize_variables()
{
  for (int i = 0; i < (int)literals.size(); ++i)
  {
    tmpWeight = literals[i].weight;
    if ( tmpWeight == 0) // ignore literals with weight 0
    {
      literals[i] = literals[literals.size() - 1];
      literals.pop_back();
      i--;
      n--;
      continue;
    }
    
    if (tmpWeight < 0) // if the weight is negative, normalize literal
    {
      tmpWeight = -tmpWeight; // results in a positive weight
      bound_offset += tmpWeight; // adjust bound offset (for leq / geq lateron)
      literals[i].weight = tmpWeight; // save new (positive) weight
      literals[i].lit = -literals[i].lit; // save the complement of the literal
    }
  }
}


void PreEncoder::join_duplicat_literals()
{
  sort(literals.begin(), literals.end(),WeightedLit::compVariable_des_var);
  vector<int32_t> del_element;
  for (int i = 1; i < literals.size(); ++i)
  {
    if (literals[i].lit == literals[i-1].lit)
    {
      literals[i].weight += literals[i-1].weight;
      del_element.push_back(i-1);
    }
    else if (literals[i].lit == -literals[i-1].lit)
    {
      bound_offset -= literals[i-1].weight;
      literals[i].weight += -literals[i-1].weight;
      del_element.push_back(i-1);
    }
  }
  
  for (int i = del_element.size() - 1; i >= 0; --i)
  {
    // no delete duplicates
    literals[del_element[i]] = literals.back();
    literals.pop_back();
    n--;
  }
}


void PreEncoder::check_for_trivial_constraints(ClauseDatabase & formula)
{
  assert(literals.size() == n);
  
  if (leq < 0 || (comparator == BOTH && leq < geq) || (comparator == BOTH && max_sum < geq))
  {
    type = DONTCARE;
    formula.addUnsat();
    stats->num_trivial++;
  }
  else if (n == 0)
  {
    if (comparator == BOTH && geq > 0) 
      formula.addUnsat();    
    
    type = DONTCARE;
    stats->num_trivial++;
    max_weight = 0;
    max_sum = 0;
  }
  else if (leq == 0)
  {
    // in the incremental case we will detected leq < 0 in the encodeNewLeq methode of IncSimplePBConstraint
    // set all literals to false to satisfied == 0
    type = DONTCARE;
    stats->num_trivial++;
    for (int i = 0; i < (int)literals.size(); ++i)
    {
      formula.addClause(-literals[i].lit);
    }
    literals.clear();
    n = 0;
    max_weight = 0;
    max_sum = 0;
  }
}

void PreEncoder::sort_literals()
{
  sort(literals.begin(), literals.end(),WeightedLit::compVariable_des);
//   sort(literals.begin(), literals.end(),WeightedLit::compVariable_asc);
}

// WARNING DONT TOUCH THIS, THIS HAVE TO BE REWRITTEN (TO MANY DEPENDENCIES) TODO
shared_ptr< IncSimplePBConstraint > PreEncoder::preEncodeIncPBConstraint(IncPBConstraint & pbconstraint, ClauseDatabase& formula)
{
  formula.addConditionals(pbconstraint.getConditionals());

  init_and_normalize(pbconstraint, formula);
  check_for_trivial_constraints(formula);
  
  if (type != DONTCARE)
  {   
    if (isAMK)
    {
      if (leq == 1)
      {
	type = AMO;
	stats->num_amo++;
      }
      else
      {
	type = AMK;
	stats->num_amk++;
      }
    }
    else
    {
      type = PB;
      stats->num_pb++;
    }
    sort_literals();
  }
  
    
  for (int i = 0; i < pbconstraint.getConditionals().size(); ++i)
    formula.getConditionals().pop_back();
    
  if (leq > max_sum)
    leq = max_sum;
    
  if (comparator == LEQ)
  { 
    shared_ptr<IncSimplePBConstraint> incSimplePbConstraint = make_shared<IncSimplePBConstraint>(IncSimplePBConstraint(max_sum, max_weight, bound_offset, type, literals, LEQ, leq));
    pbconstraint.setIncSimplePBConstraint(incSimplePbConstraint);
    incSimplePbConstraint->addConditionals(pbconstraint.getConditionals());
    return incSimplePbConstraint;
  }
  else
  {
    if (geq < 0)
      geq = 0;
    
    assert (comparator == BOTH);
    shared_ptr<IncSimplePBConstraint> incSimplePbConstraint = make_shared<IncSimplePBConstraint>(IncSimplePBConstraint(max_sum, max_weight, bound_offset, type, literals, comparator, leq, geq));
    pbconstraint.setIncSimplePBConstraint(incSimplePbConstraint);
    incSimplePbConstraint->addConditionals(pbconstraint.getConditionals());
    return incSimplePbConstraint;
  }
}


// WARNING DONT TOUCH THIS, THIS HAVE TO BE REWRITTEN (TO MANY DEPENDENCIES) TODO
SimplePBConstraint PreEncoder::preEncodePBConstraint(const PBConstraint& pbconstraint, ClauseDatabase& formula)
{
  formula.addConditionals(pbconstraint.getConditionals());
  init_and_normalize(pbconstraint, formula);
  check_for_trivial_constraints(formula);
  
  if (type == DONTCARE)
    ; // we already encode this constraint and continue below
  else if (comparator == BOTH && geq == max_sum) // note that the following trivial constraints cannot used for incremental constraints
  {
    // set all literals to true to satisfied == 0
    type = DONTCARE;
    stats->num_trivial++;
    for (int i = 0; i < (int)literals.size(); ++i)
    {
      formula.addClause(literals[i].lit);
    }
  }
  else if (max_sum <= leq)
  {
    if (comparator == LEQ)
    {
      stats->num_trivial++;
      type = DONTCARE;
    }
    else
    {
      assert(comparator == BOTH);
      PBConstraint c(literals, GEQ, geq);
      c.addConditionals(pbconstraint.getConditionals());
      
      for (int i = 0; i < pbconstraint.getConditionals().size(); ++i)
	formula.getConditionals().pop_back();
      
      return preEncodePBConstraint(c, formula);
    }
  }
  else if (n == 2 && comparator == LEQ && max_sum > leq)
  {
    // since maxsum > leq and n = 2 we know that this is an AMO and with n= 2 that this is a clause
    type = DONTCARE;
    clause.clear();
    
    for (int i = 0; i < (int) literals.size(); ++i)
    {
      clause.push_back(-literals[i].lit);
    }
    formula.addClause(clause);
    stats->num_clause++;
  }
  else
  {
    // no trivial constraint found ... trying to simplify
      if (comparator == BOTH && ((max_sum - leq) < geq)  && ((max_sum - geq) < leq) )
      {
	// both bounds getting smaller if we negate the formula
	for (int i = 0; i < (int)literals.size(); ++i)
	{
	  literals[i].lit = -literals[i].lit;
	}
	
	// we can simply use max_sum as bound offset, since we know that all weights are > 0
	// but we have to change leq in geq and vice versa, because of the negation
	int64_t oldGeq = geq;
	geq = max_sum - leq;
	leq = max_sum - oldGeq;
	
	// we have changed k so we have to readjust the variables
	PBConstraint c(literals, BOTH, leq, geq);
	c.addConditionals(pbconstraint.getConditionals());
	
	for (int i = 0; i < pbconstraint.getConditionals().size(); ++i)
	  formula.getConditionals().pop_back();
	
	return preEncodePBConstraint(c, formula);
      }

      if (comparator == BOTH && geq <= 0)
	  comparator = LEQ; // since we know that all weights > 0
	  
      if (comparator == BOTH && geq == 1)
      {
	// >= 1 is a clause since all weights are > 0 ... we simply add this clause and remove GEQ constraint
	comparator = LEQ;
	clause.clear();
	
	for (int i = 0; i < (int) literals.size(); ++i)
	{
	  clause.push_back(literals[i].lit);
	}
	formula.addClause(clause);
	
	stats->num_clause++;
	comparator = LEQ;
	
	// we have change the comparator so we can try to find new simplifications
	PBConstraint c(literals, LEQ, leq);
	c.addConditionals(pbconstraint.getConditionals());
	
	for (int i = 0; i < pbconstraint.getConditionals().size(); ++i)
	  formula.getConditionals().pop_back();
	
	return preEncodePBConstraint(c, formula);
      }
    
    if (isAMK)
    {
      // it should not happen that comparator is BOTH and n == leq + 1, since is propably handled already be the two previouse simplification
      if (comparator == LEQ && n == leq + 1)
      {
	// this is a clause
	type = DONTCARE;
	clause.clear();
	
	for (int i = 0; i < (int) literals.size(); ++i)
	{
	  clause.push_back(-literals[i].lit);
	}
	formula.addClause(clause);
	stats->num_clause++;
      }
      else
      {
	if (leq == 1)
	{
	  stats->num_amo++;
	  type = AMO;
	}
	else
	{
	  stats->num_amk++;
	  type = AMK;
	}
      }
    }
    else
    {
      type = PB;
      stats->num_pb++;
    }
    
    // NOTE that the XOR (a + b = 1) case is already handled by the previouse leq and geq clause detactions
    
    sort_literals();
  }
  
  
  for (int i = 0; i < pbconstraint.getConditionals().size(); ++i)
    formula.getConditionals().pop_back();
  
  if (comparator == LEQ)
  {
    SimplePBConstraint sc(max_sum, max_weight, type, literals, comparator, leq);
    sc.addConditionals(pbconstraint.getConditionals());
    return sc;
  }
  else
  {
    SimplePBConstraint sc(max_sum, max_weight,type, literals, comparator, leq, geq);
    sc.addConditionals(pbconstraint.getConditionals());
    return sc;
  }
}


PreEncoder::PreEncoder(PBConfig config, statistic* _stats) : config(config), stats(_stats)
{
  if (stats == 0)
  {
    stats = new statistic;
    private_stats = true;
  }
  else
  {
    private_stats = false;
  }
}

PreEncoder::~PreEncoder()
{
  if (private_stats)
    delete stats;
}