結果
| 問題 | No.5005 3-SAT |
| ユーザー |
 bin101
|
| 提出日時 | 2024-02-27 23:48:09 |
| 言語 | C++17 (gcc 12.3.0 + boost 1.83.0) |
| 結果 |
AC
|
| 実行時間 | 1,410 ms / 2,000 ms |
| コード長 | 30,948 bytes |
| コンパイル時間 | 5,622 ms |
| コンパイル使用メモリ | 266,972 KB |
| 実行使用メモリ | 6,676 KB |
| スコア | 772 |
| 最終ジャッジ日時 | 2024-02-27 23:50:05 |
| 合計ジャッジ時間 | 115,160 ms |
|
ジャッジサーバーID （参考情報） |
judge12 / judge15 |
| 純コード判定しない問題か言語 |
（要ログイン）
テストケース
テストケース表示| 入力 | 結果 | 実行時間 実行使用メモリ |
|---|---|---|
| testcase_00 | AC | 1,011 ms
6,676 KB |
| testcase_01 | AC | 1,011 ms
6,676 KB |
| testcase_02 | AC | 1,010 ms
6,676 KB |
| testcase_03 | AC | 1,009 ms
6,676 KB |
| testcase_04 | AC | 1,039 ms
6,676 KB |
| testcase_05 | AC | 1,005 ms
6,676 KB |
| testcase_06 | AC | 1,020 ms
6,676 KB |
| testcase_07 | AC | 1,008 ms
6,676 KB |
| testcase_08 | AC | 1,007 ms
6,676 KB |
| testcase_09 | AC | 1,005 ms
6,676 KB |
| testcase_10 | AC | 1,004 ms
6,676 KB |
| testcase_11 | AC | 1,165 ms
6,676 KB |
| testcase_12 | AC | 1,112 ms
6,676 KB |
| testcase_13 | AC | 1,011 ms
6,676 KB |
| testcase_14 | AC | 1,019 ms
6,676 KB |
| testcase_15 | AC | 1,064 ms
6,676 KB |
| testcase_16 | AC | 1,081 ms
6,676 KB |
| testcase_17 | AC | 1,008 ms
6,676 KB |
| testcase_18 | AC | 1,009 ms
6,676 KB |
| testcase_19 | AC | 1,004 ms
6,676 KB |
| testcase_20 | AC | 1,003 ms
6,676 KB |
| testcase_21 | AC | 1,015 ms
6,676 KB |
| testcase_22 | AC | 1,006 ms
6,676 KB |
| testcase_23 | AC | 1,037 ms
6,676 KB |
| testcase_24 | AC | 1,005 ms
6,676 KB |
| testcase_25 | AC | 1,003 ms
6,676 KB |
| testcase_26 | AC | 1,010 ms
6,676 KB |
| testcase_27 | AC | 1,018 ms
6,676 KB |
| testcase_28 | AC | 1,007 ms
6,676 KB |
| testcase_29 | AC | 1,007 ms
6,676 KB |
| testcase_30 | AC | 1,006 ms
6,676 KB |
| testcase_31 | AC | 1,077 ms
6,676 KB |
| testcase_32 | AC | 1,013 ms
6,676 KB |
| testcase_33 | AC | 1,009 ms
6,676 KB |
| testcase_34 | AC | 1,006 ms
6,676 KB |
| testcase_35 | AC | 1,008 ms
6,676 KB |
| testcase_36 | AC | 1,027 ms
6,676 KB |
| testcase_37 | AC | 1,008 ms
6,676 KB |
| testcase_38 | AC | 1,009 ms
6,676 KB |
| testcase_39 | AC | 1,016 ms
6,676 KB |
| testcase_40 | AC | 1,004 ms
6,676 KB |
| testcase_41 | AC | 1,007 ms
6,676 KB |
| testcase_42 | AC | 1,010 ms
6,676 KB |
| testcase_43 | AC | 1,410 ms
6,676 KB |
| testcase_44 | AC | 1,059 ms
6,676 KB |
| testcase_45 | AC | 1,025 ms
6,676 KB |
| testcase_46 | AC | 1,005 ms
6,676 KB |
| testcase_47 | AC | 1,011 ms
6,676 KB |
| testcase_48 | AC | 1,005 ms
6,676 KB |
| testcase_49 | AC | 1,013 ms
6,676 KB |
| testcase_50 | AC | 1,114 ms
6,676 KB |
| testcase_51 | AC | 1,008 ms
6,676 KB |
| testcase_52 | AC | 1,013 ms
6,676 KB |
| testcase_53 | AC | 1,004 ms
6,676 KB |
| testcase_54 | AC | 1,003 ms
6,676 KB |
| testcase_55 | AC | 1,190 ms
6,676 KB |
| testcase_56 | AC | 1,007 ms
6,676 KB |
| testcase_57 | AC | 1,007 ms
6,676 KB |
| testcase_58 | AC | 1,028 ms
6,676 KB |
| testcase_59 | AC | 1,030 ms
6,676 KB |
| testcase_60 | AC | 1,009 ms
6,676 KB |
| testcase_61 | AC | 1,053 ms
6,676 KB |
| testcase_62 | AC | 1,060 ms
6,676 KB |
| testcase_63 | AC | 1,005 ms
6,676 KB |
| testcase_64 | AC | 1,010 ms
6,676 KB |
| testcase_65 | AC | 1,073 ms
6,676 KB |
| testcase_66 | AC | 1,015 ms
6,676 KB |
| testcase_67 | AC | 1,010 ms
6,676 KB |
| testcase_68 | AC | 1,007 ms
6,676 KB |
| testcase_69 | AC | 1,056 ms
6,676 KB |
| testcase_70 | AC | 1,004 ms
6,676 KB |
| testcase_71 | AC | 1,005 ms
6,676 KB |
| testcase_72 | AC | 1,057 ms
6,676 KB |
| testcase_73 | AC | 1,009 ms
6,676 KB |
| testcase_74 | AC | 1,006 ms
6,676 KB |
| testcase_75 | AC | 1,010 ms
6,676 KB |
| testcase_76 | AC | 1,003 ms
6,676 KB |
| testcase_77 | AC | 1,010 ms
6,676 KB |
| testcase_78 | AC | 1,012 ms
6,676 KB |
| testcase_79 | AC | 1,045 ms
6,676 KB |
| testcase_80 | AC | 1,005 ms
6,676 KB |
| testcase_81 | AC | 1,003 ms
6,676 KB |
| testcase_82 | AC | 1,005 ms
6,676 KB |
| testcase_83 | AC | 1,006 ms
6,676 KB |
| testcase_84 | AC | 1,007 ms
6,676 KB |
| testcase_85 | AC | 1,019 ms
6,676 KB |
| testcase_86 | AC | 1,006 ms
6,676 KB |
| testcase_87 | AC | 1,007 ms
6,676 KB |
| testcase_88 | AC | 1,083 ms
6,676 KB |
| testcase_89 | AC | 1,017 ms
6,676 KB |
| testcase_90 | AC | 1,012 ms
6,676 KB |
| testcase_91 | AC | 1,005 ms
6,676 KB |
| testcase_92 | AC | 1,287 ms
6,676 KB |
| testcase_93 | AC | 1,008 ms
6,676 KB |
| testcase_94 | AC | 1,098 ms
6,676 KB |
| testcase_95 | AC | 1,015 ms
6,676 KB |
| testcase_96 | AC | 1,007 ms
6,676 KB |
| testcase_97 | AC | 1,011 ms
6,676 KB |
| testcase_98 | AC | 1,008 ms
6,676 KB |
| testcase_99 | AC | 1,021 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;
//using Int=__int128;
#define mask(x) ((1LL<<x)-1)
#define ALL(A) A.begin(),A.end()
template<typename T1,typename T2> bool chmin(T1 &a,T2 b){if(a<=b)return 0; a=b; return 1;}
template<typename T1,typename T2> bool chmax(T1 &a,T2 b){if(a>=b)return 0; a=b; return 1;}
template<typename T> int bitUP(T x,int a){return (x>>a)&1;}
enum Dir{
Right,
Down,
Left,
Up
};
//→ ↓ ← ↑
int dh[4]={0,1,0,-1}, dw[4]={1,0,-1,0};
//上から時計回り
//int dx[8]={0,1,1,1,0,-1,-1,-1}, dy[8]={1,1,0,-1,-1,-1,0,1};
long double EPS = 1e-6;
const ll INF=(1LL<<62);
const int MAX=(1<<30);
using pii=pair<int,int>;
using pil=pair<int,ll>;
using pli=pair<ll,int>;
using pll=pair<ll,ll>;
using psi=pair<string,int>;
using pis=pair<int,string>;
using psl=pair<string,ll>;
using pls=pair<ll,string>;
using pss=pair<string,string>;
template<class T>
using minimum_queue=priority_queue<T,vector<T>,greater<T>>;
using Graph=vector<vector<int>>;
using i8=int8_t;
using i16=int16_t;
using i32=int32_t;
using i64=int64_t;
using u8=uint8_t;
using u16=uint16_t;
using u32=uint32_t;
using u64=uint64_t;
void FastIO(){
ios::sync_with_stdio(false);
cin.tie(0);
cout << fixed << setprecision(20);
}
//0-indexed vector cin
template<typename T>
inline istream &operator>>(istream &is,vector<T> &v) {
for(size_t i=0;i<v.size();i++) is>>v[i];
return is;
}
//0-indexed vector cin
template<typename T>
inline istream &operator>>(istream &is,vector<vector<T>> &v) {
for(size_t i=0;i<v.size();i++){
is>>v[i];
}
return is;
}
struct Xor32{
using u32=uint32_t;
u32 x=1234567;
inline u32 rnd_make(){
x^=(x<<13);
x^=(x>>17);
x^=(x<<5);
return x;
}
inline u32 operator()(){
return rnd_make();
}
//[a,b)
inline int operator()(int a,int b){
int dis=b-a;
int add=rnd_make()%dis;
return a+add;
}
//[0,b)
inline int operator()(int b){
return rnd_make()%b;
}
//http://web.archive.org/web/20200105011004/https://topcoder.g.hatena.ne.jp/tomerun/20171216/
//[0,b)の中から異なる2つを選ぶ [0]の値<[1]の値
inline array<int,2> two(int b){
assert(b>=2);
int v1=rnd_make()%b;
int v2=rnd_make()%(b-1);
if (v2>=v1) return {v1,v2+1};
else return {v2,v1};
}
inline float random01(){
return float(rnd_make())/mask(32);
}
inline double random_double(double a,double b){
double sa=b-a;
a+=random01()*sa;
return a;
}
//確率pでtrueを返す
inline bool gen_bool(float p){
return p>random01();
}
};
struct Xor64{
u64 x=1234567;
inline u64 rnd_make(){
x ^= x << 13;
x ^= x >> 7;
x ^= x << 17;
return x;
}
inline u64 operator()(){
return rnd_make();
}
};
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();
}
};
struct TestTimer{
chrono::high_resolution_clock::time_point st;
unordered_map<string,ll> sum_time;
unordered_map<string,chrono::high_resolution_clock::time_point> start_time;
TestTimer(){}
void start(const string &s){
#ifndef ONLINE_JUDGE
start_time[s]=chrono::high_resolution_clock::now();
#endif
}
void end(const string &s){
#ifndef ONLINE_JUDGE
auto now=chrono::high_resolution_clock::now();
sum_time[s]+=chrono::duration_cast<chrono::nanoseconds>(now-start_time[s]).count();
#endif
}
void output()const{
#ifndef ONLINE_JUDGE
for(auto m:sum_time){
cerr<<m.first<<": "<<m.second/1e6<<"ms"<<endl;
}
#endif
}
};
struct TestCounter{
unordered_map<string,ll> cnt;
TestCounter(){}
void count(const string &s){
#ifndef ONLINE_JUDGE
cnt[s]++;
#endif
}
void output()const{
#ifndef ONLINE_JUDGE
for(auto m:cnt){
cerr<<m.first<<": "<<m.second<<endl;
}
#endif
}
};
Timer TIME;
Xor32 Rand32;
Xor64 Rand64;
TestTimer testTimer;
TestCounter testCounter;
//https://atcoder.jp/contests/asprocon9/submissions/34659956
template<class T,int CAPACITY>
class DynamicArray{
public:
array<T,CAPACITY> array_={};
int size_=0;
DynamicArray(){}
DynamicArray(int n){
resize(n);
}
void push_back(const T &e){
array_[size_++]=e;
}
//ソートされた状態を保つように挿入
void insert(const T &e){
int ng=-1,ok=size_;
while(ok-ng!=1){
int mid=(ok+ng)/2;
if(array_[mid]>e) ok=mid;
else ng=mid;
}
for(int i=size_;i>ok;i--){
array_[i]=array_[i-1];
}
array_[ok]=e;
size_++;
}
//eをこえる一番左の添字
int find_binary_search(const T &e)const{
int ng=-1,ok=size_;
while(ok-ng!=1){
int mid=(ok+ng)/2;
if(array_[mid]>=e) ok=mid;
else ng=mid;
}
return ok;
}
void pop_back(){
size_--;
}
inline T& operator[](int index){
return array_[index];
}
inline const T& operator[](int index) const {
return array_[index];
}
inline int size()const{
return size_;
}
inline T& back(){
return array_[size_-1];
}
const inline T& back()const{
return array_[size_-1];
}
inline auto begin() -> decltype(array_.begin()) {
return array_.begin();
}
inline auto end() -> decltype(array_.begin()) {
return array_.begin() + size_;
}
inline auto begin() const -> decltype(array_.begin()) {
return array_.begin();
}
inline auto end() const -> decltype(array_.begin()) {
return array_.begin() + size_;
}
inline void resize(int new_size){
size_=new_size;
}
void operator=(const DynamicArray &e){
for(int i=0;i<e.size_;i++){
array_[i]=e[i];
}
size_=e.size_;
}
bool operator==(const DynamicArray &v){
if(size_!=v.size_) return false;
for(int i=0;i<size_;i++){
if(array_[i]!=v[i]){
return false;
}
}
return true;
}
bool operator==(const vector<T> &v){
if(size_!=v.size()) return false;
for(int i=0;i<size_;i++){
if(array_[i]!=v[i]){
return false;
}
}
return true;
}
void clear(){
size_=0;
}
//O(1)
//末尾と入れ替える。順序が保持されないが高速
void swap_remove(int idx){
array_[idx]=array_[size_-1];
size_--;
}
//最初から見ていき、一致したものを削除(remove)
bool erase(T value){
for(int i=0;i<size_;i++){
if(array_[i]==value){
remove(i);
return true;
}
}
return false;
}
void reverse(){
for(int i=0;i<size_/2;i++){
swap(array_[i],array_[size_-1-i]);
}
}
//O(size)
//順序を気にしない場合、swap_removeの方がいい
void remove(int idx){
for(int i=idx;i<size_-1;i++){
array_[i]=array_[i+1];
}
size_--;
}
void fill(T x){
for(int i=0;i<size_;i++){
array_[i]=x;
}
}
};
//ソート
template<typename T>
inline void vsort(vector<T> &v){
sort(v.begin(),v.end());
}
//逆順ソート
template<typename T>
inline void rvsort(vector<T> &v){
sort(v.rbegin(),v.rend());
}
//1ビットの数を返す
inline int popcount(int x){
return __builtin_popcount(x);
}
//1ビットの数を返す
inline int popcount(ll x){
return __builtin_popcountll(x);
}
template<typename T>
inline void Compress(vector<T> &C){
sort(C.begin(),C.end());
C.erase(unique(C.begin(),C.end()),C.end());
}
//要素数n 初期値x
template<typename T>
inline vector<T> vmake(size_t n,T x){
return vector<T>(n,x);
}
//a,b,c,x data[a][b][c] 初期値x
template<typename... Args>
auto vmake(size_t n,Args... args){
auto v=vmake(args...);
return vector<decltype(v)>(n,move(v));
}
//vは昇順
bool is_in(const vector<int> &v,int x){
int n=v.size();
if(n==0) return false;
int ng=-1,ok=n-1;
while(ok-ng!=1){
int mid=(ok+ng)/2;
if(v[mid]<x) ng=mid;
else ok=mid;
}
if(v[ok]==x) return true;
return false;
}
template<typename T >
struct edge {
int to;
T cost;
int id;
edge()=default;
edge(int to, T cost,int id) : to(to), cost(cost), id(id) {}
};
template<class T >
struct Edge {
int from, to,id;
T cost;
Edge(int from,int to,T cost,int id):from(from),to(to),cost(cost),id(id){}
Edge()=default;
bool operator<(const Edge<T> &e){
return cost<e.cost;
}
bool operator<=(const Edge<T> &e){
return cost<=e.cost;
}
};
template<typename T>
using WeightGraph=vector<vector<edge<T>>>;
//vector cout
template<typename T>
inline ostream &operator<<(ostream &os,const vector<T> &v) {
bool sp=true;
if(string(typeid(T).name())=="c") sp=false;
for(size_t i=0;i<v.size();i++){
if(i and sp) os<<" ";
os<<v[i];
}
return os;
}
//vector<vector> cout
template<typename T>
inline ostream &operator<<(ostream &os,const vector<vector<T>> &v) {
for(size_t i=0;i<v.size();i++){
os<<v[i];
if(i+1!=v.size()) os<<"\n";
}
return os;
}
//pair cout
template<typename T, typename U>
inline ostream &operator<<(ostream &os,const pair<T,U> &p) {
os<<p.first<<" "<<p.second;
return os;
}
//map cout
template<typename F, typename S>
inline ostream &operator<<(ostream &os,const map<F,S> &M) {
bool first=false;
for(auto x:M){
if(first) os<<endl;
first=true;
os<<x;
}
return os;
}
//set cout
template<typename T>
inline ostream &operator<<(ostream &os,const set<T> &S) {
bool first=false;
for(auto x:S){
if(first) os<<endl;
first=true;
os<<x;
}
return os;
}
//pair cin
template<typename T, typename U>
inline istream &operator>>(istream &is,pair<T,U> &p) {
is>>p.first>>p.second;
return is;
}
template<typename T>
void append(vector<T> &v,const vector<T> &vp){
for(auto p:vp){
v.push_back(p);
}
}
//Fisher–Yatesアルゴリズム
template<typename T>
void shuffle(vector<T> &v){
int sz=v.size();
for(int i=sz-1;i>0;i--){
swap(v[Rand32()%(i+1)],v[i]);
}
}
template<class T,class U>
T linear_function(U x,U start_x,U end_x,T start_value,T end_value){
if(x>=end_x) return end_value;
if(x<=start_x) return start_value;
return start_value+(end_value-start_value)*(x-start_x)/(end_x-start_x);
}
//http://gasin.hatenadiary.jp/entry/2019/09/03/162613
struct SimulatedAnnealing{
long double temp_start; //差の最大値(あくまでも参考)
long double temp_end; //差の最小値(あくまでも参考)
float time_start;
float time_end;
bool is_hill;
bool minimum;
int interval; //intervalごとに温度の再計算
long double temp_now;
int cnt_calc_temp;
/*
0:線形
1:pow pow
2:指数
*/
int temp_type;
//SimulatedAnnealing(){}
SimulatedAnnealing(long double temp_start,long double temp_end,float time_start,float time_end,bool is_hill,bool minimum,int temp_type=0,int interval=1):
temp_start(temp_start),temp_end(temp_end),time_start(time_start),time_end(time_end),
is_hill(is_hill),minimum(minimum),temp_type(temp_type),interval(interval),temp_now(temp_start),cnt_calc_temp(0){
}
float calc_temp(){
if(cnt_calc_temp%interval==0){
float progress=float(TIME.span()-time_start)/(time_end-time_start);
if(progress>1.0) progress=1.0;
if(temp_type==0){//線形
temp_now=temp_start*(1.0-progress)+temp_end*progress;
//cerr<<progress<<endl;
//cerr<<temp_now<<endl;
}else if(temp_type==1){ //https://atcoder.jp/contests/ahc014/submissions/35326979
temp_now = pow(temp_start,1.0-progress)*pow(temp_end,progress);
}else{ //https://ozy4dm.hateblo.jp/entry/2022/12/22/162046#68-%E3%83%97%E3%83%AB%E3%83%BC%E3%83%8B%E3%83%B3%E3%82%B0%E6%97%A9%E6%9C%9F%E7%B5%82%E4%BA%86%E5%8D%98%E7%B4%94%E5%8C%96%E3%81%95%E3%82%8C%E3%81%9F%E8%A8%88%E7%AE%97%E3%82%92%E4%BD%BF%E7%94%A8%E3%81%99%E3%82%8B
temp_now = temp_start*pow(temp_end/temp_start,progress);
}
}
cnt_calc_temp++;
return temp_now;
}
//diff: スコアの変化量
//確率を計算
float calc_prob(float diff){
if(minimum) diff*=-1;
if(diff>0) return 1;
long double temp=calc_temp();
return exp(diff/temp);
}
inline bool operator()(long double diff){
testCounter.count("try_cnt");
if(minimum) diff*=-1;
if(diff>=0){
if(diff==0) testCounter.count("zero_change");
else testCounter.count("plus_change");
return true;
}
if(is_hill) return false;
//cerr<<calc_temp()<<endl;
long double prob = exp(diff/calc_temp());
if(Rand32.gen_bool(prob)){
testCounter.count("minus_change");
return true;
}
else return false;
}
//最大化の場合,返り値<変化量なら遷移してもよい
long double calc_tolerance(long double prob){
long double tolerance=log(prob)*calc_temp();
if(minimum) tolerance*=-1;
return tolerance;
}
//log(prob)*temp prob:[0,1]の乱数
long double calc_tolerance(){
long double prob=Rand32.random01();
return calc_tolerance(prob);
}
};
///++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
///++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
///++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//https://atcoder.jp/contests/asprocon9/submissions/34659956
#ifndef OPTUNA
#define REGIST_PARAM(name, type, defaultValue) constexpr type name = defaultValue
#else
#define REGIST_PARAM(name, type, defaultValue) type name = defaultValue
#endif
namespace OP{
REGIST_PARAM(yama,bool,false);
REGIST_PARAM(startTemp,double,500000);
REGIST_PARAM(endTemp,float,0);
REGIST_PARAM(TIME_END,int,1900);
};
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<<ans[i];
}
cout<<endl;
#ifndef ONLINE_JUDGE
testTimer.output();
testCounter.output();
cerr<<TIME.span()<<"ms"<<endl;
//cerr<<"score: "<<simulate(best_grid,true)<<endl;
#endif
}
int main(const int argc,const char** argv){
#ifndef OPTUNA
if(argc!=1){
}
#endif
FastIO();
int T=1;
//cin>>T;
while(T--) solve();
}