Open
Graph Drawing
Framework

 v. 2023.09 (Elderberry)
 

SimpSolver.h
Go to the documentation of this file.
1 /************************************************************************************[SimpSolver.h]
2 Copyright (c) 2006, Niklas Een, Niklas Sorensson
3 Copyright (c) 2007-2010, Niklas Sorensson
4 
5 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
6 associated documentation files (the "Software"), to deal in the Software without restriction,
7 including without limitation the rights to use, copy, modify, merge, publish, distribute,
8 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
10 
11 The above copyright notice and this permission notice shall be included in all copies or
12 substantial portions of the Software.
13 
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
15 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
16 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
17 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
18 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
19 **************************************************************************************************/
20 
21 #pragma once
22 
25 
26 
27 #pragma GCC visibility push(default)
28 namespace Minisat {
29 namespace Internal {
30 
31 //=================================================================================================
32 
33 
34 class SimpSolver : public Solver {
35  public:
36  // Constructor/Destructor:
37  //
38  SimpSolver();
39  ~SimpSolver();
40 
41  // Problem specification:
42  //
43  Var newVar (bool polarity = true, bool dvar = true);
44  bool addClause (const vec<Lit>& ps);
45  bool addEmptyClause(); // Add the empty clause to the solver.
46  bool addClause (Lit p); // Add a unit clause to the solver.
47  bool addClause (Lit p, Lit q); // Add a binary clause to the solver.
48  bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver.
49  bool addClause_( vec<Lit>& ps);
50  bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction).
51 
52  // Variable mode:
53  //
54  void setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.
55  bool isEliminated(Var v) const;
56 
57  // Solving:
58  //
59  bool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
60  lbool solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
61  bool solve ( bool do_simp = true, bool turn_off_simp = false);
62  bool solve (Lit p , bool do_simp = true, bool turn_off_simp = false);
63  bool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false);
64  bool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
65  bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification.
66 
67  // Memory managment:
68  //
69  virtual void garbageCollect() override;
70 
71 
72  // Generate a (possibly simplified) DIMACS file:
73  //
74 #if 0
75  void toDimacs (const char* file, const vec<Lit>& assumps);
76  void toDimacs (const char* file);
77  void toDimacs (const char* file, Lit p);
78  void toDimacs (const char* file, Lit p, Lit q);
79  void toDimacs (const char* file, Lit p, Lit q, Lit r);
80 #endif
81 
82  // Mode of operation:
83  //
84  int grow; // Allow a variable elimination step to grow by a number of clauses (default to zero).
85  int clause_lim; // Variables are not eliminated if it produces a resolvent with a length above this limit.
86  // -1 means no limit.
87  int subsumption_lim; // Do not check if subsumption against a clause larger than this. -1 means no limit.
88  double simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac').
89 
90  bool use_asymm; // Shrink clauses by asymmetric branching.
91  bool use_rcheck; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
92  bool use_elim; // Perform variable elimination.
93 
94  // Statistics:
95  //
96  int merges;
99 
100  protected:
101 
102  // Helper structures:
103  //
104  struct ElimLt {
105  const vec<int>& n_occ;
106  explicit ElimLt(const vec<int>& no) : n_occ(no) {}
107 
108  // TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating
109  // 32-bit implementation instead then, but this will have to do for now.
110  uint64_t cost (Var x) const { return (uint64_t)n_occ[toInt(mkLit(x))] * (uint64_t)n_occ[toInt(~mkLit(x))]; }
111  bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
112 
113 #if 0
114  // TODO: investigate this order alternative more.
115  bool operator()(Var x, Var y) const {
116  int c_x = cost(x);
117  int c_y = cost(y);
118  return c_x < c_y || c_x == c_y && x < y; }
119 #endif
120  };
121 
122  struct ClauseDeleted {
124  explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
125  bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } };
126 
127  // Solver state:
128  //
142 
143  // Temporaries:
144  //
146 
147  // Main internal methods:
148  //
149  lbool solve_ (bool do_simp = true, bool turn_off_simp = false);
150  bool asymm (Var v, CRef cr);
151  bool asymmVar (Var v);
152  void updateElimHeap (Var v);
153  void gatherTouchedClauses ();
154  bool merge (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
155  bool merge (const Clause& _ps, const Clause& _qs, Var v, int& size);
156  bool backwardSubsumptionCheck (bool verbose = false);
157  bool eliminateVar (Var v);
158  void extendModel ();
159 
160  void removeClause (CRef cr);
161  bool strengthenClause (CRef cr, Lit l);
162  void cleanUpClauses ();
163  bool implied (const vec<Lit>& c);
164  void relocAll (ClauseAllocator& to);
165 };
166 
167 
168 //=================================================================================================
169 // Implementation of inline methods:
170 
171 
172 inline bool SimpSolver::isEliminated (Var v) const { return (eliminated[v] != 0); }
174  assert(use_simplification);
175 #if 0
176  if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
177 #endif
178  if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
179  elim_heap.update(v); }
180 
181 
182 inline bool SimpSolver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); }
183 inline bool SimpSolver::addEmptyClause() { add_tmp.clear(); return addClause_(add_tmp); }
184 inline bool SimpSolver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
185 inline bool SimpSolver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
186 inline bool SimpSolver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
187 inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
188 
189 inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }
190 inline bool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; }
191 inline bool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; }
192 inline bool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; }
193 inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
194  budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; }
195 
196 inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
197  assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
198 
199 //=================================================================================================
200 } // namespace Internal
201 } // namespace Minisat
202 #pragma GCC visibility pop
Minisat::Internal::Heap
Definition: Heap.h:34
Minisat::Internal::SimpSolver::subsumption_lim
int subsumption_lim
Definition: SimpSolver.h:87
Minisat::Internal::SimpSolver::n_touched
int n_touched
Definition: SimpSolver.h:141
Minisat::Internal::OccLists
Definition: SolverTypes.h:274
Minisat::Internal::SimpSolver::merge
bool merge(const Clause &_ps, const Clause &_qs, Var v, vec< Lit > &out_clause)
Minisat::Internal::SimpSolver::asymm
bool asymm(Var v, CRef cr)
Minisat::Internal::SimpSolver::touched
vec< char > touched
Definition: SimpSolver.h:132
Minisat::Internal::SimpSolver::addEmptyClause
bool addEmptyClause()
Definition: SimpSolver.h:183
Minisat::Internal::SimpSolver::backwardSubsumptionCheck
bool backwardSubsumptionCheck(bool verbose=false)
Minisat::Internal::SimpSolver::elimorder
int elimorder
Definition: SimpSolver.h:129
Minisat::Internal::SimpSolver::ClauseDeleted::operator()
bool operator()(const CRef &cr) const
Definition: SimpSolver.h:125
Minisat::Internal::SimpSolver::use_elim
bool use_elim
Definition: SimpSolver.h:92
Minisat::Internal::SimpSolver::extendModel
void extendModel()
Minisat::Internal::Solver::solve
bool solve()
Definition: Solver.h:371
Minisat::Internal::SimpSolver::ElimLt::cost
uint64_t cost(Var x) const
Definition: SimpSolver.h:110
Minisat::Internal::SimpSolver::strengthenClause
bool strengthenClause(CRef cr, Lit l)
Minisat::Internal::SimpSolver::clause_lim
int clause_lim
Definition: SimpSolver.h:85
Minisat::Internal::ClauseAllocator
Definition: SolverTypes.h:212
Minisat::Internal::SimpSolver::bwdsub_assigns
int bwdsub_assigns
Definition: SimpSolver.h:140
Minisat::Internal::SimpSolver::ClauseDeleted::ca
const ClauseAllocator & ca
Definition: SimpSolver.h:123
Minisat::Internal::SimpSolver::merges
int merges
Definition: SimpSolver.h:96
Minisat::Internal::Solver::value
lbool value(Var x) const
Definition: Solver.h:340
Minisat::Internal::SimpSolver::newVar
Var newVar(bool polarity=true, bool dvar=true)
Minisat::Internal::Solver::add_tmp
vec< Lit > add_tmp
Definition: Solver.h:218
Minisat::Internal::SimpSolver::elim_heap
Heap< ElimLt > elim_heap
Definition: SimpSolver.h:136
Minisat::Internal::SimpSolver
Definition: SimpSolver.h:34
Minisat::Internal::SimpSolver::solveLimited
lbool solveLimited(const vec< Lit > &assumps, bool do_simp=true, bool turn_off_simp=false)
Definition: SimpSolver.h:196
Solver.h
Minisat::Internal::SimpSolver::addClause_
bool addClause_(vec< Lit > &ps)
Minisat::Internal::SimpSolver::occurs
OccLists< Var, vec< CRef >, ClauseDeleted > occurs
Definition: SimpSolver.h:134
Minisat::Internal::vec::copyTo
void copyTo(vec< T > &copy) const
Definition: Vec.h:91
Minisat::Internal::SimpSolver::SimpSolver
SimpSolver()
Minisat::Internal::Queue< CRef >
Minisat::Internal::SimpSolver::substitute
bool substitute(Var v, Lit x)
Minisat::Internal::SimpSolver::use_asymm
bool use_asymm
Definition: SimpSolver.h:90
Minisat::Internal::SimpSolver::n_occ
vec< int > n_occ
Definition: SimpSolver.h:135
l_True
#define l_True
Definition: SolverTypes.h:86
Minisat::Internal::SimpSolver::garbageCollect
virtual void garbageCollect() override
Minisat::Internal::Solver
Definition: Solver.h:37
r
int r[]
Definition: hierarchical-ranking.cpp:13
Minisat::Internal::SimpSolver::bwdsub_tmpunit
CRef bwdsub_tmpunit
Definition: SimpSolver.h:145
Minisat::Internal::Lit
Definition: SolverTypes.h:46
Minisat::Internal::toInt
int toInt(Var v)
Definition: SolverTypes.h:65
Minisat::Internal::SimpSolver::updateElimHeap
void updateElimHeap(Var v)
Definition: SimpSolver.h:173
Minisat::Internal::SimpSolver::asymm_lits
int asymm_lits
Definition: SimpSolver.h:97
Minisat::Internal::SimpSolver::use_rcheck
bool use_rcheck
Definition: SimpSolver.h:91
Minisat::Internal::SimpSolver::setFrozen
void setFrozen(Var v, bool b)
Definition: SimpSolver.h:187
Minisat::Internal::SimpSolver::~SimpSolver
~SimpSolver()
Minisat::Internal::SimpSolver::asymmVar
bool asymmVar(Var v)
Queue.h
Minisat::Internal::SimpSolver::gatherTouchedClauses
void gatherTouchedClauses()
Minisat::Internal::SimpSolver::ClauseDeleted
Definition: SimpSolver.h:122
Minisat::Internal::SimpSolver::use_simplification
bool use_simplification
Definition: SimpSolver.h:130
Minisat::Internal::lbool
Definition: SolverTypes.h:91
Minisat::Internal::SimpSolver::grow
int grow
Definition: SimpSolver.h:84
Minisat
Definition: Minisat.h:55
Minisat::Internal::Solver::solve_
lbool solve_()
Minisat::Internal::SimpSolver::ElimLt::operator()
bool operator()(Var x, Var y) const
Definition: SimpSolver.h:111
Minisat::Internal::SimpSolver::implied
bool implied(const vec< Lit > &c)
Minisat::Internal::Clause
Definition: SolverTypes.h:137
Minisat::Internal::SimpSolver::eliminateVar
bool eliminateVar(Var v)
Minisat::Internal::SimpSolver::cleanUpClauses
void cleanUpClauses()
Minisat::Internal::SimpSolver::elimclauses
vec< uint32_t > elimclauses
Definition: SimpSolver.h:131
Minisat::Internal::SimpSolver::subsumption_queue
Queue< CRef > subsumption_queue
Definition: SimpSolver.h:137
Minisat::Internal::SimpSolver::ElimLt::n_occ
const vec< int > & n_occ
Definition: SimpSolver.h:105
Minisat::Internal::SimpSolver::eliminate
bool eliminate(bool turn_off_elim=false)
Minisat::Internal::vec
Definition: Vec.h:39
Minisat::Internal::Solver::assumptions
vec< Lit > assumptions
Definition: Solver.h:205
Minisat::Internal::SimpSolver::eliminated
vec< char > eliminated
Definition: SimpSolver.h:139
Minisat::Internal::Solver::budgetOff
void budgetOff()
Definition: Solver.h:362
l_Undef
#define l_Undef
Definition: SolverTypes.h:88
Minisat::Internal::SimpSolver::eliminated_vars
int eliminated_vars
Definition: SimpSolver.h:98
Minisat::Internal::mkLit
Lit mkLit(Var var, bool sign=false)
Definition: SolverTypes.h:58
Minisat::Internal::SimpSolver::frozen
vec< char > frozen
Definition: SimpSolver.h:138
Minisat::Internal::Solver::toDimacs
void toDimacs(std::ostream &out, const vec< Lit > &assumps)
Minisat::Internal::SimpSolver::ElimLt::ElimLt
ElimLt(const vec< int > &no)
Definition: SimpSolver.h:106
Minisat::Internal::Solver::polarity
vec< char > polarity
Definition: Solver.h:197
Minisat::Internal::SimpSolver::removeClause
void removeClause(CRef cr)
Minisat::Internal::SimpSolver::relocAll
void relocAll(ClauseAllocator &to)
Minisat::Internal::SimpSolver::isEliminated
bool isEliminated(Var v) const
Definition: SimpSolver.h:172
Minisat::Internal::SimpSolver::addClause
bool addClause(const vec< Lit > &ps)
Definition: SimpSolver.h:182
Minisat::Internal::SimpSolver::ClauseDeleted::ClauseDeleted
ClauseDeleted(const ClauseAllocator &_ca)
Definition: SimpSolver.h:124
Minisat::Internal::SimpSolver::ElimLt
Definition: SimpSolver.h:104
Minisat::Internal::Var
int Var
Definition: SolverTypes.h:42
Minisat::Internal::CRef
RegionAllocator< uint32_t >::Ref CRef
Definition: SolverTypes.h:130
Minisat::Internal::SimpSolver::simp_garbage_frac
double simp_garbage_frac
Definition: SimpSolver.h:88