1 /***************************************************************************************[SimpSolver.h]
2 Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon
3 CRIL - Univ. Artois, France
4 LRI - Univ. Paris Sud, France (2009-2013)
5 Labri - Univ. Bordeaux, France
7 Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
8 CRIL - Univ. Artois, France
9 Labri - Univ. Bordeaux, France
11 Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
12 Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it
13 is based on. (see below).
15 Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel
16 version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software
17 without restriction, including the rights to use, copy, modify, merge, publish, distribute,
18 sublicence, and/or sell copies of the Software, and to permit persons to whom the Software is
19 furnished to do so, subject to the following conditions:
21 - The above and below copyrights notices and this permission notice shall be included in all
22 copies or substantial portions of the Software;
23 - The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot
24 be used in any competitive event (sat competitions/evaluations) without the express permission of
25 the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event
26 using Glucose Parallel as an embedded SAT engine (single core or not).
29 --------------- Original Minisat Copyrights
31 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
32 Copyright (c) 2007-2010, Niklas Sorensson
34 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
35 associated documentation files (the "Software"), to deal in the Software without restriction,
36 including without limitation the rights to use, copy, modify, merge, publish, distribute,
37 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
38 furnished to do so, subject to the following conditions:
40 The above copyright notice and this permission notice shall be included in all copies or
41 substantial portions of the Software.
43 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
44 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
45 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
46 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
47 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
48 **************************************************************************************************/
50 #ifndef Glucose_SimpSolver_h
51 #define Glucose_SimpSolver_h
53 #include "mtl/Queue.h"
54 #include "core/Solver.h"
55 #include "mtl/Clone.h"
59 //=================================================================================================
62 class SimpSolver : public Solver {
64 // Constructor/Destructor:
69 SimpSolver(const SimpSolver &s);
75 virtual Clone* clone() const {
76 return new SimpSolver(*this);
80 // Problem specification:
82 virtual Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
83 bool addClause (const vec<Lit>& ps);
84 bool addEmptyClause(); // Add the empty clause to the solver.
85 bool addClause (Lit p); // Add a unit clause to the solver.
86 bool addClause (Lit p, Lit q); // Add a binary clause to the solver.
87 bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver.
88 virtual bool addClause_( vec<Lit>& ps);
89 bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction).
93 void setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.
94 bool isEliminated(Var v) const;
98 bool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
99 lbool solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
100 bool solve ( bool do_simp = true, bool turn_off_simp = false);
101 bool solve (Lit p , bool do_simp = true, bool turn_off_simp = false);
102 bool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false);
103 bool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
104 bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification.
108 virtual void garbageCollect();
111 // Generate a (possibly simplified) DIMACS file:
114 void toDimacs (const char* file, const vec<Lit>& assumps);
115 void toDimacs (const char* file);
116 void toDimacs (const char* file, Lit p);
117 void toDimacs (const char* file, Lit p, Lit q);
118 void toDimacs (const char* file, Lit p, Lit q, Lit r);
121 // Mode of operation:
124 int grow; // Allow a variable elimination step to grow by a number of clauses (default to zero).
125 int clause_lim; // Variables are not eliminated if it produces a resolvent with a length above this limit.
126 // -1 means no limit.
127 int subsumption_lim; // Do not check if subsumption against a clause larger than this. -1 means no limit.
128 double simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac').
130 bool use_asymm; // Shrink clauses by asymmetric branching.
131 bool use_rcheck; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
132 bool use_elim; // Perform variable elimination.
141 // Helper structures:
144 const vec<int>& n_occ;
145 explicit ElimLt(const vec<int>& no) : n_occ(no) {}
147 // TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating
148 // 32-bit implementation instead then, but this will have to do for now.
149 uint64_t cost (Var x) const { return (uint64_t)n_occ[toInt(mkLit(x))] * (uint64_t)n_occ[toInt(~mkLit(x))]; }
150 bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
152 // TODO: investigate this order alternative more.
153 // bool operator()(Var x, Var y) const {
154 // int c_x = cost(x);
155 // int c_y = cost(y);
156 // return c_x < c_y || c_x == c_y && x < y; }
159 struct ClauseDeleted {
160 const ClauseAllocator& ca;
161 explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
162 bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } };
167 bool use_simplification;
168 vec<uint32_t> elimclauses;
170 OccLists<Var, vec<CRef>, ClauseDeleted>
173 Heap<ElimLt> elim_heap;
174 Queue<CRef> subsumption_queue;
176 vec<char> eliminated;
184 // Main internal methods:
186 virtual lbool solve_ (bool do_simp = true, bool turn_off_simp = false);
187 bool asymm (Var v, CRef cr);
188 bool asymmVar (Var v);
189 void updateElimHeap (Var v);
190 void gatherTouchedClauses ();
191 bool merge (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
192 bool merge (const Clause& _ps, const Clause& _qs, Var v, int& size);
193 bool backwardSubsumptionCheck (bool verbose = false);
194 bool eliminateVar (Var v);
196 void unsatExplanation();
197 void removeClause (CRef cr,bool inPurgatory=false);
198 bool strengthenClause (CRef cr, Lit l);
199 void cleanUpClauses ();
200 bool implied (const vec<Lit>& c);
201 virtual void relocAll (ClauseAllocator& to);
205 //=================================================================================================
206 // Implementation of inline methods:
209 inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; }
210 inline void SimpSolver::updateElimHeap(Var v) {
211 assert(use_simplification);
212 // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
213 if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
214 elim_heap.update(v); }
217 inline bool SimpSolver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); }
218 inline bool SimpSolver::addEmptyClause() { add_tmp.clear(); return addClause_(add_tmp); }
219 inline bool SimpSolver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
220 inline bool SimpSolver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
221 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); }
222 inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
224 inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }
225 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; }
226 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; }
227 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; }
228 inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
229 budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; }
231 inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
232 assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
234 //=================================================================================================