picasso/SAT_Encoding.h at master · lorensipro/picasso · GitHub

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
/****************************************************************************************
 *
 * This file is part of Graph Coloring
 *
 * Graph Coloring is free software: you can redistribute it and/or modify it
 * under the terms of the GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Graph Coloring is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY;
 * without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
 * See the GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License along with Graph Coloring.
 * If not, see http://www.gnu.org/licenses/.
 *
 * Contributors:
 *       - Valentin Montmirail ([email protected])
 ***************************************************************************************************/

#ifndef SAT_ENCODING_H
#define SAT_ENCODING_H

#include "Graph.h"
#include "SimpSolver.h"
#include "Encoder.h"
#include "Enc_Totalizer.h"

using namespace std;
using namespace msp;

class SAT_Encoding {

private:

	bool verbose = false;

	unsigned int nbNodes;

public:

	vector< vector<unsigned int> > s_ij;

	vector<unsigned int> n_i;

	inline unsigned int getNbNodes() { return nbNodes; }

	SAT_Encoding(Graph* g, Glucose::Solver* solver);

	~SAT_Encoding() { }

};

#endif