#956181 (C++17) No.5005 3-SAT

• 問題: No.5005 3-SAT
• ユーザー: bin101
• 提出日時: 2024-02-27 23:55:52
• 言語: C++17 (gcc 12.3.0 + boost 1.83.0)
• 結果: AC
• 実行時間: 1,394 ms / 2,000 ms
• コード長: 16,469 bytes
• コンパイル時間: 5,318 ms
• コンパイル使用メモリ: 260,132 KB
• 実行使用メモリ: 6,676 KB
• スコア: 95,685
• 最終ジャッジ日時: 2024-02-27 23:57:48
• 合計ジャッジ時間: 112,685 ms
• ジャッジサーバーID （参考情報）: judge11 / judge12

入力	結果	実行時間; 実行使用メモリ
testcase_00	AC	1,032 ms; 6,676 KB
testcase_01	AC	1,010 ms; 6,676 KB
testcase_02	AC	1,010 ms; 6,676 KB
testcase_03	AC	1,020 ms; 6,676 KB
testcase_04	AC	1,011 ms; 6,676 KB
testcase_05	AC	1,011 ms; 6,676 KB
testcase_06	AC	1,003 ms; 6,676 KB
testcase_07	AC	1,014 ms; 6,676 KB
testcase_08	AC	1,004 ms; 6,676 KB
testcase_09	AC	1,003 ms; 6,676 KB
testcase_10	AC	1,004 ms; 6,676 KB
testcase_11	AC	1,174 ms; 6,676 KB
testcase_12	AC	1,082 ms; 6,676 KB
testcase_13	AC	1,010 ms; 6,676 KB
testcase_14	AC	1,015 ms; 6,676 KB
testcase_15	AC	1,011 ms; 6,676 KB
testcase_16	AC	1,058 ms; 6,676 KB
testcase_17	AC	1,007 ms; 6,676 KB
testcase_18	AC	1,007 ms; 6,676 KB
testcase_19	AC	1,015 ms; 6,676 KB
testcase_20	AC	1,003 ms; 6,676 KB
testcase_21	AC	1,020 ms; 6,676 KB
testcase_22	AC	1,006 ms; 6,676 KB
testcase_23	AC	1,146 ms; 6,676 KB
testcase_24	AC	1,008 ms; 6,676 KB
testcase_25	AC	1,056 ms; 6,676 KB
testcase_26	AC	1,003 ms; 6,676 KB
testcase_27	AC	1,011 ms; 6,676 KB
testcase_28	AC	1,013 ms; 6,676 KB
testcase_29	AC	1,003 ms; 6,676 KB
testcase_30	AC	1,015 ms; 6,676 KB
testcase_31	AC	1,055 ms; 6,676 KB
testcase_32	AC	1,005 ms; 6,676 KB
testcase_33	AC	1,012 ms; 6,676 KB
testcase_34	AC	1,012 ms; 6,676 KB
testcase_35	AC	1,008 ms; 6,676 KB
testcase_36	AC	1,039 ms; 6,676 KB
testcase_37	AC	1,004 ms; 6,676 KB
testcase_38	AC	1,035 ms; 6,676 KB
testcase_39	AC	1,005 ms; 6,676 KB
testcase_40	AC	1,003 ms; 6,676 KB
testcase_41	AC	1,008 ms; 6,676 KB
testcase_42	AC	1,016 ms; 6,676 KB
testcase_43	AC	1,394 ms; 6,676 KB
testcase_44	AC	1,042 ms; 6,676 KB
testcase_45	AC	1,028 ms; 6,676 KB
testcase_46	AC	1,021 ms; 6,676 KB
testcase_47	AC	1,021 ms; 6,676 KB
testcase_48	AC	1,082 ms; 6,676 KB
testcase_49	AC	1,021 ms; 6,676 KB
testcase_50	AC	1,109 ms; 6,676 KB
testcase_51	AC	1,010 ms; 6,676 KB
testcase_52	AC	1,004 ms; 6,676 KB
testcase_53	AC	1,016 ms; 6,676 KB
testcase_54	AC	1,015 ms; 6,676 KB
testcase_55	AC	1,177 ms; 6,676 KB
testcase_56	AC	1,004 ms; 6,676 KB
testcase_57	AC	1,004 ms; 6,676 KB
testcase_58	AC	1,051 ms; 6,676 KB
testcase_59	AC	1,008 ms; 6,676 KB
testcase_60	AC	1,012 ms; 6,676 KB
testcase_61	AC	1,037 ms; 6,676 KB
testcase_62	AC	1,054 ms; 6,676 KB
testcase_63	AC	1,010 ms; 6,676 KB
testcase_64	AC	1,044 ms; 6,676 KB
testcase_65	AC	1,066 ms; 6,676 KB
testcase_66	AC	1,013 ms; 6,676 KB
testcase_67	AC	1,071 ms; 6,676 KB
testcase_68	AC	1,005 ms; 6,676 KB
testcase_69	AC	1,033 ms; 6,676 KB
testcase_70	AC	1,018 ms; 6,676 KB
testcase_71	AC	1,023 ms; 6,676 KB
testcase_72	AC	1,031 ms; 6,676 KB
testcase_73	AC	1,023 ms; 6,676 KB
testcase_74	AC	1,003 ms; 6,676 KB
testcase_75	AC	1,009 ms; 6,676 KB
testcase_76	AC	1,010 ms; 6,676 KB
testcase_77	AC	1,008 ms; 6,676 KB
testcase_78	AC	1,010 ms; 6,676 KB
testcase_79	AC	1,011 ms; 6,676 KB
testcase_80	AC	1,010 ms; 6,676 KB
testcase_81	AC	1,012 ms; 6,676 KB
testcase_82	AC	1,008 ms; 6,676 KB
testcase_83	AC	1,013 ms; 6,676 KB
testcase_84	AC	1,014 ms; 6,676 KB
testcase_85	AC	1,018 ms; 6,676 KB
testcase_86	AC	1,060 ms; 6,676 KB
testcase_87	AC	1,005 ms; 6,676 KB
testcase_88	AC	1,063 ms; 6,676 KB
testcase_89	AC	1,004 ms; 6,676 KB
testcase_90	AC	1,003 ms; 6,676 KB
testcase_91	AC	1,015 ms; 6,676 KB
testcase_92	AC	1,271 ms; 6,676 KB
testcase_93	AC	1,005 ms; 6,676 KB
testcase_94	AC	1,107 ms; 6,676 KB
testcase_95	AC	1,006 ms; 6,676 KB
testcase_96	AC	1,004 ms; 6,676 KB
testcase_97	AC	1,009 ms; 6,676 KB
testcase_98	AC	1,009 ms; 6,676 KB
testcase_99	AC	1,008 ms; 6,676 KB

ソースコード

#ifndef TOGASAT_HPP
#define TOGASAT_HPP
/************************************************************
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 <assert.h>
#include <math.h>
#include <stdio.h>
#include <algorithm>
#include <fstream>
#include <iostream>
#include <list>
#include <queue>
#include <set>
#include <sstream>
#include <string>
#include <vector>

#include <unordered_map>
#include <unordered_set>
// 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<Lit> data;  //(x1 v x2 v not x3)
    Clause() {}
    Clause(const std::vector<Lit> &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<Lit> &ps, bool learnt = false) {
    static CRef res = 0;
    ca[res] = std::move(Clause(ps, learnt));
    return res++;
  }

  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<Lit> &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<Lit> &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<CRef, Clause> ca;  // store clauses
  std::unordered_set<CRef> clauses;     // original problem;
  std::unordered_set<CRef> learnts;
  std::unordered_map<int, std::vector<Watcher>> watches;
  std::vector<VarData> vardata;  // store reason and level for each variable
  std::vector<bool> polarity;    // The preferred polarity of each variable
  std::vector<bool> decision;
  std::vector<bool> seen;
  // Todo
  int qhead;
  std::vector<Lit> trail;
  std::vector<int> trail_lim;
  // Todo rename(not heap)
  std::set<std::pair<double, Var>> order_heap;
  std::vector<double> activity;
  double var_inc;
  std::vector<Lit> model;
  std::vector<Lit> 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<double, Var> 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<std::pair<double, Var>> 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<Lit> &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<Watcher> &ws = watches[p.x];
      std::vector<Watcher>::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<Lit> 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<lbool> 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<Lit> 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(std::vector<int> &clause) {
    std::vector<Lit> 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

#ifndef ONLINE_JUDGE
//#define OPTUNA
#endif

#ifdef ONLINE_JUDGE
#define NDEBUG
#pragma GCC target("avx2")
#pragma GCC optimize("O3")
#pragma GCC optimize("unroll-loops")
#endif

#include<bits/stdc++.h>
using namespace std;
using ll=long long int;

struct Timer{
    chrono::high_resolution_clock::time_point st;
    float local;
    Timer(){
#ifndef ONLINE_JUDGE
        local=1.0;
#endif
        start();
    }
    void start(){
        st=chrono::high_resolution_clock::now();
    }
    int span()const{
        auto now=chrono::high_resolution_clock::now();
        return chrono::duration_cast<chrono::milliseconds>(now-st).count();
    }
};
Timer TIME;



void solve(){
    vector<vector<int>> cs;
    for(int i=0;i<2048;i++){
        int a,b,c,p,q,r;
        cin>>a>>b>>c>>p>>q>>r;
        a++;
        b++;
        c++;
        if(p==0) a*=-1;
        if(q==0) b*=-1;
        if(r==0) c*=-1;
        cs.push_back({a,b,c});
    }
    vector<int> ans;
    for(int i=1;i<2048;i++){
        cerr<<i<<endl;
        if(TIME.span()>1000) break;
        togasat::Solver solver;
        for(int j=0;j<i;j++){
            solver.addClause(cs[j]);
        }
        auto status=solver.solve();
        if(status==1){ //False
            break;
        }else{
            ans=solver.assigns;
        }
    }
    //cout<<ans<<endl;
    for(int i=255;i>=0;i--){
        cout<<1-ans[i];
    }
    cout<<endl;

#ifndef ONLINE_JUDGE
    cerr<<TIME.span()<<"ms"<<endl;
#endif
}
 
int main(const int argc,const char** argv){
    solve();
}