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
FormulaPB.h
/*!
* \author Vasco Manquinho - vmm@sat.inesc-id.pt
*
* @section LICENSE
*
* Open-WBO, Copyright (c) 2013-2022, 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 FormulaPB_h
#define FormulaPB_h
#ifdef SIMP
#include "simp/SimpSolver.h"
#else
#include "core/Solver.h"
#endif
using NSPACE::vec;
using NSPACE::Lit;
namespace upmax {
// Cardinality constraint of the form atMostK
class Card {
public:
Card(vec<Lit> &lits, int64_t rhs, bool sign = false) {
lits.copyTo(_lits);
_rhs = rhs;
if (sign) {
int s = 0;
for (int i = 0; i < _lits.size(); i++) {
s += 1;
_lits[i] = ~_lits[i];
}
_rhs = s - _rhs;
}
}
Card() { _rhs = 0; }
~Card() {}
void print() {
printf("Card: ");
for (int i = 0; i < _lits.size(); i++) {
if (sign(_lits[i]))
printf("~");
printf("%d ", var(_lits[i]) + 1);
}
printf(" <= %d\n", (int)_rhs);
}
vec<Lit> _lits;
int64_t _rhs;
};
// PB constraint. The constraint sign is encoded in the structure.
class PB {
public:
PB(vec<Lit> &lits, vec<uint64_t> &coeffs, int64_t rhs, bool s = false) {
lits.copyTo(_lits);
coeffs.copyTo(_coeffs);
_rhs = rhs;
_sign = s;
}
PB() {
_rhs = 0;
_sign = false;
}
~PB() {}
void addProduct(Lit l, int64_t c) {
_coeffs.push();
_lits.push();
if (c >= 0) {
_coeffs[_coeffs.size() - 1] = c;
_lits[_lits.size() - 1] = l;
} else {
_coeffs[_coeffs.size() - 1] = -c;
_lits[_lits.size() - 1] = ~l;
_rhs += -c;
}
}
void addRHS(int64_t rhs) { _rhs += rhs; }
void changeSign() {
int s = 0;
for (int i = 0; i < _coeffs.size(); i++) {
s += _coeffs[i];
_lits[i] = ~(_lits[i]);
}
_rhs = s - _rhs;
_sign = !(_sign);
}
bool isClause() {
// Assume _sign == false...
bool sign = _sign;
if (_sign)
changeSign();
if (_rhs != 1) {
if (_sign != sign)
changeSign();
return false;
}
for (int i = 0; i < _coeffs.size(); i++) {
if (_coeffs[i] != 1) {
if (_sign != sign)
changeSign();
return false;
}
}
return true;
}
bool isCardinality() {
// Assume _sign == false...
bool sign = _sign;
if (_sign)
changeSign();
for (int i = 0; i < _coeffs.size(); i++) {
if (_coeffs[i] != 1) {
if (_sign != sign)
changeSign();
return false;
}
}
return true;
}
void print() {
// Assume _sign == false...
if (isClause())
printf("Clause: ");
else if (isCardinality())
printf("Card: ");
else
printf("PB: ");
for (int i = 0; i < _coeffs.size(); i++) {
printf("%d ", (int)_coeffs[i]);
if (sign(_lits[i]))
printf("~");
printf("%d ", var(_lits[i]) + 1);
}
printf(" >= %d\n", (int)_rhs);
}
vec<uint64_t> _coeffs;
vec<Lit> _lits;
int64_t _rhs;
bool _sign; // atLeast: false; atMost: true
};
class PBObjFunction {
public:
PBObjFunction(vec<Lit> &lits, vec<uint64_t> &coeffs, int64_t c = 0) {
lits.copyTo(_lits);
coeffs.copyTo(_coeffs);
_const = c;
}
PBObjFunction() { _const = 0; }
~PBObjFunction() {}
void addProduct(Lit l, int64_t c) {
_coeffs.push();
_lits.push();
if (c >= 0) {
_coeffs[_coeffs.size() - 1] = c;
_lits[_lits.size() - 1] = l;
} else {
_coeffs[_coeffs.size() - 1] = -c;
_lits[_coeffs.size() - 1] = ~l;
_const += c;
}
}
vec<uint64_t> _coeffs;
vec<Lit> _lits;
int64_t _const;
};
} // namespace upmax
#endif
Computing file changes ...