Open
Graph Drawing
Framework

 v. 2023.09 (Elderberry)
 

Loading...
Searching...
No Matches
Minisat.h
Go to the documentation of this file.
1
32#pragma once
33
34#include <ogdf/basic/basic.h>
35
38
39#include <fstream>
40#include <iostream>
41#include <sstream>
42#include <string>
43#include <vector>
44
45#include <stdarg.h>
46#include <stdio.h>
47
48namespace Minisat {
49
50using std::endl;
51using std::string;
52
60public:
62
63 Clause() { }
64
65 Clause(const Clause& src) { src.m_ps.copyTo(m_ps); }
66
67 virtual ~Clause() { }
68
69 // this function allows to put signed Vars directly
70 // because Vars in Solver are starting with 0 (not signable with "-")
71 // values in input are staring with 1/-1 and are recalculated to 0-base in this function
73
77 Internal::Lit lit;
78 if (signedVar >= 0) {
79 lit = Internal::mkLit(signedVar - 1, true);
80 } else {
81 lit = Internal::mkLit(-(signedVar + 1), false);
82 }
83 m_ps.push(lit);
84 }
85
87
90 void addMultiple(int Amount, ...);
91
93 void setSign(Internal::Var x, bool sign) {
94 for (int i = 0; i < m_ps.size(); i++) {
95 if (Internal::var(m_ps[i]) == x) {
96 m_ps[i] = Internal::mkLit(x, sign);
97 break;
98 }
99 }
100 }
101
105 for (int i = 0; i < m_ps.size(); i++) {
106 if (Internal::var(m_ps[i]) == x) {
107 return Internal::sign(m_ps[i]);
108 }
109 }
110 std::cout << "Variable not in Clause" << std::endl;
111 return false;
112 }
113
115 //the vec-class doesn't allow to erase elements at a position
117 m_ps.copyTo(help);
118 m_ps.clear();
119 for (int i = 0; i < m_ps.size(); i++) {
120 if (Internal::var(m_ps[i]) != x) {
121 m_ps.push(help[i]);
122 }
123 }
124 }
125
127 static char convertLitSign(Internal::Lit lit) {
128 if (sign(lit) == 0) {
129 return '-';
130 } else {
131 return ' ';
132 }
133 }
134
136 for (int i = 0; i < m_ps.size() - 1; i++) {
137 std::cout << convertLitSign(m_ps[i]) << Internal::var(m_ps[i]) + 1 << " || ";
138 }
139 std::cout << convertLitSign(m_ps[m_ps.size() - 1])
140 << Internal::var(m_ps[m_ps.size() - 1]) + 1 << std::endl;
141 }
142};
143
144using clause = Clause*;
145
151private:
153 std::vector<int> m_vModel;
154
155 void reset() { m_vModel.clear(); }
156
157public:
159
160 Model() {};
161
162 virtual ~Model() { reset(); }
163
165 bool getValue(int var) const {
166 OGDF_ASSERT(var > 0);
167 OGDF_ASSERT(var <= (int)m_vModel.size());
168 return m_vModel[var - 1] != 0;
169 }
170
173 reset();
174
175 m_vModel.reserve(S.model.size());
176 for (int i = 0; i < S.model.size(); i++) {
177 m_vModel.push_back(Internal::toInt(S.model[i]));
178 }
179 }
180
181 void printModel() {
182 for (int i = 0; i < (int)m_vModel.size(); i++) {
183 std::cout << "Var " << i << " = " << m_vModel[i] << " ";
184 }
185 std::cout << std::endl;
186 }
187
188 std::string intToString(const int i) {
189 std::string s;
190 switch (i) {
191 case 0:
192 s = "False";
193 break;
194 case 1:
195 s = "True";
196 break;
197 case 2:
198 s = "Undefined";
199 break;
200 default:
201 s = "";
202 };
203 return s;
204 };
205};
206
214private:
215 std::stringstream m_messages;
216 std::vector<Clause*> m_Clauses;
217
218 void free();
219
220public:
222
223 virtual ~Formula() { free(); }
224
226 void newVar() { Solver::newVar(); }
227
229 void newVars(unsigned int Count) {
230 //proofs if variables from clause are valid (still known to formula)
231 for (unsigned int i = 0; i < Count; i++) {
232 Solver::newVar();
233 }
234 }
235
237
241
243
247
249 template<class Iteratable>
251 auto cl = newClause();
252 for (auto literal : literals) {
253 cl->add(literal);
254 }
255 finalizeClause(cl);
256 }
257
259
264
266 Clause* getClause(const int pos);
267
269 void removeClause(int i);
270
272 int getProblemClauseCount() { return nClauses(); }
273
275 int getClauseCount() { return (int)m_Clauses.size(); }
276
278 int getVariableCount() { return nVars(); }
279
281
286
288
293 bool solve(Model& ReturnModel, double& timeLimit);
294
295 Internal::Var getVarFromLit(const Internal::Lit& lit) { return Internal::var(lit); }
296
300 removeClause(clausePos);
301 m_Clauses[clausePos]->add(signedVar);
302 Solver::addClause(m_Clauses[clausePos]->m_ps);
303 }
304
306 void reset();
307
309 bool readDimacs(const char* filename);
310
312 bool readDimacs(const string& filename);
313
315 bool readDimacs(std::istream& in);
316
318 bool writeDimacs(const char* filename);
319
321 bool writeDimacs(const string& filename);
322
324 bool writeDimacs(std::ostream& f);
325};
326
327}
Basic declarations, included by all source files.
Represents a simple class for clause storage.
Definition Minisat.h:59
static char convertLitSign(Internal::Lit lit)
converts the sign of a lit into char
Definition Minisat.h:127
Internal::vec< Internal::Lit > m_ps
Definition Minisat.h:61
void addMultiple(int Amount,...)
add multiple literals to the clause
void setSign(Internal::Var x, bool sign)
sets the sign of a variable if its present within the clause
Definition Minisat.h:93
void writeToConsole()
Definition Minisat.h:135
void removeLit(Internal::Var x)
Definition Minisat.h:114
bool getSign(Internal::Var x)
returns the sign of a variable if its present within the clause, if the variable is not representet f...
Definition Minisat.h:104
void add(Internal::Var signedVar)
adds a literal to the clause
Definition Minisat.h:76
Clause(const Clause &src)
Definition Minisat.h:65
virtual ~Clause()
Definition Minisat.h:67
The Formula class.
Definition Minisat.h:213
bool readDimacs(const char *filename)
read a formula from a DIMACS file
void removeClause(int i)
removes a complete clause
std::vector< Clause * > m_Clauses
Definition Minisat.h:216
void addClause(const Iteratable &literals)
Add a clause given by a list of literals.
Definition Minisat.h:250
virtual ~Formula()
Definition Minisat.h:223
void newVar()
add a new variable to the formula
Definition Minisat.h:226
void newVars(unsigned int Count)
add multiple new variables to the formula
Definition Minisat.h:229
Clause * getClause(const int pos)
returns a clause at position pos in Formula
bool readDimacs(const string &filename)
read a formula from a DIMACS file
int getProblemClauseCount()
count of problem clauses
Definition Minisat.h:272
int getClauseCount()
count of learned clauses
Definition Minisat.h:275
Clause * newClause()
creates a new clause within the formula. If not all variables are known, missing ones are generated a...
bool solve(Model &ReturnModel, double &timeLimit)
tries to solve the formula with a time limit in milliseconds
bool writeDimacs(std::ostream &f)
write a formula in DIMACS format
void clauseAddLiteral(unsigned int clausePos, Internal::Var signedVar)
adds a literal to a clause and moves clause to the end of list
Definition Minisat.h:299
bool solve(Model &ReturnModel)
tries to solve the formula
bool finalizeNotExtensibleClause(const clause cl)
adds a clause to the formula's solver if all variables are known
std::stringstream m_messages
Definition Minisat.h:215
bool writeDimacs(const char *filename)
write a formula to a DIMACS file
bool writeDimacs(const string &filename)
write a formula to a DIMACS file
bool readDimacs(std::istream &in)
read a formula in DIMACS format
int getVariableCount()
returns varable count currently in solver
Definition Minisat.h:278
Internal::Var getVarFromLit(const Internal::Lit &lit)
Definition Minisat.h:295
void finalizeClause(const clause cl)
adds a clause to the formula's solver. If not all variables are known, missing ones are generated auo...
void reset()
delete all clauses and variables
int size(void) const
Definition Vec.h:63
void clear(bool dealloc=false)
Definition Vec.h:121
void push(void)
Definition Vec.h:73
void copyTo(vec< T > &copy) const
Definition Vec.h:90
Represents a simple class for model storage.
Definition Minisat.h:150
bool getValue(int var) const
returns the value of the assignemt of a variable in the model
Definition Minisat.h:165
virtual ~Model()
Definition Minisat.h:162
Internal::Solver::SolverStatus solverStatus
Definition Minisat.h:158
void setModel(Internal::Solver &S)
sets the model to the model of minsat
Definition Minisat.h:172
std::string intToString(const int i)
Definition Minisat.h:188
std::vector< int > m_vModel
internal storage of a model by minisat
Definition Minisat.h:153
void printModel()
Definition Minisat.h:181
void reset()
Definition Minisat.h:155
#define OGDF_EXPORT
Specifies that a function or class is exported by the OGDF DLL.
Definition config.h:101
#define OGDF_ASSERT(expr)
Assert condition expr. See doc/build.md for more information.
Definition basic.h:41
static MultilevelBuilder * getDoubleFactoredZeroAdjustedMerger()