#pragma GCC optimize("O3") #include // clang-format off using namespace std; using ll = long long int; #define all(v) (v).begin(),(v).end() #define repeat(cnt,l) for(typename remove_const::type>::type cnt={};(cnt)<(l);++(cnt)) #define rrepeat(cnt,l) for(auto cnt=(l)-1;0<=(cnt);--(cnt)) #define iterate(cnt,b,e) for(auto cnt=(b);(cnt)!=(e);++(cnt)) #define upto(cnt,b,e,step) for(auto cnt=(b);(cnt)<=(e);(cnt)+=(step)) #define downto(cnt,b,e,step) for(auto cnt=(b);(e)<=(cnt);(cnt)-=(step)) const long long MD = 998244353; const long double PI = 3.1415926535897932384626433832795L; template inline ostream& operator <<(ostream &o, const pair p) { o << '(' << p.first << ':' << p.second << ')'; return o; } template inline T& chmax(T& to, const T& val) { return to = max(to, val); } template inline T& chmin(T& to, const T& val) { return to = min(to, val); } void bye(string s, int code = 0) { cout << s << endl; exit(code); } mt19937_64 randdev(8901016); template::value>::type* = nullptr> inline T rand(T l, T h, Random& rand = randdev) { return uniform_int_distribution(l, h)(rand); } template::value>::type* = nullptr> inline T rand(T l, T h, Random& rand = randdev) { return uniform_real_distribution(l, h)(rand); }template static ostream& operator<<(ostream& o, const std::vector& v) { o << "[ "; for(const auto& e : v) o< struct MyRangeFormat{ I b,e; MyRangeFormat(I _b, I _e):b(_b),e(_e){} }; template static ostream& operator<<(ostream& o, const MyRangeFormat& f) { o << "[ "; iterate(i,f.b,f.e) o<<*i<<' '; return o << ']'; } template struct MyMatrixFormat{ const I& p; long long n, m; MyMatrixFormat(const I& _p, long long _n, long long _m):p(_p),n(_n),m(_m){} }; template static ostream& operator<<(ostream& o, const MyMatrixFormat& f) { o<<'\n'; repeat(i,(f.n)) { repeat(j,f.m) o<(m,m+w)) #define FMTR(b,e) (MyRangeFormat(b,e)) #define FMTV(v) FMTR(v.begin(),v.end()) #define FMTM(m,h,w) (MyMatrixFormat(m,h,w)) #if defined(_WIN32) || defined(_WIN64) #define getc_x _getc_nolock #define putc_x _putc_nolock #elif defined(__GNUC__) #define getc_x getc_unlocked #define putc_x putc_unlocked #else #define getc_x getc #define putc_x putc #endif class MaiScanner { FILE* fp_; constexpr bool isvisiblechar(char c) noexcept { return (0x21<=(c)&&(c)<=0x7E); } public: inline MaiScanner(FILE* fp):fp_(fp){} template void input_integer(T& var) noexcept { var = 0; T sign = 1; int cc = getc_x(fp_); for (; cc < '0' || '9' < cc; cc = getc_x(fp_)) if (cc == '-') sign = -1; for (; '0' <= cc && cc <= '9'; cc = getc_x(fp_)) var = (var << 3) + (var << 1) + cc - '0'; var = var * sign; } inline int c() noexcept { return getc_x(fp_); } template::value, nullptr_t>::type = nullptr> inline MaiScanner& operator>>(T& var) noexcept { input_integer(var); return *this; } inline MaiScanner& operator>>(string& var) { int cc = getc_x(fp_); for (; !isvisiblechar(cc); cc = getc_x(fp_)); for (; isvisiblechar(cc); cc = getc_x(fp_)) var.push_back(cc); return *this; } template inline void in(IT begin, IT end) { for (auto it = begin; it != end; ++it) *this >> *it; } }; class MaiPrinter { FILE* fp_; public: inline MaiPrinter(FILE* fp):fp_(fp){} template void output_integer(T var) noexcept { if (var == 0) { putc_x('0', fp_); return; } if (var < 0) putc_x('-', fp_), var = -var; char stack[32]; int stack_p = 0; while (var) stack[stack_p++] = '0' + (var % 10), var /= 10; while (stack_p) putc_x(stack[--stack_p], fp_); } inline MaiPrinter& operator<<(char c) noexcept { putc_x(c, fp_); return *this; } template::value, nullptr_t>::type = nullptr> inline MaiPrinter& operator<<(T var) noexcept { output_integer(var); return *this; } inline MaiPrinter& operator<<(const char* str_p) noexcept { while (*str_p) putc_x(*(str_p++), fp_); return *this; } inline MaiPrinter& operator<<(const string& str) { const char* p = str.c_str(); const char* l = p + str.size(); while (p < l) putc_x(*p++, fp_); return *this; } template void join(IT begin, IT end, char sep = ' ') { for (bool b = 0; begin != end; ++begin, b = 1) b ? *this << sep << *begin : *this << *begin; } }; MaiScanner scanner(stdin); MaiPrinter printer(stdout); // clang-format on #ifndef TOGASAT_HPP #define TOGASAT_HPP /* https://github.com/togatoga/togasat/blob/master/LICENSE MIT License Copyright (c) 2019 Hitoshi Togasaki Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. */ /************************************************************ MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson Copyright (c) 2007-2010 Niklas Sorensson Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. ************************************************************/ #include #include #include #include #include #include #include #include #include #include #include #include #include #include // SAT Solver // CDCL Solver // Author togatoga // https://github.com/togatoga/togasat namespace togasat { using Var = int; using CRef = int; using lbool = int; const CRef CRef_Undef = -1; class Solver { private: const lbool l_True = 0; const lbool l_False = 1; const lbool l_Undef = 2; const int var_Undef = -1; // Literal struct Lit { int x; inline bool operator==(Lit p) const { return x == p.x; } inline bool operator!=(Lit p) const { return x != p.x; } inline bool operator<(Lit p) const { return x < p.x; } inline Lit operator~() { Lit q; q.x = x ^ 1; return q; } }; inline Lit mkLit(Var var, bool sign) { Lit p; p.x = var + var + sign; return p; }; inline bool sign(Lit p) const { return p.x & 1; } inline int var(Lit p) const { return p.x >> 1; } inline int toInt(Var v) { return v; } inline int toInt(Lit p) { return p.x; } inline Lit toLit(int x) { Lit p; p.x = x; return p; } const Lit lit_Undef = {-2}; const Lit lit_Error = {-1}; // lifted boolean // VarData struct VarData { CRef reason; int level; }; inline VarData mkVarData(CRef cr, int l) { VarData d = {cr, l}; return d; } // Watcher struct Watcher { CRef cref; Lit blocker; Watcher() {} Watcher(CRef cr, Lit p) : cref(cr), blocker(p) {} bool operator==(const Watcher &w) const { return cref == w.cref; } bool operator!=(const Watcher &w) const { return cref != w.cref; } }; // Clause class Clause { public: struct { bool learnt; int size; } header; std::vector data; //(x1 v x2 v not x3) Clause() {} Clause(const std::vector &ps, bool learnt) { header.learnt = learnt; header.size = ps.size(); // data = move(ps); data.resize(header.size); for (int i = 0; i < ps.size(); i++) { data[i] = ps[i]; // //data.emplace_back(ps[i]); } } int size() const { return header.size; } bool learnt() const { return header.learnt; } Lit &operator[](int i) { return data[i]; } Lit operator[](int i) const { return data[i]; } }; CRef allocClause(std::vector &ps, bool learnt = false) { static CRef res = 0; ca[res] = std::move(Clause(ps, learnt)); return res++; } public: Var newVar(bool sign = true, bool dvar = true) { int v = nVars(); assigns.emplace_back(l_Undef); vardata.emplace_back(mkVarData(CRef_Undef, 0)); activity.emplace_back(0.0); seen.push_back(false); polarity.push_back(sign); decision.push_back(0); setDecisionVar(v, dvar); return v; } bool addClause_(std::vector &ps) { // std::sort(ps.begin(), ps.end()); // empty clause if (ps.size() == 0) { return false; } else if (ps.size() == 1) { uncheckedEnqueue(ps[0]); } else { CRef cr = allocClause(ps, false); // clauses.insert(cr); attachClause(cr); } return true; } void attachClause(CRef cr) { const Clause &c = ca[cr]; assert(c.size() > 1); watches[(~c[0]).x].emplace_back(Watcher(cr, c[1])); watches[(~c[1]).x].emplace_back(Watcher(cr, c[0])); } // Input void readClause(const std::string &line, std::vector &lits) { lits.clear(); int parsed_lit, var; parsed_lit = var = 0; bool neg = false; std::stringstream ss(line); while (ss) { int val; ss >> val; if (val == 0) break; var = abs(val) - 1; while (var >= nVars()) { newVar(); } lits.emplace_back(val > 0 ? mkLit(var, false) : mkLit(var, true)); } } std::unordered_map ca; // store clauses std::unordered_set clauses; // original problem; std::unordered_set learnts; std::unordered_map> watches; std::vector vardata; // store reason and level for each variable std::vector polarity; // The preferred polarity of each variable std::vector decision; std::vector seen; // Todo int qhead; std::vector trail; std::vector trail_lim; // Todo rename(not heap) std::set> order_heap; std::vector activity; double var_inc; std::vector model; std::vector conflict; int nVars() const { return vardata.size(); } int decisionLevel() const { return trail_lim.size(); } void newDecisionLevel() { trail_lim.emplace_back(trail.size()); } inline CRef reason(Var x) const { return vardata[x].reason; } inline int level(Var x) const { return vardata[x].level; } inline void varBumpActivity(Var v) { std::pair p = std::make_pair(activity[v], v); activity[v] += var_inc; if (order_heap.erase(p) == 1) { order_heap.emplace(std::make_pair(activity[v], v)); } if (activity[v] > 1e100) { // Rescale std::set> tmp_order; tmp_order = std::move(order_heap); order_heap.clear(); for (int i = 0; i < nVars(); i++) { activity[i] *= 1e-100; } for (auto &val : tmp_order) { order_heap.emplace(std::make_pair(activity[val.second], val.second)); } var_inc *= 1e-100; } } bool satisfied(const Clause &c) const { for (int i = 0; i < c.size(); i++) { if (value(c[i]) == l_True) { return true; } } return false; } lbool value(Var p) const { return assigns[p]; } lbool value(Lit p) const { if (assigns[var(p)] == l_Undef) { return l_Undef; } return assigns[var(p)] ^ sign(p); } void setDecisionVar(Var v, bool b) { decision[v] = b; order_heap.emplace(std::make_pair(0.0, v)); } void uncheckedEnqueue(Lit p, CRef from = CRef_Undef) { assert(value(p) == l_Undef); assigns[var(p)] = sign(p); vardata[var(p)] = std::move(mkVarData(from, decisionLevel())); trail.emplace_back(p); } // decision Lit pickBranchLit() { Var next = var_Undef; while (next == var_Undef or value(next) != l_Undef) { if (order_heap.empty()) { next = var_Undef; break; } else { auto p = *order_heap.rbegin(); next = p.second; order_heap.erase(p); } } return next == var_Undef ? lit_Undef : mkLit(next, polarity[next]); } // clause learning void analyze(CRef confl, std::vector &out_learnt, int &out_btlevel) { int pathC = 0; Lit p = lit_Undef; int index = trail.size() - 1; out_learnt.emplace_back(mkLit(0, false)); do { assert(confl != CRef_Undef); Clause &c = ca[confl]; for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++) { Lit q = c[j]; if (not seen[var(q)] and level(var(q)) > 0) { varBumpActivity(var(q)); seen[var(q)] = 1; if (level(var(q)) >= decisionLevel()) { pathC++; } else { out_learnt.emplace_back(q); } } } while (not seen[var(trail[index--])]) ; p = trail[index + 1]; confl = reason(var(p)); seen[var(p)] = 0; pathC--; } while (pathC > 0); out_learnt[0] = ~p; // unit clause if (out_learnt.size() == 1) { out_btlevel = 0; } else { int max_i = 1; for (int i = 2; i < out_learnt.size(); i++) { if (level(var(out_learnt[i])) > level(var(out_learnt[max_i]))) { max_i = i; } } Lit p = out_learnt[max_i]; out_learnt[max_i] = out_learnt[1]; out_learnt[1] = p; out_btlevel = level(var(p)); } for (int i = 0; i < out_learnt.size(); i++) { seen[var(out_learnt[i])] = false; } } // backtrack void cancelUntil(int level) { if (decisionLevel() > level) { for (int c = trail.size() - 1; c >= trail_lim[level]; c--) { Var x = var(trail[c]); assigns[x] = l_Undef; polarity[x] = sign(trail[c]); order_heap.emplace(std::make_pair(activity[x], x)); } qhead = trail_lim[level]; trail.erase(trail.end() - (trail.size() - trail_lim[level]), trail.end()); trail_lim.erase(trail_lim.end() - (trail_lim.size() - level), trail_lim.end()); } } CRef propagate() { CRef confl = CRef_Undef; int num_props = 0; while (qhead < trail.size()) { Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. std::vector &ws = watches[p.x]; std::vector::iterator i, j, end; num_props++; for (i = j = ws.begin(), end = i + ws.size(); i != end;) { // Try to avoid inspecting the clause: Lit blocker = i->blocker; if (value(blocker) == l_True) { *j++ = *i++; continue; } CRef cr = i->cref; Clause &c = ca[cr]; Lit false_lit = ~p; if (c[0] == false_lit) c[0] = c[1], c[1] = false_lit; assert(c[1] == false_lit); i++; Lit first = c[0]; Watcher w = Watcher(cr, first); if (first != blocker && value(first) == l_True) { *j++ = w; continue; } // Look for new watch: for (int k = 2; k < c.size(); k++) if (value(c[k]) != l_False) { c[1] = c[k]; c[k] = false_lit; watches[(~c[1]).x].emplace_back(w); goto NextClause; } *j++ = w; if (value(first) == l_False) { // conflict confl = cr; qhead = trail.size(); while (i < end) *j++ = *i++; } else { uncheckedEnqueue(first, cr); } NextClause:; } int size = i - j; ws.erase(ws.end() - size, ws.end()); } return confl; } static double luby(double y, int x) { // Find the finite subsequence that contains index 'x', and the // size of that subsequence: int size, seq; for (size = 1, seq = 0; size < x + 1; seq++, size = 2 * size + 1) ; while (size - 1 != x) { size = (size - 1) >> 1; seq--; x = x % size; } return pow(y, seq); } lbool search(int nof_conflicts) { int backtrack_level; std::vector learnt_clause; learnt_clause.emplace_back(mkLit(-1, false)); int conflictC = 0; while (true) { CRef confl = propagate(); if (confl != CRef_Undef) { // CONFLICT conflictC++; if (decisionLevel() == 0) return l_False; learnt_clause.clear(); analyze(confl, learnt_clause, backtrack_level); cancelUntil(backtrack_level); if (learnt_clause.size() == 1) { uncheckedEnqueue(learnt_clause[0]); } else { CRef cr = allocClause(learnt_clause, true); // learnts.insert(cr); attachClause(cr); uncheckedEnqueue(learnt_clause[0], cr); } // varDecay var_inc *= 1.05; } else { // NO CONFLICT if ((nof_conflicts >= 0 and conflictC >= nof_conflicts)) { cancelUntil(0); return l_Undef; } Lit next = pickBranchLit(); if (next == lit_Undef) { return l_True; } newDecisionLevel(); uncheckedEnqueue(next); } } }; public: std::vector assigns; // The current assignments (ex assigns[0] = 0 -> // X1 = True, assigns[1] = 1 -> X2 = False) lbool answer; // SATISFIABLE 0 UNSATISFIABLE 1 UNKNOWN 2 Solver() { qhead = 0; } void parseDimacsProblem(std::string problem_name) { std::vector lits; int vars = 0; int clauses = 0; std::string line; std::ifstream ifs(problem_name, std::ios_base::in); while (ifs.good()) { getline(ifs, line); if (line.size() > 0) { if (line[0] == 'p') { sscanf(line.c_str(), "p cnf %d %d", &vars, &clauses); } else if (line[0] == 'c' or line[0] == 'p') { continue; } else { readClause(line, lits); if (lits.size() > 0) addClause_(lits); } } } ifs.close(); } lbool solve() { model.clear(); conflict.clear(); lbool status = l_Undef; answer = l_Undef; var_inc = 1.01; int curr_restarts = 0; double restart_inc = 2; double restart_first = 100; while (status == l_Undef) { double rest_base = luby(restart_inc, curr_restarts); status = search(rest_base * restart_first); curr_restarts++; } answer = status; return status; }; void addClause(const std::vector &clause) { std::vector lits; lits.resize(clause.size()); for (int i = 0; i < clause.size(); i++) { int var = abs(clause[i]) - 1; while (var >= nVars()) newVar(); lits[i] = std::move((clause[i] > 0 ? mkLit(var, false) : mkLit(var, true))); } addClause_(lits); } void printAnswer() { if (answer == 0) { std::cout << "SAT" << std::endl; for (int i = 0; i < assigns.size(); i++) { if (assigns[i] == 0) { std::cout << (i + 1) << " "; } else { std::cout << -(i + 1) << " "; } } std::cout << "0" << std::endl; } else { std::cout << "UNSAT" << std::endl; } } }; } // namespace togasat #endif // TOGASAT_HPP // // int main_test() { // 0, 1, 1 // (x1 + x2 + -x3)(-x1 + x2 + x3)(-x1 + -x2 + x3)(x1 + -x2 + x3)(x1 + x2 + x3) // unsatisfiableにならないような… togasat::Solver solver; solver.addClause({1, 2, -3}); solver.addClause({-1, 2, 3}); solver.addClause({-1, -2, 3}); solver.addClause({1, -2, 3}); // solver.addClause({-1, -2, 3}); // solver.addClause({1, -2, -3}); // solver.addClause({1, 2, -3}); // solver.addClause({-1, 2, -3}); solver.addClause({1, 2, 3}); // solver.addClause({-1, -2, -3}); auto stat = solver.solve(); solver.printAnswer(); return 0; } array, 3> C[2048]; int main() { // return main_test(); repeat(i, 2048) { int a, b, c, x, y, z; scanner >> a >> b >> c >> x >> y >> z; // a = rand(0, 255); // b = rand(0, 255); // c = rand(0, 255); // x = rand(0, 1); // y = rand(0, 1); // z = rand(0, 1); C[i][0] = make_pair(a, x); C[i][1] = make_pair(b, y); C[i][2] = make_pair(c, z); } int g_best = -1; string g_best_str = ""; // upto(T, 800, 1200, 200) { { const int T = 800; togasat::Solver solver; repeat(i, 256) solver.newVar(); repeat(i, T) { vector cl(3); repeat(j, 3) { cl[j] = (C[i][j].first + 1)*(C[i][j].second*2-1); } solver.addClause(cl); } auto stat = solver.solve(); // solver.printAnswer(); int best = 0; repeat(i, 2048) { bool ok = false; repeat(j, 3) ok |= C[i][j].second == !solver.assigns[C[i][j].first]; // repeat(j, 3) cout << (C[i][j].second == !solver.assigns[C[i][j].first]); // cout << endl; if (!ok) break; best = i + 1; } if (best > g_best) { g_best = best; g_best_str = ""; repeat(i, 256) { g_best_str.push_back('0' + !solver.assigns[i]); } } } reverse(all(g_best_str)); clog << g_best<