結果

問題 No.5005 3-SAT
ユーザー bin101bin101
提出日時 2024-02-28 00:26:38
言語 C++17
(gcc 12.3.0 + boost 1.83.0)
結果
AC  
実行時間 1,987 ms / 2,000 ms
コード長 16,527 bytes
コンパイル時間 3,979 ms
コンパイル使用メモリ 252,516 KB
実行使用メモリ 8,960 KB
スコア 101,387
最終ジャッジ日時 2024-02-28 00:30:08
合計ジャッジ時間 208,581 ms
ジャッジサーバーID
(参考情報)
judge13 / judge15
純コード判定しない問題か言語
このコードへのチャレンジ
(要ログイン)

テストケース

テストケース表示
入力 結果 実行時間
実行使用メモリ
testcase_00 AC 1,985 ms
7,040 KB
testcase_01 AC 1,984 ms
7,552 KB
testcase_02 AC 1,985 ms
7,680 KB
testcase_03 AC 1,986 ms
8,320 KB
testcase_04 AC 1,985 ms
7,516 KB
testcase_05 AC 1,986 ms
8,800 KB
testcase_06 AC 1,986 ms
8,448 KB
testcase_07 AC 1,986 ms
8,576 KB
testcase_08 AC 1,985 ms
8,704 KB
testcase_09 AC 1,987 ms
8,832 KB
testcase_10 AC 1,985 ms
7,808 KB
testcase_11 AC 1,987 ms
8,576 KB
testcase_12 AC 1,987 ms
8,704 KB
testcase_13 AC 1,985 ms
7,296 KB
testcase_14 AC 1,984 ms
7,424 KB
testcase_15 AC 1,985 ms
7,784 KB
testcase_16 AC 1,986 ms
8,544 KB
testcase_17 AC 1,984 ms
7,808 KB
testcase_18 AC 1,985 ms
7,548 KB
testcase_19 AC 1,986 ms
8,448 KB
testcase_20 AC 1,985 ms
8,192 KB
testcase_21 AC 1,985 ms
7,808 KB
testcase_22 AC 1,985 ms
7,680 KB
testcase_23 AC 1,986 ms
8,704 KB
testcase_24 AC 1,986 ms
8,704 KB
testcase_25 AC 1,986 ms
8,704 KB
testcase_26 AC 1,986 ms
7,808 KB
testcase_27 AC 1,987 ms
8,448 KB
testcase_28 AC 1,984 ms
7,040 KB
testcase_29 AC 1,986 ms
8,704 KB
testcase_30 AC 1,986 ms
7,424 KB
testcase_31 AC 1,987 ms
8,700 KB
testcase_32 AC 1,985 ms
7,296 KB
testcase_33 AC 1,986 ms
8,832 KB
testcase_34 AC 1,986 ms
8,448 KB
testcase_35 AC 1,986 ms
8,576 KB
testcase_36 AC 1,985 ms
7,808 KB
testcase_37 AC 1,986 ms
7,936 KB
testcase_38 AC 1,987 ms
8,448 KB
testcase_39 AC 1,987 ms
8,576 KB
testcase_40 AC 1,984 ms
7,680 KB
testcase_41 AC 1,985 ms
8,448 KB
testcase_42 AC 1,986 ms
7,808 KB
testcase_43 AC 1,986 ms
8,576 KB
testcase_44 AC 1,986 ms
8,320 KB
testcase_45 AC 1,986 ms
8,576 KB
testcase_46 AC 1,986 ms
8,540 KB
testcase_47 AC 1,986 ms
8,320 KB
testcase_48 AC 1,986 ms
8,672 KB
testcase_49 AC 1,985 ms
7,552 KB
testcase_50 AC 1,987 ms
8,704 KB
testcase_51 AC 1,986 ms
8,704 KB
testcase_52 AC 1,987 ms
8,832 KB
testcase_53 AC 1,986 ms
8,192 KB
testcase_54 AC 1,985 ms
7,776 KB
testcase_55 AC 1,986 ms
8,704 KB
testcase_56 AC 1,985 ms
7,808 KB
testcase_57 AC 1,986 ms
8,064 KB
testcase_58 AC 1,986 ms
6,912 KB
testcase_59 AC 1,985 ms
6,676 KB
testcase_60 AC 1,986 ms
8,548 KB
testcase_61 AC 1,986 ms
8,704 KB
testcase_62 AC 1,986 ms
7,936 KB
testcase_63 AC 1,986 ms
8,064 KB
testcase_64 AC 1,986 ms
8,832 KB
testcase_65 AC 1,986 ms
8,576 KB
testcase_66 AC 1,986 ms
8,560 KB
testcase_67 AC 1,986 ms
8,960 KB
testcase_68 AC 1,886 ms
8,576 KB
testcase_69 AC 1,985 ms
7,552 KB
testcase_70 AC 1,985 ms
7,040 KB
testcase_71 AC 1,986 ms
8,576 KB
testcase_72 AC 1,987 ms
8,704 KB
testcase_73 AC 1,985 ms
7,808 KB
testcase_74 AC 1,985 ms
8,832 KB
testcase_75 AC 1,986 ms
8,320 KB
testcase_76 AC 1,987 ms
8,832 KB
testcase_77 AC 1,986 ms
8,576 KB
testcase_78 AC 1,987 ms
8,704 KB
testcase_79 AC 1,986 ms
8,704 KB
testcase_80 AC 1,987 ms
8,576 KB
testcase_81 AC 1,985 ms
8,448 KB
testcase_82 AC 1,986 ms
8,448 KB
testcase_83 AC 1,986 ms
8,576 KB
testcase_84 AC 1,987 ms
8,684 KB
testcase_85 AC 1,987 ms
8,448 KB
testcase_86 AC 1,985 ms
7,296 KB
testcase_87 AC 1,986 ms
8,448 KB
testcase_88 AC 1,987 ms
8,448 KB
testcase_89 AC 1,986 ms
8,576 KB
testcase_90 AC 1,986 ms
8,448 KB
testcase_91 AC 1,987 ms
8,448 KB
testcase_92 AC 1,986 ms
8,320 KB
testcase_93 AC 1,986 ms
8,832 KB
testcase_94 AC 1,985 ms
8,692 KB
testcase_95 AC 1,987 ms
8,804 KB
testcase_96 AC 1,987 ms
8,704 KB
testcase_97 AC 1,986 ms
8,556 KB
testcase_98 AC 1,986 ms
8,576 KB
testcase_99 AC 1,986 ms
8,320 KB
権限があれば一括ダウンロードができます

ソースコード

diff #

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

struct Timer{
    chrono::high_resolution_clock::time_point st;
    chrono::high_resolution_clock::time_point now;
    int cnt=0;
    float local;

    Timer(){
#ifndef ONLINE_JUDGE
        local=1.0;
#endif
        start();
    }
    void start(){
        st=chrono::high_resolution_clock::now();
    }
    int span(){
        cnt++;
        if((cnt&1023)==0 or true){
            now=chrono::high_resolution_clock::now();
        }
        return chrono::duration_cast<chrono::milliseconds>(now-st).count();
    }
};
Timer TIME;

#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) {
      if(TIME.span()>1980){
          return l_False;
      }
      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

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(256);
    int ok=800,ng=1150;
    while(ng-ok!=1 and TIME.span()<1800){
        int mid=(ok+ng)/2;
        togasat::Solver solver;
        for(int j=0;j<mid;j++){
            solver.addClause(cs[j]);
        }
        auto status=solver.solve();
        if(status==1){
            ng=mid;
        }else{
            //cerr<<mid<<endl;
            ok=mid;
            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();
}
0