pb2cnf.cpp

#include "pb2cnf.h"
#include <math.h>

#include <algorithm>
#include <memory>

using namespace PBLib;
using namespace std;

////////////////////////////////////////////////////////////////////
//        Encoding for incremental PB constraints                 //
////////////////////////////////////////////////////////////////////
void PB2CNF::encodeIncInital(IncPBConstraint& incPbconstraint, ClauseDatabase& formula, AuxVarManager& auxVars)
{
  
  shared_ptr<IncSimplePBConstraint> constraint = pre_encoder.preEncodeIncPBConstraint(incPbconstraint, formula);  

  vector<int32_t> geqOneClause; // for the amo constraint
  
  switch(constraint->getType())
  {
    case DONTCARE:
      constraint->setIncrementalData(make_shared<IncrementalDontCare>());
      break;
    case AMO:
      for (auto wlits : constraint->getWeightedLiterals())
	geqOneClause.push_back(wlits.lit);
      
      constraint->setIncrementalData(make_shared<AMOIncrementalData>(geqOneClause));
      encode_amo(*constraint, formula, auxVars);
      break;
    case AMK:
      encode_inc_amk(constraint, incPbconstraint, formula, auxVars);
      break;
    case PB:
      encode_inc_pb(constraint, incPbconstraint, formula, auxVars);
      break;
    default:
      assert(false && "this should never occure");
  }
}


void PB2CNF::encode_inc_with_adder(shared_ptr< IncSimplePBConstraint > constraint, ClauseDatabase & formula, AuxVarManager & auxVars)
{
  stats->num_adder_encodings++;
  adder_encoder.encode(constraint, formula, auxVars);
}

void PB2CNF::encode_inc_with_swc(shared_ptr< IncSimplePBConstraint > constraint, ClauseDatabase& formula, AuxVarManager& auxVars)
{
  swc_encoder.encode(constraint, formula, auxVars);
}



void PB2CNF::encode_inc_amk(shared_ptr< IncSimplePBConstraint > constraint, IncPBConstraint & incPbconstraint, ClauseDatabase & formula, AuxVarManager & auxVars)
{
  if (card_encoder.encodingValue(constraint) < config->MAX_CLAUSES_PER_CONSTRAINT ) // aprox number of card clauses 
    encode_inc_with_card(constraint, formula, auxVars);
  else
    encode_inc_with_adder(constraint, formula, auxVars);
}

void PB2CNF::encode_inc_pb(shared_ptr< IncSimplePBConstraint > constraint, IncPBConstraint & incPbconstraint, ClauseDatabase & formula, AuxVarManager & auxVars)
{
  if(config->pb_encoder == PB_ENCODER::ADDER)
  {
    encode_inc_with_adder(constraint, formula, auxVars);
    return;
  }
  
  if(config->pb_encoder == PB_ENCODER::SWC)
  {
    encode_inc_with_swc(constraint, formula, auxVars);
    return;
  }
  
  if (swc_encoder.encodingValue(constraint) < config->MAX_CLAUSES_PER_CONSTRAINT ) // aprox number of card clauses 
    encode_inc_with_swc(constraint, formula, auxVars);
  else
    encode_inc_with_adder(constraint, formula, auxVars);
}


void PB2CNF::encode_inc_with_card(shared_ptr< IncSimplePBConstraint > constraint, ClauseDatabase & formula, AuxVarManager & auxVars)
{
  stats->num_card_encodings++;
  card_encoder.encode(constraint, formula, auxVars);
}




////////////////////////////////////////////////////////////////////
//        Encoding for normal PB constraints                      //
////////////////////////////////////////////////////////////////////

bool PB2CNF::try_to_encode_in_threshold(SimplePBConstraint& constraint, ClauseDatabase& formula, AuxVarManager& auxVars, int clause_threshold)
{
  
  //TODO refactor this... and use encodingValue methode
	if (constraint.getType() == DONTCARE)
		return true;
	
	if (clause_threshold == 0)
		return false;
	
  if (constraint.getType() == AMO)
  {
	  if (constraint.getN() * 3 < clause_threshold)
	  {
		  encode_amo(constraint, formula, auxVars);
		  return true;
	  }
	  else
		  return false;
  }
  
  if (constraint.getType() == AMK)
  {
	  if ( (constraint.getN() * ceil(log2(constraint.getLeq())) * ceil(log2(constraint.getLeq()))) < clause_threshold)
	  {
		  encode_amk(constraint, formula, auxVars);
		  return true;
	  }
	  else
		  return false;
  }

  assert(constraint.getType() == PB);
	// since we cannot approx the number of clauses with BDD encoding on real PBs we try to encode the constraint within the limit,
  // if this is not possible we cancle the encoding and fallback to the adder encoding
  tmpFormula.clearDatabase();
  tmpVariables.clear();
  auxVars.startRememberReturnedVariables(&tmpVariables);
  bdd_encoder.bddEncode(constraint, tmpFormula, auxVars, false, clause_threshold);
  auxVars.stopRememerReturnedVariables();
  

  int64_t num_of_bin_merge_clauses = (constraint.getComparator() == BOTH ? 2 : 1) * constraint.getN() * ceil(log2(constraint.getLeq())) * ceil(log2(constraint.getLeq())) * ceil(log2(constraint.getMaxWeight()));
  if (bdd_encoder.wasToBig() || tmpFormula.getClauses().size() > num_of_bin_merge_clauses)
  {
    // BDD was to big
    auxVars.freeVariables(tmpVariables); // reset aux variables of tmp BDD encoding
    
    if ( num_of_bin_merge_clauses < clause_threshold)
	{
	  // use non gac variant
		bool tmp = config->use_gac_binary_merge;
		config->use_gac_binary_merge = false;
		encode_with_binary_merge(constraint, formula, auxVars);
		config->use_gac_binary_merge = tmp;
	}
    else
      return false;
  }
  else
  {
    // encode with BDD
    stats->num_bdd_gates_encodings++;
    formula.addClauses(tmpFormula.getClauses());
  }
  tmpFormula.clearDatabase();
  tmpVariables.clear();
	
	return false;
}


int32_t PB2CNF::encodeAtLeastK(const vector< int32_t >& literals, int64_t k, vector< vector< int32_t > >& formula, int32_t firstAuxiliaryVariable)
{
  vector<int64_t> weights;
  for (int i = 0; i < literals.size(); ++i)
    weights.push_back(1);
  
  return encodeGeq(weights, literals, k, formula, firstAuxiliaryVariable);
}


int32_t PB2CNF::encodeAtMostK(const vector< int32_t >& literals, int64_t k, vector< vector< int32_t > >& formula, int32_t firstAuxiliaryVariable)
{
  vector<int64_t> weights;
  for (int i = 0; i < literals.size(); ++i)
    weights.push_back(1);
  
  return encodeLeq(weights, literals, k, formula, firstAuxiliaryVariable);
}


int32_t PB2CNF::encodeGeq(const vector< int64_t >& weights, const vector< int32_t >& literals, int64_t geq, vector< vector< int32_t > >& formula, int32_t firstAuxiliaryVariable)
{
  assert(weights.size() == literals.size());
  
  if (literals.size() != weights.size())
  {
    cerr << "c [PBLib] error: size of weights differ from size of literals, can not encode constraint" << endl;
    return 0;
  }
  
  vector<WeightedLit> lits;
  for (int i = 0; i < weights.size(); ++i)
    lits.push_back(WeightedLit(literals[i], weights[i]));
  
  PBLib::PBConstraint constraint(lits, PBLib::GEQ, geq);
  VectorClauseDatabase clauseDatabase(config, &formula);
  AuxVarManager auxVars(firstAuxiliaryVariable);
  
  encode(constraint, clauseDatabase, auxVars);
  
  return auxVars.getBiggestReturnedAuxVar();
}

int32_t PB2CNF::encodeBoth(const vector< int64_t >& weights, const vector< int32_t >& literals, int64_t leq, int64_t geq, vector< vector< int32_t > >& formula, int32_t firstAuxiliaryVariable)
{
  assert(weights.size() == literals.size());
  
  if (literals.size() != weights.size())
  {
    cerr << "c [PBLib] error: size of weights differ from size of literals, can not encode constraint" << endl;
    return 0;
  }
  
  vector<WeightedLit> lits;
  for (int i = 0; i < weights.size(); ++i)
    lits.push_back(WeightedLit(literals[i], weights[i]));
  
  PBLib::PBConstraint constraint(lits, PBLib::BOTH, leq, geq);
  VectorClauseDatabase clauseDatabase(config, &formula);
  AuxVarManager auxVars(firstAuxiliaryVariable);
  
  encode(constraint, clauseDatabase, auxVars);
  
  return auxVars.getBiggestReturnedAuxVar();
}


int32_t PB2CNF::encodeLeq(const vector< int64_t >& weights, const vector< int32_t >& literals, int64_t leq, vector< vector< int32_t > >& formula, int32_t firstAuxiliaryVariable)
{
  assert(weights.size() == literals.size());
  
  if (literals.size() != weights.size())
  {
    cerr << "c [PBLib] error: size of weights differ from size of literals, can not encode constraint" << endl;
    return 0;
  }
  
  vector<WeightedLit> lits;
  for (int i = 0; i < weights.size(); ++i)
    lits.push_back(WeightedLit(literals[i], weights[i]));
  
  PBLib::PBConstraint constraint(lits, PBLib::LEQ, leq);
  VectorClauseDatabase clauseDatabase(config, &formula);
  AuxVarManager auxVars(firstAuxiliaryVariable);
  
  encode(constraint, clauseDatabase, auxVars);
  
  return auxVars.getBiggestReturnedAuxVar();
}

  

void PB2CNF::encode(const PBConstraint& pbconstraint, PBSATSolver& satsolver, AuxVarManager& auxVars, int clause_threshold)
{
	// encode with clause clause threshold
	VectorClauseDatabase formula(config);
	SimplePBConstraint constraint = pre_encoder.preEncodePBConstraint(pbconstraint, formula);
	
	for(auto clause : formula.getClauses())
		satsolver.addClause(clause);
	
	if (constraint.getType() == DONTCARE)
		return;
	
	if (try_to_encode_in_threshold(constraint, formula, auxVars, clause_threshold))
	{
		if (config->print_used_encodings)cout << "c debug: encoded in clauses" << endl;
		for(auto clause : formula.getClauses())
			satsolver.addClause(clause);
		return;
	}
	if (config->print_used_encodings) cout << "c debug: encoded native" << endl;
	
	

	
	if (constraint.getComparator() == BOTH)
	{
		encode(constraint.getLeqConstraint(), satsolver, auxVars, clause_threshold / 2);
		encode(constraint.getGeqConstraint(), satsolver, auxVars, clause_threshold / 2);
	}
	else
	{
	  if (constraint.getType() == AMO || constraint.getType() == AMK)
	  {
		  vector<int32_t> lits;
		  for (auto wlit : constraint.getWeightedLiterals())
			  lits.push_back(wlit.lit);
		  
		  satsolver.addAtMost(lits, constraint.getLeq());
	  }
	  else
	  {
		  assert(constraint.getType() == PB);
		  vector<int32_t> lits;
		  vector<int64_t> weights;
		  for (auto wlit : constraint.getWeightedLiterals())
		  {
			  lits.push_back(wlit.lit);
			  weights.push_back(wlit.weight);
		  }
		  
		  satsolver.addPBLeq(lits, weights, constraint.getLeq());
	  }
  }
}


void PB2CNF::encode(const PBConstraint& pbconstraint, ClauseDatabase& formula, AuxVarManager& auxVars)
{
  SimplePBConstraint constraint = pre_encoder.preEncodePBConstraint(pbconstraint, formula);
  
  if (config->just_approximate)
  {
	  // experimental code
	  cout << "c warning, approximation is experimental code" << endl;
	  vector<WeightedLit> approx_lits;
	  long double new_max = config->approximate_max_value;
	  long double old_max = constraint.getMaxWeight();

	  for (WeightedLit lit : constraint.getWeightedLiterals())
	  {
		  approx_lits.push_back(WeightedLit(lit.lit,  floor((((long double)lit.weight) / old_max) * new_max)));
	  }
	  
	  
	  if (constraint.getComparator() == BOTH)
	  {
			long double new_geq = ceil(((long double)constraint.getGeq() / old_max) * new_max);
			long double new_leq = ceil(((long double)constraint.getLeq() / old_max) * new_max);
			constraint = pre_encoder.preEncodePBConstraint(PBConstraint(approx_lits, BOTH, new_leq, new_geq), formula);
	  }
	  else
	  {
			long double new_leq = ceil(((long double)constraint.getLeq() / old_max) * new_max);
			constraint = pre_encoder.preEncodePBConstraint(PBConstraint(approx_lits, LEQ, new_leq), formula);
	  }
  }

  switch(constraint.getType())
  {
    case DONTCARE:
      break; 
    case AMO:
      encode_amo(constraint, formula, auxVars);
      break;
    case AMK:
      encode_amk(constraint, formula, auxVars);
      break;
    case PB:
      encode_pb(constraint, formula, auxVars);
      break;
    default:
      assert(false && "this should never occure");
  }  
}

void PB2CNF::encode_amo(SimplePBConstraint & constraint, ClauseDatabase & formula, AuxVarManager & auxVars)
{
  stats->num_amo_encodings++;
  switch (config->amo_encoder)
  {
    using namespace AMO_ENCODER;
    case BDD:
      bdd_sec_amo.encode(constraint, formula, auxVars);
      break;
    case NESTED:
      amo_encoder.encode(constraint, formula, auxVars);
      break;
    case BIMANDER:
      bimander_amo_encoding.encode(constraint, formula, auxVars);
      break;
    case COMMANDER:
      commander_amo_encoding.encode(constraint, formula, auxVars);
      break;
    case KPRODUCT:
      k_product_encoer.encode(constraint, formula, auxVars);
      break;
    case BINARY:
      binary_amo_encoder.encode(constraint, formula, auxVars);
      break;
    case PAIRWISE:
      naive_amo_encoder.encode(constraint, formula, auxVars);
      break;
    case BEST:
      if (!encodeWithBestEncoder(vector<Encoder*>
			    {&bdd_sec_amo, &amo_encoder, &bimander_amo_encoding, &commander_amo_encoding, &k_product_encoer, &binary_amo_encoder, &naive_amo_encoder, &adder_encoder},
			    constraint, formula, auxVars)
      )
      {
	cerr << "c [pblib] error: could not encode a constraint" << endl;
	cout << "c [pblib] current constraint: "; constraint.printNoNL(); cout << endl;
	assert(false);
      }
      break;
    default:
      amo_encoder.encode(constraint, formula, auxVars);
  }
}


void PB2CNF::encode_amk(SimplePBConstraint& constraint, ClauseDatabase& formula, AuxVarManager& auxVars)
{

  if (config->amk_encoder == AMK_ENCODER::CARD)
    encode_with_card(constraint, formula, auxVars);
  else 
  if (config->amk_encoder == AMK_ENCODER::BDD)
    encode_with_bdd(constraint, formula, auxVars);
  else
  if (!encodeWithBestEncoder(vector<Encoder*>
			    {&card_encoder, &bdd_encoder, &adder_encoder},
			    constraint, formula, auxVars)
  )
  {
      cerr << "c [pblib] error: could not encode a constraint" << endl;
      cout << "c [pblib] current constraint: "; constraint.printNoNL(); cout << endl;
      assert(false);
  }
  
  
}

void PB2CNF::encode_with_binary_merge(SimplePBConstraint& constraint, ClauseDatabase& formula, AuxVarManager& auxVars)
{
  if (constraint.getComparator() == BOTH)
  {
    // since the LEQ or GEQ could be a DONTCARE (result in an error) or a AMO / AMK constraint, we call the encode methode again (for an other preencoding)
    // and probably end up here again
    encode(constraint.getGeqConstraint(), formula, auxVars);
    encode(constraint.getLeqConstraint(), formula, auxVars);
  }
  else
  {
    binary_merge.encode(constraint, formula, auxVars);
  }
}



void PB2CNF::encode_pb(SimplePBConstraint& constraint, ClauseDatabase& formula, AuxVarManager& auxVars)
{
  if(config->pb_encoder == PB_ENCODER::SORTINGNETWORKS)
  {
    sorting_networks.encode(constraint, formula, auxVars);
    return;
  }
  else 
  if(config->pb_encoder == PB_ENCODER::ADDER)
  {
    encode_with_adder(constraint, formula, auxVars);
    return;
  }
  else 
  if(config->pb_encoder == PB_ENCODER::BDD)
  {
    encode_with_bdd(constraint, formula, auxVars);
    return;
  }
  else 
  if(config->pb_encoder == PB_ENCODER::BINARY_MERGE)
  {
    encode_with_binary_merge(constraint, formula, auxVars);
    return;
  }
  else 
  if(config->pb_encoder == PB_ENCODER::SWC)
  {
    encode_with_swc(constraint, formula, auxVars);
    return;
  }
  else //TODO this way bdds are calculated twice: first time during clause counting, secound time if selected as best encoding
  if (!encodeWithBestEncoder(vector<Encoder*>
			    {&sorting_networks, &adder_encoder, &bdd_encoder, &binary_merge},
			    constraint, formula, auxVars)
  )
  {
      cerr << "c [pblib] error: could not encode a constraint" << endl;
      cout << "c [pblib] current constraint: "; constraint.printNoNL(); cout << endl;
      assert(false);
  }
}

void PB2CNF::encode_with_adder(SimplePBConstraint& constraint, ClauseDatabase& formula, AuxVarManager& auxVars)
{
  stats->num_adder_encodings++;
  adder_encoder.encode(constraint, formula, auxVars);
}

void PB2CNF::encode_with_swc(SimplePBConstraint& constraint, ClauseDatabase& formula, AuxVarManager& auxVars)
{
  swc_encoder.encode(constraint, formula, auxVars);
}


void PB2CNF::encode_with_bdd(SimplePBConstraint& constraint, ClauseDatabase& formula, AuxVarManager& auxVars)
{
  stats->num_bdd_gates_encodings++;
  bdd_encoder.encode(constraint, formula, auxVars);
}

void PB2CNF::encode_with_card(SimplePBConstraint& constraint, ClauseDatabase& formula, AuxVarManager& auxVars)
{
  stats->num_card_encodings++;
  card_encoder.encode(constraint, formula, auxVars);
}



PB2CNF::PB2CNF() : PB2CNF(basic_default_config, nullptr)
{
  
}


PB2CNF::PB2CNF(PBConfig& config, statistic* _stats) 
  : tmpFormula(config), pre_encoder(config, _stats), config(config), bdd_encoder(config), adder_encoder(config), amo_encoder(config), binary_amo_encoder(config), k_product_encoer(config), commander_amo_encoding(config), naive_amo_encoder(config), bimander_amo_encoding(config), bdd_sec_amo(config), card_encoder(config), sorting_networks(config),binary_merge(config), swc_encoder(config), stats(_stats)
{
  if (stats == 0)
  {
    stats = new statistic;
    private_stats = true;
  }
  else
  {
    private_stats = false;
  }
}



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



bool PB2CNF::encodeWithBestEncoder(vector< Encoder*> encoders, SimplePBConstraint& constraint, ClauseDatabase& formula, AuxVarManager& auxVars)
{
  if (encoders.size() == 0)
    return false;
  
  Encoder* bestEncoder = encoders[0];
  int64_t  bestValue= encoders[0]->encodingValue(constraint);
  
  for (int i = 1; i < encoders.size(); ++i)
  {
    int64_t encodingValue = encoders[i]->encodingValue(constraint);
    if (encodingValue < 0)
      continue;
    
    if ( (bestValue < 0) || (encodingValue < bestValue))
    {
      bestValue = encodingValue;
      bestEncoder = encoders[i];
    }
  }
  
  if (bestValue < 0)
    return false;
  
  bestEncoder->encode(constraint, formula, auxVars);
  
  return true;
}


bool PB2CNF::encodeWithBestEncoder(std::vector< Encoder* > encoders, shared_ptr< IncSimplePBConstraint > constraint, ClauseDatabase& formula, AuxVarManager& auxVars)
{
  if (encoders.size() == 0)
    return false;
  
  Encoder* bestEncoder = encoders[0];
  int64_t  bestValue= encoders[0]->encodingValue(constraint);
  
  for (int i = 1; i < encoders.size(); ++i)
  {
    int64_t encodingValue = encoders[i]->encodingValue(constraint);
    if (encodingValue < 0)
      continue;
    
    if ( (bestValue < 0) || (encodingValue < bestValue))
    {
      bestValue = encodingValue;
      bestEncoder = encoders[i];
    }
  }
  
  if (bestValue < 0)
    return false;
  
  bestEncoder->encode(constraint, formula, auxVars);
  
  return true;
}