Open
Graph Drawing
Framework

 v. 2023.09 (Elderberry)
 

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