結果
| 問題 | No.5005 3-SAT |
| ユーザー |
|
| 提出日時 | 2022-04-29 19:19:44 |
| 言語 | C++17 (gcc 12.3.0 + boost 1.83.0) |
| 結果 |
AC
|
| 実行時間 | 208 ms / 2,000 ms |
| コード長 | 23,181 bytes |
| コンパイル時間 | 3,756 ms |
| 実行使用メモリ | 5,244 KB |
| スコア | 95,669 |
| 最終ジャッジ日時 | 2022-04-29 19:19:55 |
| 合計ジャッジ時間 | 10,339 ms |
|
ジャッジサーバーID （参考情報） |
judge13 / judge12 |
| 純コード判定しない問題か言語 |
（要ログイン）
テストケース
テストケース表示| 入力 | 結果 | 実行時間 実行使用メモリ |
|---|---|---|
| testcase_00 | AC | 15 ms
3,884 KB |
| testcase_01 | AC | 3 ms
3,804 KB |
| testcase_02 | AC | 3 ms
3,820 KB |
| testcase_03 | AC | 6 ms
3,832 KB |
| testcase_04 | AC | 3 ms
3,840 KB |
| testcase_05 | AC | 6 ms
3,960 KB |
| testcase_06 | AC | 11 ms
3,872 KB |
| testcase_07 | AC | 15 ms
4,100 KB |
| testcase_08 | AC | 65 ms
4,280 KB |
| testcase_09 | AC | 5 ms
3,780 KB |
| testcase_10 | AC | 12 ms
3,988 KB |
| testcase_11 | AC | 3 ms
3,744 KB |
| testcase_12 | AC | 3 ms
3,748 KB |
| testcase_13 | AC | 20 ms
4,092 KB |
| testcase_14 | AC | 5 ms
3,800 KB |
| testcase_15 | AC | 3 ms
3,916 KB |
| testcase_16 | AC | 12 ms
3,896 KB |
| testcase_17 | AC | 5 ms
3,804 KB |
| testcase_18 | AC | 5 ms
3,932 KB |
| testcase_19 | AC | 15 ms
3,964 KB |
| testcase_20 | AC | 32 ms
4,040 KB |
| testcase_21 | AC | 111 ms
4,724 KB |
| testcase_22 | AC | 5 ms
3,864 KB |
| testcase_23 | AC | 5 ms
3,788 KB |
| testcase_24 | AC | 22 ms
3,944 KB |
| testcase_25 | AC | 159 ms
5,132 KB |
| testcase_26 | AC | 4 ms
3,784 KB |
| testcase_27 | AC | 14 ms
3,940 KB |
| testcase_28 | AC | 20 ms
3,932 KB |
| testcase_29 | AC | 10 ms
3,912 KB |
| testcase_30 | AC | 5 ms
3,792 KB |
| testcase_31 | AC | 6 ms
3,956 KB |
| testcase_32 | AC | 38 ms
4,196 KB |
| testcase_33 | AC | 7 ms
3,820 KB |
| testcase_34 | AC | 7 ms
3,868 KB |
| testcase_35 | AC | 16 ms
3,948 KB |
| testcase_36 | AC | 3 ms
3,932 KB |
| testcase_37 | AC | 58 ms
4,372 KB |
| testcase_38 | AC | 172 ms
5,076 KB |
| testcase_39 | AC | 2 ms
3,832 KB |
| testcase_40 | AC | 4 ms
3,936 KB |
| testcase_41 | AC | 169 ms
5,052 KB |
| testcase_42 | AC | 4 ms
3,792 KB |
| testcase_43 | AC | 2 ms
3,780 KB |
| testcase_44 | AC | 39 ms
4,040 KB |
| testcase_45 | AC | 3 ms
3,836 KB |
| testcase_46 | AC | 38 ms
4,100 KB |
| testcase_47 | AC | 10 ms
3,840 KB |
| testcase_48 | AC | 26 ms
4,052 KB |
| testcase_49 | AC | 32 ms
4,028 KB |
| testcase_50 | AC | 8 ms
3,956 KB |
| testcase_51 | AC | 39 ms
4,140 KB |
| testcase_52 | AC | 22 ms
4,052 KB |
| testcase_53 | AC | 4 ms
3,924 KB |
| testcase_54 | AC | 24 ms
4,024 KB |
| testcase_55 | AC | 2 ms
3,832 KB |
| testcase_56 | AC | 8 ms
3,964 KB |
| testcase_57 | AC | 26 ms
4,044 KB |
| testcase_58 | AC | 5 ms
3,840 KB |
| testcase_59 | AC | 16 ms
4,052 KB |
| testcase_60 | AC | 3 ms
3,772 KB |
| testcase_61 | AC | 7 ms
3,860 KB |
| testcase_62 | AC | 5 ms
3,864 KB |
| testcase_63 | AC | 18 ms
3,964 KB |
| testcase_64 | AC | 135 ms
4,984 KB |
| testcase_65 | AC | 208 ms
5,244 KB |
| testcase_66 | AC | 17 ms
3,968 KB |
| testcase_67 | AC | 8 ms
3,984 KB |
| testcase_68 | AC | 67 ms
4,336 KB |
| testcase_69 | AC | 13 ms
3,972 KB |
| testcase_70 | AC | 4 ms
3,840 KB |
| testcase_71 | AC | 29 ms
4,152 KB |
| testcase_72 | AC | 12 ms
3,988 KB |
| testcase_73 | AC | 5 ms
3,852 KB |
| testcase_74 | AC | 51 ms
4,224 KB |
| testcase_75 | AC | 5 ms
3,972 KB |
| testcase_76 | AC | 20 ms
3,988 KB |
| testcase_77 | AC | 6 ms
3,940 KB |
| testcase_78 | AC | 10 ms
3,896 KB |
| testcase_79 | AC | 10 ms
3,852 KB |
| testcase_80 | AC | 19 ms
3,984 KB |
| testcase_81 | AC | 5 ms
3,856 KB |
| testcase_82 | AC | 3 ms
3,768 KB |
| testcase_83 | AC | 6 ms
4,004 KB |
| testcase_84 | AC | 14 ms
3,932 KB |
| testcase_85 | AC | 35 ms
4,092 KB |
| testcase_86 | AC | 4 ms
3,796 KB |
| testcase_87 | AC | 21 ms
3,940 KB |
| testcase_88 | AC | 6 ms
3,880 KB |
| testcase_89 | AC | 21 ms
4,032 KB |
| testcase_90 | AC | 18 ms
3,988 KB |
| testcase_91 | AC | 13 ms
3,928 KB |
| testcase_92 | AC | 3 ms
3,936 KB |
| testcase_93 | AC | 5 ms
3,796 KB |
| testcase_94 | AC | 4 ms
3,832 KB |
| testcase_95 | AC | 7 ms
3,868 KB |
| testcase_96 | AC | 110 ms
4,880 KB |
| testcase_97 | AC | 64 ms
4,416 KB |
| testcase_98 | AC | 21 ms
4,064 KB |
| testcase_99 | AC | 11 ms
3,900 KB |
ソースコード
#pragma GCC optimize("O3")
#include <bits/stdc++.h>
// 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<typename remove_reference<decltype(l)>::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<typename T1, typename T2> inline ostream& operator <<(ostream &o, const pair<T1, T2> p) { o << '(' << p.first << ':' << p.second << ')'; return o; }
template<typename T> inline T& chmax(T& to, const T& val) { return to = max(to, val); }
template<typename T> 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<typename T, typename Random = decltype(randdev), typename enable_if<is_integral<T>::value>::type* = nullptr>
inline T rand(T l, T h, Random& rand = randdev) { return uniform_int_distribution<T>(l, h)(rand); }
template<typename T, typename Random = decltype(randdev), typename enable_if<is_floating_point<T>::value>::type* = nullptr>
inline T rand(T l, T h, Random& rand = randdev) { return uniform_real_distribution<T>(l, h)(rand); }template<typename T>
static ostream& operator<<(ostream& o, const std::vector<T>& v) {
o << "[ "; for(const auto& e : v) o<<e<<' '; return o << ']';
}
template <typename I> struct MyRangeFormat{ I b,e; MyRangeFormat(I _b, I _e):b(_b),e(_e){} };
template<typename I> static ostream& operator<<(ostream& o, const MyRangeFormat<I>& f) {
o << "[ "; iterate(i,f.b,f.e) o<<*i<<' '; return o << ']';
}
template <typename I> 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<typename I> static ostream& operator<<(ostream& o, const MyMatrixFormat<I>& f) {
o<<'\n'; repeat(i,(f.n)) { repeat(j,f.m) o<<f.p[i][j]<<' '; o<<'\n'; }
return o;
}
struct LOG_t { ~LOG_t() { cout << endl; } };
#define LOG (LOG_t(),cout<<'L'<<__LINE__<<": ")
#define FMTA(m,w) (MyRangeFormat<decltype(m+0)>(m,m+w))
#define FMTR(b,e) (MyRangeFormat<decltype(e)>(b,e))
#define FMTV(v) FMTR(v.begin(),v.end())
#define FMTM(m,h,w) (MyMatrixFormat<decltype(m+0)>(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<typename T> 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<typename T, typename enable_if<is_integral<T>::value, nullptr_t>::type = nullptr>
inline MaiScanner& operator>>(T& var) noexcept { input_integer<T>(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<typename IT> 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<typename T>
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<typename T, typename enable_if<is_integral<T>::value, nullptr_t>::type = nullptr>
inline MaiPrinter& operator<<(T var) noexcept { output_integer<T>(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<typename IT> 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 <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++;
}
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<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(const 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
//
//
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<pair<int, int>, 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 = "";
int T = 950;
// upto(T, 800, 1200, 200) {
while(100 <= T)
{
togasat::Solver solver;
repeat(i, 256) solver.newVar();
repeat(i, T) {
vector<int> 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]);
}
}
if (best >= T) break;
T -= 50;
}
reverse(all(g_best_str));
clog << g_best<<endl;
cout << g_best_str << endl;
return 0;
}