Open
Graph Drawing
Framework

 v. 2022.02 (Dogwood)
 

Minisat.h
Go to the documentation of this file.
1 
32 #pragma once
33 
34 #include <ogdf/basic/basic.h>
35 
38 
39 #include <stdio.h>
40 #include <iostream>
41 #include <fstream>
42 
43 #include <stdarg.h>
44 
45 #include <string>
46 #include <sstream>
47 
48 #include <vector>
49 
50 namespace Minisat
51 {
52 
53 using std::string;
54 using std::endl;
55 
63 {
64 public:
66  Clause(){}
67  Clause( const Clause &src ) { src.m_ps.copyTo(m_ps); }
68  virtual ~Clause(){}
69 
70  // this function allows to put signed Vars directly
71  // because Vars in Solver are starting with 0 (not signable with "-")
72  // values in input are staring with 1/-1 and are recalculated to 0-base in this function
74 
77  void add(Internal::Var signedVar)
78  {
79  Internal::Lit lit;
80  if ( signedVar >= 0 )
81  {
82  lit = Internal::mkLit(signedVar-1, true);
83  }
84  else
85  {
86  lit = Internal::mkLit(-(signedVar+1), false);
87  }
88  m_ps.push(lit);
89  }
90 
92 
95  void addMultiple ( int Amount, ... );
96 
98  void setSign(Internal::Var x, bool sign)
99  {
100  for ( int i = 0; i < m_ps.size(); i++ )
101  {
102  if (Internal::var(m_ps[i]) == x) {
103  m_ps[i] = Internal::mkLit(x, sign);
104  break;
105  }
106  }
107  }
108 
112  {
113  for (int i = 0; i < m_ps.size(); i++) {
114  if (Internal::var(m_ps[i]) == x) {
115  return Internal::sign(m_ps[i]);
116  }
117  }
118  std::cout << "Variable not in Clause" << std::endl;
119  return false;
120  }
121 
123  {
124  //the vec-class doesn't allow to erase elements at a position
126  m_ps.copyTo(help);
127  m_ps.clear();
128  for ( int i = 0; i < m_ps.size(); i++ )
129  {
130  if (Internal::var(m_ps[i]) != x) {
131  m_ps.push( help[i] );
132  }
133 
134  }
135  }
136 
138  static char convertLitSign(Internal::Lit lit)
139  {
140  if ( sign(lit) == 0 )
141  return '-';
142  else
143  return ' ';
144  }
145 
147  {
148  for ( int i = 0; i < m_ps.size() - 1; i++ )
149  std::cout << convertLitSign( m_ps[i] ) << Internal::var(m_ps[i]) + 1 << " || ";
150  std::cout << convertLitSign( m_ps[ m_ps.size() - 1 ] ) << Internal::var(m_ps[m_ps.size() - 1]) + 1 << std::endl;
151  }
152 };
153 
154 using clause = Clause*;
155 
161 {
162 private:
164  std::vector<int> m_vModel;
165 
166  void reset()
167  {
168  m_vModel.clear();
169  }
170 
171 public:
173 
174  Model() {};
175  virtual ~Model() { reset(); }
176 
178  bool getValue (int var) const
179  {
180  OGDF_ASSERT(var > 0);
181  OGDF_ASSERT(var <= (int)m_vModel.size());
182  return m_vModel[var-1] != 0;
183  }
184 
187  {
188  reset();
189 
190  m_vModel.reserve( S.model.size() );
191  for ( int i = 0; i < S.model.size() ; i++ )
192  {
193  m_vModel.push_back(Internal::toInt(S.model[i]));
194  }
195  }
196 
197  void printModel()
198  {
199  for ( int i = 0; i < (int)m_vModel.size(); i++ )
200  {
201  std::cout << "Var " << i << " = " << m_vModel[i] << " ";
202  }
203  std::cout << std::endl;
204  }
205 
206  std::string intToString ( const int i )
207  {
208  std::string s;
209  switch ( i )
210  {
211  case 0:
212  s = "False";
213  break;
214  case 1:
215  s = "True";
216  break;
217  case 2:
218  s = "Undefined";
219  break;
220  default :
221  s = "";
222  };
223  return s;
224  };
225 };
226 
234 {
235 private:
236  std::stringstream m_messages;
237  std::vector<Clause*> m_Clauses;
238 
239  void free();
240 
241 public:
242  Formula() {}
243  virtual ~Formula(){ free(); }
244 
246 void newVar ()
247 {
248  Solver::newVar();
249 }
250 
252 void newVars ( unsigned int Count )
253 {
254  //proofs if variables from clause are valid (still known to formula)
255  for ( unsigned int i = 0; i < Count; i++ )
256  Solver::newVar();
257 }
258 
260 
263 Clause *newClause();
264 
266 
269 void finalizeClause( const clause cl );
270 
272 template<class Iteratable>
273 void addClause(const Iteratable &literals)
274 {
275  auto cl = newClause();
276  for (auto literal : literals) {
277  cl->add(literal);
278  }
279  finalizeClause(cl);
280 }
281 
283 
287 bool finalizeNotExtensibleClause ( const clause cl );
288 
290 Clause *getClause ( const int pos );
291 
293 void removeClause( int i );
294 
297 {
298  return nClauses();
299 }
300 
303 {
304  return (int)m_Clauses.size();
305 }
306 
309 {
310  return nVars();
311 }
312 
314 
318 bool solve( Model &ReturnModel );
319 
321 
326 bool solve( Model &ReturnModel, double& timeLimit );
327 
329 {
330  return Internal::var(lit);
331 }
332 
335 void clauseAddLiteral(unsigned int clausePos, Internal::Var signedVar)
336 {
337  removeClause( clausePos );
338  m_Clauses[clausePos]->add(signedVar);
339  Solver::addClause( m_Clauses[clausePos]->m_ps );
340 }
341 
343 void reset();
344 
346 bool readDimacs(const char *filename);
347 
349 bool readDimacs(const string &filename);
350 
352 bool readDimacs(std::istream &in);
353 
355 bool writeDimacs(const char *filename);
356 
358 bool writeDimacs(const string &filename);
359 
361 bool writeDimacs(std::ostream &f);
362 };
363 
364 }
Minisat::Clause::m_ps
Internal::vec< Internal::Lit > m_ps
Definition: Minisat.h:65
SolverTypes.h
Minisat::Clause::writeToConsole
void writeToConsole()
Definition: Minisat.h:146
OGDF_ASSERT
#define OGDF_ASSERT(expr)
Assert condition expr. See doc/build.md for more information.
Definition: basic.h:41
Minisat::Model::solverStatus
Internal::Solver::SolverStatus solverStatus
Definition: Minisat.h:172
Minisat::Clause::add
void add(Internal::Var signedVar)
adds a literal to the clause
Definition: Minisat.h:77
Minisat::Model::setModel
void setModel(Internal::Solver &S)
sets the model to the model of minsat
Definition: Minisat.h:186
Minisat::Clause::~Clause
virtual ~Clause()
Definition: Minisat.h:68
Minisat::Formula::newVar
void newVar()
add a new variable to the formula
Definition: Minisat.h:246
Minisat::Formula
The Formula class.
Definition: Minisat.h:233
Minisat::Formula::newVars
void newVars(unsigned int Count)
add multiple new variables to the formula
Definition: Minisat.h:252
backward::Color::reset
@ reset
Definition: backward.hpp:1719
Solver.h
Minisat::Formula::Formula
Formula()
Definition: Minisat.h:242
Minisat::Internal::vec::copyTo
void copyTo(vec< T > &copy) const
Definition: Vec.h:90
Minisat::Clause::Clause
Clause(const Clause &src)
Definition: Minisat.h:67
Minisat::Clause::setSign
void setSign(Internal::Var x, bool sign)
sets the sign of a variable if its present within the clause
Definition: Minisat.h:98
Minisat::Model::m_vModel
std::vector< int > m_vModel
internal storage of a model by minisat
Definition: Minisat.h:164
Minisat::Formula::getProblemClauseCount
int getProblemClauseCount()
count of problem clauses
Definition: Minisat.h:296
Minisat::Formula::m_messages
std::stringstream m_messages
Definition: Minisat.h:236
Minisat::Internal::Solver
Definition: Solver.h:36
Minisat::Internal::Solver::SolverStatus
Definition: Solver.h:61
Minisat::Internal::vec::size
int size(void) const
Definition: Vec.h:63
Minisat::Internal::Lit
Definition: SolverTypes.h:45
Minisat::Formula::m_Clauses
std::vector< Clause * > m_Clauses
Definition: Minisat.h:237
Minisat::Internal::toInt
int toInt(Var v)
Definition: SolverTypes.h:64
Minisat::Model::getValue
bool getValue(int var) const
returns the value of the assignemt of a variable in the model
Definition: Minisat.h:178
Minisat::Model
Represents a simple class for model storage.
Definition: Minisat.h:160
Minisat::Internal::vec::push
void push(void)
Definition: Vec.h:73
Minisat::Clause::convertLitSign
static char convertLitSign(Internal::Lit lit)
converts the sign of a lit into char
Definition: Minisat.h:138
Minisat::Model::Model
Model()
Definition: Minisat.h:174
Minisat::Formula::getClauseCount
int getClauseCount()
count of learned clauses
Definition: Minisat.h:302
Minisat::Model::reset
void reset()
Definition: Minisat.h:166
Minisat::Formula::~Formula
virtual ~Formula()
Definition: Minisat.h:243
Minisat
Definition: Minisat.h:50
Minisat::Internal::sign
bool sign(Lit p)
Definition: SolverTypes.h:60
Minisat::Clause::getSign
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:111
Minisat::Internal::vec
Definition: Vec.h:38
Minisat::Clause
Represents a simple class for clause storage.
Definition: Minisat.h:62
basic.h
Basic declarations, included by all source files.
Minisat::Internal::vec::clear
void clear(bool dealloc=false)
Definition: Vec.h:121
Minisat::Formula::addClause
void addClause(const Iteratable &literals)
Add a clause given by a list of literals.
Definition: Minisat.h:273
Minisat::Internal::mkLit
Lit mkLit(Var var, bool sign=false)
Definition: SolverTypes.h:57
OGDF_EXPORT
#define OGDF_EXPORT
Specifies that a function or class is exported by the OGDF DLL.
Definition: config.h:99
Minisat::Internal::Solver::model
vec< lbool > model
Definition: Solver.h:126
Minisat::Model::intToString
std::string intToString(const int i)
Definition: Minisat.h:206
Minisat::Clause::Clause
Clause()
Definition: Minisat.h:66
Minisat::Formula::clauseAddLiteral
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:335
Minisat::Formula::getVarFromLit
Internal::Var getVarFromLit(const Internal::Lit &lit)
Definition: Minisat.h:328
Minisat::Internal::var
int var(Lit p)
Definition: SolverTypes.h:61
Minisat::Model::printModel
void printModel()
Definition: Minisat.h:197
Minisat::Clause::removeLit
void removeLit(Internal::Var x)
Definition: Minisat.h:122
Minisat::Formula::getVariableCount
int getVariableCount()
returns varable count currently in solver
Definition: Minisat.h:308
Minisat::Internal::Var
int Var
Definition: SolverTypes.h:41
Minisat::Model::~Model
virtual ~Model()
Definition: Minisat.h:175