Pseudo Boolean optimisation - marcbenedi/SAT-tfg GitHub Wiki

Table of contents

  • Features
    • Pseudo-Boolean minimisation problems representation
      • Pseudo-Boolean formula
      • Pseudo-Boolean constraints
      • Pseudo-Boolean minimisation problem
    • How to solve it
      • Search strategy
        • Binary
        • Linear
      • Solver
        • Without timeout
        • Timeout per SAT solver execution
        • Global timeout
  • Examples

Features

Pseudo-Boolean minimisation problems representation

Pseudo-Boolean formula

Pseudo-Boolean formulae are represented with the class PBFormula. The first parameter are the coefficients and the second one the variables.

PBFormula({1,5,3,4},{1,2,3,4});
//x_1 + 5x_2 + 3x_3 + 4x_4

As you can see, the Pseudo-Boolean formulas are linear.

Pseudo-Boolean constraint

Pseudo-Boolean constraints are represented with the class PBConstraint. The first parameter is a PBFormula and the second one is an int64_t.

PBConstraint(PBFormula({1,5,3,4},{1,2,3,4}),8);
//x_1 + 5x_2 + 3x_3 + 4x_4 <= 8

Pseudo-Boolean minimisation problem

A Pseudo-Boolean minimisation problem has two components:

  • A set of pseudo-Boolean constraints
  • A cost function
std::vector< PBConstraint > constraints = {
    PBConstraint(PBFormula({1,5,3,4},{1,2,3,4}),8)
};
PBFormula costFunction({-15,-10,-9,-5},{1,2,3,4});
PBMin m = PBMin(constraints, costFunction);

How to solve it

Search strategy

There are two search strategies. These strategies define which strategy will be used to find the minim value:

  • Binary search
#include "BinarySearchStrategy.h"
BinarySearchStrategy bs;
  • Linear search
#include "LinearSearchStrategy.h"
LinearSearchStrategy ls;

For example, if the cost function of the problem is 3x+y, the possible minimum value is between 0 and 4. For example, if the selected search strategy is Linear search, the values will be selected like 4,3,2,1,0 until the minimum satisfiable value is found or no value is satisfiable.

Solver

Solver is the class in charge of solving the problem.

Without timeout
...
#include "Solver.h"

std::vector< PBConstraint > constraints = ...;
PBFormula costFunction(...,...);
PBMin m = ...;

BinarySearchStrategy bs;

Solver s(&bs, m);

std::vector< int32_t > model;
int64_t min;
bool sat = s.run(model,min);
Timeout per SAT solver execution
...
#include "SimpleTimeoutSolver.h"

std::vector< PBConstraint > constraints = ...;
PBFormula costFunction(...,...);
PBMin m = ...;

BinarySearchStrategy bs;
int timeout = 6;

SimpleTimeoutSolver s(timeout, &bs, m);

std::vector< int32_t > model;
int64_t min;
bool sat = s.run(model,min);
Global timeout
...
#include "GeneralTimeoutSolver.h"

std::vector< PBConstraint > constraints = ...;
PBFormula costFunction(...,...);
PBMin m = ...;

BinarySearchStrategy bs;
int timeout = 60;

GeneralTimeoutSolver s(timeout, &bs, m);

std::vector< int32_t > model;
int64_t min;
bool sat = s.run(model,min);

Examples

The knapsack problem

#include "PBConstraint.h"
#include <vector>
#include "LinearSearchStrategy.h"
#include "Solver.h"
#include "PBMin.h"

int main() {

	//PROBLEM DEFINITION
	std::vector< PBConstraint > constraints = {
			PBConstraint(PBFormula({1,5,3,4},{1,2,3,4}),8)
	};
	PBFormula costFunction({-15,-10,-9,-5},{1,2,3,4});

	//TOOLS TO SOLVE THE PROBLEM
	LinearSearchStrategy bs;
	PBMin m = PBMin(constraints, costFunction);
	Solver s(&bs,m);

	//VARIABLES WHERE THE RESULT WILL BE STORED
	std::vector< int32_t > model;
	int64_t min;

	//START THE EXECUTION
	bool sat = s.run(model,min);

	//PRINT THE SOLUTION
	std::cout << "Is the problem satisfiable? " << sat <<'\n';
	std::cout << "Which is the maximum value I can carry on? " << abs(min) << '\n';
	std::cout << "How?" << '\n';
	for (size_t i = 0; i < 4; i++) {
		std::cout << model[i] << " ";
	}
	std::cout << '\n';

}
Is the problem satisfiable? 1  
Which is the maximum value I can carry on? 29  
How?  
1 -2 3 4

Printing the model

The for iterates between 0 and 4, which is the number of variables, because internally the software generates auxiliar variables to convert the problem into CNFs. The SAT solver generates a model for these variables also but we don't care about them. That's why we only print the variables we want to know their assignment.

for (size_t i = 0; i < model.size(); i++) {
	std::cout << model[i] << " ";
}
Is the problem satisfiable? 1  
Which is the maximum value I can carry on? 29  
How?  
1 -2 3 4 5 -6 -7 8 -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 -23 -24 -25 -26 -27 -28 -29 -30 -31 -32 -33 -34 -35
 -36 -37 -38 -39 -40 -41 -42 -43 -44 -45 -46 -47 48 49 50 51 52 53 54 55 56 57 -58 -59 -60 -61 -62 -63 -64 -65 -66 -67 -68 -6
9 -70 -71 -72 -73 -74 -75 -76 -77 -78 -79 -80 -81 -82 -83 -84 -85 -86 87 88 89 90 91 92 93 94 95 96 -97 -98 -99 -100 -101 -10
2 -103 -104 -105 -106 -107 -108 -109 -110 -111 -112 -113 -114 -115 -116 -117 -118 -119 -120 -121 -122 -123 -124 -125 126 127
128 129 130 131 132 133 134 135 -136 -137 -138 -139 -140 -141 -142 -143 -144 -145 -146 -147 -148 -149 -150 -151 -152 -153 -15
4 -155 -156 -157 -158 -159 -160 -161 -162 -163 -164 0
⚠️ **GitHub.com Fallback** ⚠️