Revision 613cbffb7e96f803f23141771593a583bb420279 authored by Pedro Orvalho on 28 April 2023, 12:39:23 UTC, committed by GitHub on 28 April 2023, 12:39:23 UTC
1 parent bab67fc
Encoder.h
/*!
* \author Ruben Martins - rubenm@andrew.cmu.edu
*
* @section LICENSE
*
* Open-WBO, Copyright (c) 2013-2017, Ruben Martins, Vasco Manquinho, Ines Lynce
* UpMax, Copyright (c) 2022, Pedro Orvalho, Vasco Manquinho, Ruben Martins
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
* in the Software without restriction, including without limitation the rights
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
* copies of the Software, and to permit persons to whom the Software is
* furnished to do so, subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in
* all copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
* AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
* SOFTWARE.
*
*/
#ifndef Encoder_h
#define Encoder_h
#ifdef SIMP
#include "simp/SimpSolver.h"
#else
#include "core/Solver.h"
#endif
#include "MaxTypes.h"
#include "core/SolverTypes.h"
// Encodings
#include "encodings/Enc_CNetworks.h"
#include "encodings/Enc_GTE.h"
#include "encodings/Enc_Ladder.h"
#include "encodings/Enc_MTotalizer.h"
#include "encodings/Enc_SWC.h"
#include "encodings/Enc_Totalizer.h"
#include "encodings/Enc_Adder.h"
using NSPACE::vec;
using NSPACE::Lit;
using NSPACE::Solver;
namespace upmax {
//=================================================================================================
class Encoder {
public:
Encoder(int incremental = _INCREMENTAL_NONE_,
int cardinality = _CARD_TOTALIZER_, int amo = _AMO_LADDER_,
int pb = _PB_SWC_) {
pb_encoding = pb;
amo_encoding = amo;
incremental_strategy = incremental;
cardinality_encoding = cardinality;
totalizer.setIncremental(incremental);
}
~Encoder() {}
// TEMP
vec<Lit> &lits();
vec<Lit> &outputs();
// At-most-one encodings:
//
// Encode exactly-one constraint into CNF.
void encodeAMO(Solver *S, vec<Lit> &lits);
// Cardinality encodings:
//
// Encode cardinality constraint into CNF.
void encodeCardinality(Solver *S, vec<Lit> &lits, int64_t rhs);
// Update the rhs of an already existent cardinality constraint
void updateCardinality(Solver *S, int64_t rhs);
// Incremental cardinality encodings:
//
// Build a cardinality constraint that can count up to 'rhs'.
// No restriction is made on the value of 'rhs'.
// buildCardinality + updateCardinality is equivalent to encodeCardinality.
// Useful for incremental encodings.
void buildCardinality(Solver *S, vec<Lit> &lits, int64_t rhs);
// Incremental update for cardinality constraints;
void incUpdateCardinality(Solver *S, vec<Lit> &join, vec<Lit> &lits,
int64_t rhs, vec<Lit> &assumptions);
void incUpdateCardinality(Solver *S, vec<Lit> &lits, int64_t rhs,
vec<Lit> &assumptions) {
vec<Lit> empty;
incUpdateCardinality(S, empty, lits, rhs, assumptions);
}
// Add two disjoint cardinality constraints
void addCardinality(Solver *S, Encoder &enc, int64_t rhs);
// PB encodings:
//
// Encode pseudo-Boolean constraint into CNF.
void encodePB(Solver *S, vec<Lit> &lits, vec<uint64_t> &coeffs, uint64_t rhs);
// Update the rhs of an already existent pseudo-Boolean constraint.
void updatePB(Solver *S, uint64_t rhs);
// Predicts the number of clauses needed for the encoding
int predictPB(Solver *S, vec<Lit> &lits, vec<uint64_t> &coeffs, uint64_t rhs);
// Incremental PB encodings:
//
// Incremental PB encoding.
void incEncodePB(Solver *S, vec<Lit> &lits, vec<uint64_t> &coeffs,
int64_t rhs, vec<Lit> &assumptions, int size);
// Incremental update of PB encodings.
void incUpdatePB(Solver *S, vec<Lit> &lits, vec<uint64_t> &coeffs,
int64_t rhs, vec<Lit> &assumptions);
// Incremental update of assumptions.
void incUpdatePBAssumptions(Solver *S, vec<Lit> &assumptions);
// Incremental construction of the totalizer encoding.
// Joins a set of new literals, x_1 + ... + x_i, to an existing encoding of
// the type
// y_1 + ... + y_j <= k. It also updates 'k' to 'rhs'.
void joinEncoding(Solver *S, vec<Lit> &lits, int64_t rhs);
// Other:
//
// Returns true if an encoding has been built, false otherwise.
bool hasCardEncoding();
bool hasPBEncoding();
// Controls the type of encoding to be used:
//
void setCardEncoding(int enc) { cardinality_encoding = enc; }
int getCardEncoding() { return cardinality_encoding; }
void setPBEncoding(int enc) { pb_encoding = enc; }
int getPBEncoding() { return pb_encoding; }
void setAMOEncoding(int enc) { amo_encoding = enc; }
int getAMOEncoding() { return amo_encoding; }
// Controls the modulo value that is used in the modulo totalizer encoding.
//
void setModulo(int m) { mtotalizer.setModulo(m); }
int getModulo() { return mtotalizer.getModulo(); }
// Sets the incremental strategy for the totalizer encoding.
//
void setIncremental(int incremental) {
incremental_strategy = incremental;
totalizer.setIncremental(incremental);
}
protected:
int incremental_strategy;
int cardinality_encoding;
int pb_encoding;
int amo_encoding;
// At-most-one encodings
Ladder ladder;
// Cardinality encodings
CNetworks cnetworks;
MTotalizer mtotalizer;
Totalizer totalizer;
Adder adder;
// PB encodings
SWC swc;
GTE gte;
};
} // namespace upmax
#endif
Computing file changes ...