修改项目结构
This commit is contained in:
parent
6c89cb4334
commit
8992b41a8b
18
README.md
18
README.md
@ -1,18 +0,0 @@
|
||||
### Compile
|
||||
```
|
||||
make clean; make
|
||||
```
|
||||
|
||||
|
||||
### Run
|
||||
|
||||
$instance: input cnf
|
||||
|
||||
```
|
||||
./Light $instance
|
||||
```
|
||||
|
||||
For more options, try './light -h'
|
||||
|
||||
|
||||
|
||||
72
bug.txt
72
bug.txt
@ -1,72 +0,0 @@
|
||||
|
||||
这个200s 退出了
|
||||
03bb7baaa45980753a0e7050ae44755d-atco_enc3_opt1_03_53.cnf
|
||||
|
||||
preprocess 占了特别大内存
|
||||
04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf
|
||||
|
||||
==2320428==
|
||||
==2320428== Process terminating with default action of signal 15 (SIGTERM)
|
||||
==2320428== at 0x4DF912F: poll (poll.c:29)
|
||||
==2320428== by 0x50E09B8: ??? (in /usr/lib/x86_64-linux-gnu/libevent_core-2.1.so.7.0.1)
|
||||
==2320428== by 0x50DBCEC: event_base_loop (in /usr/lib/x86_64-linux-gnu/libevent_core-2.1.so.7.0.1)
|
||||
==2320428== by 0x4F1AAC5: ??? (in /usr/lib/x86_64-linux-gnu/libopen-pal.so.40.30.2)
|
||||
==2320428== by 0x4D78401: start_thread (pthread_create.c:442)
|
||||
==2320428== by 0x4E06743: clone (clone.S:100)
|
||||
==2320428==
|
||||
==2320428== HEAP SUMMARY:
|
||||
==2320428== in use at exit: 5,263,216,314 bytes in 121,653 blocks
|
||||
==2320428== total heap usage: 230,366 allocs, 108,713 frees, 5,284,993,033 bytes allocated
|
||||
==2320428==
|
||||
==2320426==
|
||||
==2320426== Process terminating with default action of signal 15 (SIGTERM)
|
||||
==2320426== at 0x4DF912F: poll (poll.c:29)
|
||||
==2320426== by 0x50E09B8: ??? (in /usr/lib/x86_64-linux-gnu/libevent_core-2.1.so.7.0.1)
|
||||
==2320426== by 0x50DBCEC: event_base_loop (in /usr/lib/x86_64-linux-gnu/libevent_core-2.1.so.7.0.1)
|
||||
==2320426== by 0x4F1AAC5: ??? (in /usr/lib/x86_64-linux-gnu/libopen-pal.so.40.30.2)
|
||||
==2320426== by 0x4D78401: start_thread (pthread_create.c:442)
|
||||
==2320426== by 0x4E06743: clone (clone.S:100)
|
||||
==2320426==
|
||||
==2320426== HEAP SUMMARY:
|
||||
==2320426== in use at exit: 164,740,285 bytes in 19,687 blocks
|
||||
==2320426== total heap usage: 61,284 allocs, 41,597 frees, 167,994,848 bytes allocated
|
||||
==2320426==
|
||||
==2320426== LEAK SUMMARY:
|
||||
==2320426== definitely lost: 5,056 bytes in 12 blocks
|
||||
==2320426== indirectly lost: 0 bytes in 0 blocks
|
||||
==2320426== possibly lost: 160,111,368 bytes in 4,232 blocks
|
||||
==2320426== still reachable: 4,623,861 bytes in 15,443 blocks
|
||||
==2320426== of which reachable via heuristic:
|
||||
==2320426== newarray : 1,040 bytes in 2 blocks
|
||||
==2320426== suppressed: 0 bytes in 0 blocks
|
||||
==2320426== Rerun with --leak-check=full to see details of leaked memory
|
||||
==2320426==
|
||||
==2320426== Use --track-origins=yes to see where uninitialised values come from
|
||||
==2320426== For lists of detected and suppressed errors, rerun with: -s
|
||||
==2320426== ERROR SUMMARY: 4 errors from 4 contexts (suppressed: 0 from 0)
|
||||
==2320427==
|
||||
==2320427== Process terminating with default action of signal 15 (SIGTERM)
|
||||
==2320427== at 0x4DF912F: poll (poll.c:29)
|
||||
==2320427== by 0x50E09B8: ??? (in /usr/lib/x86_64-linux-gnu/libevent_core-2.1.so.7.0.1)
|
||||
==2320427== by 0x50DBCEC: event_base_loop (in /usr/lib/x86_64-linux-gnu/libevent_core-2.1.so.7.0.1)
|
||||
==2320427== by 0x4F1AAC5: ??? (in /usr/lib/x86_64-linux-gnu/libopen-pal.so.40.30.2)
|
||||
==2320427== by 0x4D78401: start_thread (pthread_create.c:442)
|
||||
==2320427== by 0x4E06743: clone (clone.S:100)
|
||||
==2320427==
|
||||
==2320427== HEAP SUMMARY:
|
||||
==2320427== in use at exit: 5,263,151,743 bytes in 121,171 blocks
|
||||
==2320427== total heap usage: 230,206 allocs, 109,035 frees, 5,285,767,114 bytes allocated
|
||||
==2320427==
|
||||
==2320429==
|
||||
==2320429== Process terminating with default action of signal 15 (SIGTERM)
|
||||
==2320429== at 0x4DF912F: poll (poll.c:29)
|
||||
==2320429== by 0x50E09B8: ??? (in /usr/lib/x86_64-linux-gnu/libevent_core-2.1.so.7.0.1)
|
||||
==2320429== by 0x50DBCEC: event_base_loop (in /usr/lib/x86_64-linux-gnu/libevent_core-2.1.so.7.0.1)
|
||||
==2320429== by 0x4F1AAC5: ??? (in /usr/lib/x86_64-linux-gnu/libopen-pal.so.40.30.2)
|
||||
==2320429== by 0x4D78401: start_thread (pthread_create.c:442)
|
||||
==2320429== by 0x4E06743: clone (clone.S:100)
|
||||
==2320429==
|
||||
==2320429== HEAP SUMMARY:
|
||||
==2320429== in use at exit: 5,262,646,978 bytes in 121,271 blocks
|
||||
==2320429== total heap usage: 230,016 allocs, 108,745 frees, 5,284,059,066 bytes allocated
|
||||
==2320429==
|
||||
284
cal.py
284
cal.py
@ -1,284 +0,0 @@
|
||||
#!/usr/bin/python
|
||||
# -*- coding: UTF-8 -*-
|
||||
|
||||
from multiprocessing import set_forkserver_preload
|
||||
import os
|
||||
import os.path
|
||||
from posixpath import split
|
||||
from random import sample
|
||||
import re
|
||||
import shutil
|
||||
from time import monotonic, sleep
|
||||
from tokenize import Number
|
||||
|
||||
# global limit
|
||||
CUTOFF = 3600
|
||||
PUNISH = 2 #PAR2
|
||||
MEMS_MAX = 61440 # 60G
|
||||
|
||||
class states(object):
|
||||
res = "unknown"
|
||||
time = CUTOFF*PUNISH
|
||||
mems = MEMS_MAX
|
||||
mono = False # only this one can solve
|
||||
best = False # show the best performance
|
||||
ls_time = 0 # LS_time
|
||||
|
||||
class solver(object):
|
||||
def __init__(self, res_dir, name):
|
||||
self.res_dir = res_dir # save the results files
|
||||
self.print_name = name # names want to show
|
||||
self.datas = dict() # datas[ins] save the instances
|
||||
def reset(self):
|
||||
# SAT-ins UNSAT-ins solved-ins all-ins
|
||||
self.sat_num = self.unsat_num = self.solved_num = self.all_num = 0
|
||||
self.avg_sat_time = self.avg_unsat_time = self.avg_solved_time = self.avg_all_time = 0.0
|
||||
self.PAR_sat_time = self.PAR_unsat_time = self.PAR_solved_time = self.PAR_all_time = 0.0
|
||||
self.mono_num = 0
|
||||
self.best_num = 0
|
||||
def cal_soln(self, ins_name):
|
||||
self.all_num += 1
|
||||
state = self.datas[ins_name]
|
||||
if(self.datas[ins_name].time > CUTOFF):
|
||||
self.datas[ins_name] = states()
|
||||
if(state.res=="sat"):
|
||||
self.sat_num += 1
|
||||
self.solved_num += 1
|
||||
self.avg_sat_time += state.time
|
||||
self.avg_solved_time += state.time
|
||||
self.avg_all_time += state.time
|
||||
self.PAR_sat_time += state.time
|
||||
self.PAR_solved_time += state.time
|
||||
self.PAR_all_time += state.time
|
||||
elif(state.res=="unsat"):
|
||||
self.unsat_num += 1
|
||||
self.solved_num += 1
|
||||
self.avg_unsat_time += state.time
|
||||
self.avg_solved_time += state.time
|
||||
self.avg_all_time += state.time
|
||||
self.PAR_unsat_time += state.time
|
||||
self.PAR_solved_time += state.time
|
||||
self.PAR_all_time += state.time
|
||||
else:
|
||||
self.avg_all_time += CUTOFF
|
||||
self.PAR_all_time += CUTOFF * PUNISH
|
||||
def deal_avg(self):
|
||||
if(self.sat_num>0):
|
||||
self.avg_sat_time /= self.sat_num
|
||||
self.PAR_sat_time /= self.sat_num
|
||||
if(self.unsat_num>0):
|
||||
self.avg_unsat_time /= self.unsat_num
|
||||
self.PAR_unsat_time /= self.unsat_num
|
||||
if(self.solved_num>0):
|
||||
self.avg_solved_time /= self.solved_num
|
||||
self.PAR_solved_time /= self.solved_num
|
||||
if(self.all_num>0):
|
||||
self.avg_all_time /= self.all_num
|
||||
self.PAR_all_time /= self.all_num
|
||||
def to_string(self, state):
|
||||
line = ""
|
||||
line += str(state.res) + " "
|
||||
line += str(round(state.time,2))
|
||||
if state.mono:
|
||||
line += "[M]"
|
||||
elif state.best:
|
||||
line += "[B]"
|
||||
# if (state.byCDCL):
|
||||
# line += "{C}"
|
||||
# elif(state.byLS):
|
||||
# line += "{L}"
|
||||
line += str()
|
||||
return line.ljust(18)
|
||||
|
||||
return super().to_string(state)
|
||||
|
||||
|
||||
class solver_SAT_standard_gnomon(solver):
|
||||
def cal_soln(self, ins_name):
|
||||
if(not ins_name in self.datas):
|
||||
self.datas[ins_name] = states()
|
||||
real_file_path = self.res_dir + "/" + ins_name
|
||||
fstr = open(real_file_path, "r").read()
|
||||
|
||||
if(not len(re.findall(r"s\s+UNSATISFIABLE", fstr))==0):
|
||||
self.datas[ins_name].res = "unsat"
|
||||
elif(not len(re.findall(r"s\s+SATISFIABLE", fstr))==0):
|
||||
self.datas[ins_name].res = "sat"
|
||||
|
||||
if(not self.datas[ins_name].res == "unknown"):
|
||||
|
||||
timestr = re.findall(r"real\s+(\d+\.\d+)", fstr)[-1]
|
||||
|
||||
# timestr = re.findall(r"real.*m.*s", fstr)[-1]
|
||||
# minute = int(timestr.split('m')[0].split()[-1])
|
||||
# second = float(timestr.split('m')[-1].split('s')[0])
|
||||
self.datas[ins_name].time = float(timestr)
|
||||
if (self.datas[ins_name].time > CUTOFF*PUNISH):
|
||||
self.datas[ins_name].res="unknown"
|
||||
# confstr = re.findall(r"c conflicts:.*per second", fstr)[-1]
|
||||
# self.datas[ins_name].time = int(confstr.split()[-4])
|
||||
|
||||
return super().cal_soln(ins_name)
|
||||
def to_string(self, state):
|
||||
return super().to_string(state)
|
||||
|
||||
SOLVER_LEN = 20
|
||||
SAMPLE_LEN = 20
|
||||
NUMBER_LEN = 8
|
||||
print_title = True
|
||||
class calculater(object):
|
||||
solvers = []
|
||||
sample_dirs = [] # sample dirs, [sample_dir, sample_name]s
|
||||
def __init__(self, solvers, sample_dirs):
|
||||
self.solvers = solvers
|
||||
self.sample_dirs = sample_dirs
|
||||
def __show_in_mark_down(self, samp_name):
|
||||
global print_title
|
||||
if(print_title):
|
||||
print_title = False
|
||||
title = "| sample".ljust(SAMPLE_LEN+2)
|
||||
title += " | solver".ljust(SOLVER_LEN+3)
|
||||
title += " | #SAT".ljust(NUMBER_LEN+3)
|
||||
title += " | avg_t".ljust(NUMBER_LEN+3)
|
||||
title += " | #UNSAT".ljust(NUMBER_LEN+3)
|
||||
title += " | avg_t".ljust(NUMBER_LEN+3)
|
||||
title += " | #ALL".ljust(NUMBER_LEN+3)
|
||||
title += " | PAR2_t".ljust(NUMBER_LEN+3)
|
||||
title += " | best".ljust(NUMBER_LEN+3)
|
||||
title += " | mono".ljust(NUMBER_LEN+3)
|
||||
title += " | s".ljust(NUMBER_LEN+3)
|
||||
title += " | TIME".ljust(NUMBER_LEN+3)
|
||||
title += " |"
|
||||
print(title)
|
||||
|
||||
split = "| " + '-'*(SAMPLE_LEN)
|
||||
split += " | " + '-'*(SOLVER_LEN)
|
||||
split += " | " + '-'*(NUMBER_LEN)
|
||||
split += " | " + '-'*(NUMBER_LEN)
|
||||
split += " | " + '-'*(NUMBER_LEN)
|
||||
split += " | " + '-'*(NUMBER_LEN)
|
||||
split += " | " + '-'*(NUMBER_LEN)
|
||||
split += " | " + '-'*(NUMBER_LEN)
|
||||
split += " | " + '-'*(NUMBER_LEN)
|
||||
split += " | " + '-'*(NUMBER_LEN)
|
||||
split += " | " + '-'*(NUMBER_LEN)
|
||||
split += " | " + '-'*(NUMBER_LEN)
|
||||
split += " |"
|
||||
self.split_line = split
|
||||
print(split)
|
||||
|
||||
#sota = self.solvers[0].solved_num * self.solvers[0].PAR_solved_time + CUTOFF * PUNISH * (self.sample_ins_ct - self.solvers[0].solved_num)
|
||||
sota = self.solvers[0].PAR_all_time * self.sample_ins_ct
|
||||
|
||||
for slv in self.solvers:
|
||||
|
||||
s = (sota - CUTOFF * PUNISH * (self.sample_ins_ct - slv.solved_num)) / (slv.solved_num * slv.PAR_solved_time)
|
||||
|
||||
time = slv.solved_num * slv.PAR_solved_time + CUTOFF * PUNISH * (self.sample_ins_ct - slv.solved_num) / 1.5
|
||||
time = time / self.sample_ins_ct
|
||||
|
||||
line = "| " + (samp_name + "("+str(self.sample_ins_ct) + ")").ljust(SAMPLE_LEN)
|
||||
line += " | " + slv.print_name.ljust(SOLVER_LEN)
|
||||
line += " | " + str(slv.sat_num).ljust(NUMBER_LEN)
|
||||
line += " | " + str(round(slv.avg_sat_time,2)).ljust(NUMBER_LEN)
|
||||
line += " | " + str(slv.unsat_num).ljust(NUMBER_LEN)
|
||||
line += " | " + str(round(slv.avg_unsat_time,2)).ljust(NUMBER_LEN)
|
||||
line += " | " + str(slv.solved_num).ljust(NUMBER_LEN)
|
||||
line += " | " + str(round(slv.PAR_all_time,2)).ljust(NUMBER_LEN)
|
||||
line += " | " + str(slv.best_num).ljust(NUMBER_LEN)
|
||||
line += " | " + str(slv.mono_num).ljust(NUMBER_LEN)
|
||||
line += " | " + str(round(s,2)).ljust(NUMBER_LEN)
|
||||
line += " | " + str(round(time,2)).ljust(NUMBER_LEN)
|
||||
line += " |"
|
||||
print(line)
|
||||
|
||||
def cal_and_show(self):
|
||||
for sample in self.sample_dirs:
|
||||
title_line = ""
|
||||
for slv in self.solvers:
|
||||
title_line += slv.print_name.ljust(18)
|
||||
print(title_line)
|
||||
samp_dir = sample[0]
|
||||
samp_name = sample[1]
|
||||
print_line_ct = 0
|
||||
sample_ins_ct = 0
|
||||
for slv in self.solvers:
|
||||
slv.reset()
|
||||
for ins_name in open(samp_dir):
|
||||
sample_ins_ct += 1
|
||||
ins_name = ins_name.strip()
|
||||
best_time = CUTOFF*PUNISH
|
||||
solved_ct = 0
|
||||
for slv in self.solvers:
|
||||
slv.cal_soln(ins_name)
|
||||
best_time = min(slv.datas[ins_name].time, best_time)
|
||||
if not slv.datas[ins_name].res == "unknown":
|
||||
solved_ct += 1
|
||||
if(not best_time == CUTOFF*PUNISH):
|
||||
for slv in self.solvers:
|
||||
if(slv.datas[ins_name].time == best_time):
|
||||
slv.datas[ins_name].best = True
|
||||
slv.best_num += 1
|
||||
if(solved_ct == 1):
|
||||
slv.datas[ins_name].mono = True
|
||||
slv.mono_num += 1
|
||||
|
||||
|
||||
line = ""
|
||||
no_answer = True
|
||||
answer_this = "unknown"
|
||||
all_can_solve = True
|
||||
have_diff_res = False
|
||||
for slv in self.solvers:
|
||||
stt = slv.datas[ins_name]
|
||||
line += slv.to_string(stt)
|
||||
if(not stt.res == "unknown"):
|
||||
no_answer = False
|
||||
answer_this = stt.res
|
||||
elif(stt.res == "unknown"):
|
||||
all_can_solve = False
|
||||
line += ins_name
|
||||
if(not all_can_solve and not no_answer):
|
||||
have_diff_res = True
|
||||
|
||||
# if(True):
|
||||
if(False):
|
||||
# if(no_answer):
|
||||
# if(all_can_solve):
|
||||
# if(have_diff_res):
|
||||
# if(have_diff_res and answer_this == "sat"):
|
||||
# if(self.solvers[-2].datas[ins_name].res != self.solvers[-1].datas[ins_name].res):
|
||||
print_line_ct += 1
|
||||
print(line)
|
||||
|
||||
self.sample_ins_ct = sample_ins_ct
|
||||
for slv in self.solvers:
|
||||
slv.deal_avg()
|
||||
self.__show_in_mark_down(samp_name)
|
||||
if(print_line_ct>0):
|
||||
print("print line ct = ", print_line_ct)
|
||||
else:
|
||||
print(self.split_line)
|
||||
|
||||
|
||||
def gen_samples(dir):
|
||||
samples = []
|
||||
for root, dirs, files in os.walk(dir):
|
||||
for file in files:
|
||||
sample_name = file.strip(".txt")
|
||||
sample_dir = os.path.join(root, file)
|
||||
# print(sample_dir, sample_name)
|
||||
samples.append([sample_dir, sample_name])
|
||||
return samples
|
||||
|
||||
if __name__ == "__main__":
|
||||
solvers = []
|
||||
solvers.append(solver_SAT_standard_gnomon("./result","light-cloud-circle"))
|
||||
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/huawei_sat/kissat-mab","origin-mab"))
|
||||
# solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/huawei_simp/kissat-mab","preprocess-mab"))
|
||||
samples = []
|
||||
samples.append(["/pub/data/chenzh/data/sat2022/all.txt", "dump_sat"])
|
||||
clt = calculater(solvers, samples)
|
||||
clt.cal_and_show()
|
||||
|
||||
|
||||
263
nohup.log
263
nohup.log
@ -1,263 +0,0 @@
|
||||
exp-result-seed10 a7b23445c21b27eb3c918c1e96ba25df-hyp_cec_multi_1.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 a7cb2567e1f5b7ec2f4ba09931e29b96-s2n:s2n_stuffer_write_base64.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 aa4638ca3654f1a300c809125a3133ee-6s22_Iter57.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 aad5bbe8920c5afc84068bb1da27ee8f-LABS_n041_goal003.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 ab660e179140ea816eca23098fd50078-sum_of_three_cubes_33_unknown_representation.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 ac6256657058fe65dc7ddaf773ab83bf-SC21_Timetable_C_527_E_71_Cl_35_S_35.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 ae5f6e83a289d226a353efd95b663717-6s22_Iter99.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 af63ce577d1fea121ba80b4b1d148f0c-sudoku-N30-22.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 af834fd3ce15078d2ab055c996758c00-sum_of_three_cubes_33_known_representation.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 b043968ec004b4ac19eb31926c24d22c-mdp-36-11-unsat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 b1c44904cf06682f973b60c8282f45e8-mp1-squ_ali_s10x10_c39_bail_SAT.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 b24684abee2e253a4aee233eed155a5b-GP_100_948_34.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 b29cb3449d70126d186e1f6a4fccc419-pj2015_k9.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 b2bcdd97e7d0ca8858b412eb34b26ba9-hyp_cec_multi_5.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 b344f80cef9889d952c76736d0ad92d9-9dlx_vliw_at_b_iq6.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 b3828c92f2c77f8d7581570685679d76-sin_depth_miter_8.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 b3cf73d0383f781adf09a2192fa03a15-string_compare_safety_cbmc_unwinding_670.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 b51583e32432c5778c7e3e996c3bfeba-sqrt_ineq_3.c.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 b88d206fb35ef87bd7ec5d4a1430ae0c-20-100-p100-55_sat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 b8d10f8c82a85c03c000fbd005e5a838-worker_50_150_40_0.85.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 b8e3b884886922343f5cb72d92c24b97-frb75-13-2.used-as.sat04-878.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 b8f9b018d16835c564dcd8395118c79f-aws-encryption-sdk-c:aws_cryptosdk_priv_hdr_parse_alg_id.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 b913c17d26ac9f3ad15fa83dc98960c7-sudoku-N30-27.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 b96071f89fa1b1670b8375010b1dd42b-SCPC-500-9.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 b962abe508e5a677dbce14056111b48b-j3037_1_rggt_bm1.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 ba8621490e4e7212fffdb55fb6bd282d-combined-crypto1-wff-seed-108-wffvars-500-cryptocplx-31-overlap-2.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 bb0613595001749a0ada02f2da85bc89-PancakeVsInsertSort_7_7.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 bb80971144a5423532aea9424dade891-div-mitern174.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 bc16508e3f279bec0a072b939bbe6440-af-synthesis_stb_50_40_2_sat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 bcb2104a3558d87ac3b2107c10d54648-mp1-blockpuzzle_5x12_s6_free3.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 bd5bc8b7711b75f3cd3ad935bf000659-af-synthesis_stb_50_20_8_unsat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 be2b20414899ed839ac14bf8b9365692-pj2016_k140.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c0d927c372e355081aa1f537cc910843-GP_100_948_32.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c0df94532b1ca8a705d3af05378f377d-SCPC-500-20.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c1b30b4e03c3024ad9d084e29e79aa46-BubbleVsPancakeSort_6_6.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c1cb62f85f0c6a29c5d3c47d25fbc24a-Carry_Bits_Fast_23.cnf.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c221c5dc006de79e561124dab52aae82-mdp-28-12-unsat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c23aed727ae2d9cbb888d771991995aa-tseitin_grid_n16_m16.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c2596b3f0d779d532a667962b1e54b42-pj2008_k300.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c2828483a78420f9a90e3ed9728c06cc-GP_100_951_37.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c2894b8d82492f03bb73bbc65896c016-aws-c-common:aws_priority_queue_s_remove_node.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c2f827691e524e272d21de55b3749877-GP_100_951_35.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c33dc89922f1ddea4e7eeddafe4143b3-reconf20_20_grid10_1_6141.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c3b4a96d92da617218449abad4334d6d-div-mitern164.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c3de1f05d136b8ec420732ca829f3217-corePKCS11:C_CreateObject.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c5be40965caf3abdba3994ff3d1f32b6-grid-color-12-14-4-cb.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c846dfb21b50596aef8fbe5591d75eb0-UNSAT_MS_opt_snake_p20.pddl_29.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c98459d6a1763d809729e276b9c4cbbd-linked_list_swap_contents_safety_unwind74.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 c9886f58320a360adbc8db9470563bea-ctl_4291_567_12_unsat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 ca6db14aaa04027d2b8af47ec910bd68-cfi-rigid-s2-0064-04-or_2.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 cac1c09f968ef8654c499156d1292385-SCPC-500-18.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 cb3c725fd30d50c6785b907054194260-worker_40_40_30_0.9.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 cb8f9ffb66d9b5ef663e6759be0b5e4e-q_query_3_L200_coli.sat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 cbd7e28e510e658abbbe312bdffc6407-worker_50_50_50_0.85.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 ccb55d1b802617fcb969e12859d66124-g2-mizh-md5-48-2.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 cd1585619fea2f2634525a3663873764-linked_list_swap_contents_safety_unwind55.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 cd361d33986dccd7f2d86016d6c35241-ecarev-110-4099-22-30-7.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 cd36b290c27ed9bafedfb2ca88469f01-mdp-28-12-sat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 cd72a64e1b857fd30b9ec831cf462bf1-mp1-21.7.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 cd7c8f8aa9901293a9bc31839eafcc40-reconf10_42_queen20_4_0961.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 cda0871abcaa41bb403207731bd24fe5-af-synthesis_stb_50_100_4_unsat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 cdcdc78497a72d622493b1bac4f0f28b-reconf20_26_3-FullIns_4_1.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 ce32731c73701c2ac2bed5341b6ae3ca-mp1-9_27.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 ce4345ce697134021029c2686d5eb04c-Carry_Save_Fast_3.cnf.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 cf194dbcba619ea53edb4170c056ac5b-grid-color-14-14-14-cb.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 cfa14a7015b0f7fecd98e898f3c95896-velev-vliw-sat-4.0-b8.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d065d395159d19735706e0b5cb823f17-af-synthesis_stb_50_20_8_sat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d0ee45ac97c6b5cc63a528f46a5797aa-linked_list_swap_contents_safety_unwind44.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d1a4dc04e54d4fa58dfbbf61bd2415b4-SC22_Timetable_C_451_E_50_Cl_30_S_28.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d1dbf88a58406c931fd696267ed8159e-s2n:s2n_stuffer_private_key_from_pem.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d1f5c3af78f13f39595288976115d7d3-3d_perfect_euler_bricks.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d21199e73859ca35386912c5c475d6c7-tseitin_n192_d3.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d32a1553afeebf44835370c9567b3598-cfi-rigid-t2-0048-01-or_3_shuffle_all.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d3c07914f3ebb42906b986aa431243af-summle_X8646_steps8_I1-2-2-4-4-8-25-100.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d3c22bb79a638adc35682226f35e3bc4-pj2003_k9.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d40af7b45bba9c64033c0dd47b07f4a4-mdp-36-16-sat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d518d21a9d851741940749cb59f558af-rphp_p6_r28.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d60f78323b957025e55ca528d641b83b-SC22_Timetable_C_451_E_48_Cl_30_S_27.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d6947217ad779e1175c716cca42525c6-summle_X111113_steps7_I1-2-2-4-4-8-25-100.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d6c845a5f92ebc059b3f0ab2f6d395ed-cfi-rigid-z2-0088-02-or_2_shuffle_all.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d702aa8568706efda8308ef8d24f907b-div-mitern167.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d7039acbd2f060fe1e32a273b07c2c77-sudoku-N30-29.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d78819115db81dee343d7777fbc5844f-cfi-rigid-s2-0064-02-or_2.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d79e09d2a1639a01528c0703df4d4946-pj2008_k400.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d7f273dc6e97efe55c8b7f9cc547eb2d-sin_depth_miter_1.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d8602e623f87dd33f4a1a69ee42d15be-reconf20_50_grid10_3_6844.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d87714e099c66f0034fb95727fa47ccc-Wallace_Bits_Fast_2.cnf.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d892eb7b3b3a44192ee639e222eee058-reconf10_99_Ins_3_1.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d8bb23406e76bf5a4b7a6edba8784a74-Lab-Project-FreeRTOS-Cellular-Library:Cellular_ATRemoveTrailingWhiteSpaces.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d90c519010bfda89d1626c0321a55a64-j3045_10_gmto_bm1.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 d9e9100c382d44fb67af82f8d69814f1-cfi-rigid-t2-0048-03-or_3_shuffle_all.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 dcac26e190c906c61ac7222d6d4628c7-grid-color-14-14-12-cb.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 dd0196aee30d0a83b6fe8bc7eba01806-aws-encryption-sdk-c:aws_cryptosdk_priv_hdr_parse_iv.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 ddc7ca4c5dcb102a3ecc63721498f746-SC22_Timetable_C_436_E_39_Cl_29_S_27.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 ddcb0cd9b7bca43c3a5189326ae88aab-linked_list_swap_contents_safety_unwind71.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e011c703e4a2ff46069ec2af2997b580-sin_depth_miter_6.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e01c39b7b41c9ff1621579b747254fab-ncc_none_3001_7_3_3_1_31_435991723.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e02e21075d3bb8b0e64ea9b8122c75ff-PancakeVsInsertSort_6_7.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e0b938c32e36e2939d712dd4024f9ec6-j3037_9_mdd_b.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e28cf003c086c99f3a3d9a90aebf8ed1-intel046_Iter124.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e4128445a07bb86afca1f3590d9adfa9-worker_80_80_80_0.8.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e436f6303d3f499969eafe05b0914a4b-bmc_QICE_snp_vld_50.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e47567e16e4aeb4d8f3806dfbfdfd646-sudoku-N30-8.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e4f345877ba5fa2b8fb26be06a123748-rphp_p105_r105.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e55a49d8065d65650f24c0f3ecef30b6-af-synthesis_stb_50_120_4_unsat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e5f5dbace0183455d167a88100312c34-Nb52T6.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e6f793931983295561620a027d9b3e95-mdp-36-14-unsat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e7c0d40392681b1a55d5d3c826a26766-reconf20_116_le450_25c_1.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e7cd2c407974b35fa97f8e64a691bfa0-j3037_10_gmto_b.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e85b6cb3e2751d5c80559433ba1adf06-vlsat2_24450_2770239.dimacs.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e8d9e3a985463b8e4f45b6e09b77bf6c-cfi-rigid-t2-0048-02-or_3_shuffle_all.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e97ebde59cb17ef6f7c4430224b21ed1-grid-color-14-14-8-cb.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e992a45933d191dc4fbe8cc4836109f8-sum_of_three_cubes_165_known_representation.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e99ce61fe251b404ec85f6246fd4bb19-Wallace_Bits_Fast_7.cnf.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 e9b4369f9a98e397ac69eb7740ffef49-Carry_Save_Fast_2.cnf.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 ea8a79747c7ab142a897b7e8e638245f-j3045_4_mdd_b.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 eb659cd21250abdc8c9cec49073c32c6-linked_list_swap_contents_safety_unwind59.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 eb8a25e0db5d0605e3e15670f7a07f27-grid-color-14-14-2-cb.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 ed410c758e5025f1bb97922574d1c2ff-reconf10_86_sp003_1.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 ed6920e7126f57daabfb85415607fdb5-sum_of_three_cubes_906_unknown_representation.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 ee06244cc0ed073bd6abf147dc27eff6-pj2016_k120.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 eede03732955f620b5291f9dcf9f95df-tseitin_n200_d3.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 efc1b836380d0f84e7512f7b2ccdbb60-PancakeVsInsertSort_8_5.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 f0f279c7d5043e783f73237cf6bddf33-Break_triple_20_72.xml.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 f1afd5e8d4b842c15c6a2c420b2b2dba-pj2018_k10.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 f1b3d254596523910f3af07fc1942e64-Break_unsat_12_19.xml.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 f2a73aa514c859c91db462e1e2a1315b-af-synthesis_stb_50_140_1_sat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 f5f1d6a47ed7449a18d872a3f93d8aa5-GP_120_400_15.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 f64806fd4fe79f1efaefa7ce68d93ee1-sin_depth_miter_4.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 f8a966a2ba189ad5fa45f870f3c5e200-sudoku-N30-7.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 f8ad493b11bf0692c1f3919642cebdb1-PancakeVsInsertSort_9_3.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 f8b7241f662ab4d36337b74bb7984122-summle_X111119_steps7_I1-2-2-4-4-8-25-100.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 f9dd957b2f5940a3e3adaa2eeaaba011-mdp-36-12-sat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 fa88b447f6b41b04686085480678affe-UNSAT_H_instances_childsnack_p12.hddl_1.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 fb5cf4ad3c46dd294eb8253218524ba6-cfi-rigid-r2-0072-01-or_3.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 fbf3b9f8a03a1efedae3da04622fe96e-sqrt-mitern168.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 fca7a5a04aaed5f0eacccc4139dc894a-satcoin-genesis-SAT-8192.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 fdfd5975c57d7cd2264ef6aff6cb4815-SE_PR_stb_588_138.apx_1.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 fe800e62b55609cb152965c223e72280-div-mitern171.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 fe96b630b3e761821308b544368dd521-GP_100_950_34.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 fec4ba2cf2416933dcf7b8153be97344-bz-X-4-7-6.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 fee70cede2b5b55bfbdb6e48fbe7ce4f-DLTM_twitter690_74_16.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 ff3be72b9f5f44036875aa48f5434456-worker_20_60_20_0.9.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result-seed10 fff3f8c76467cdf9d92689969fd94281-mod2c-rand3bip-sat-240-2.shuffled-as.sat05-2519.cnf --share=1 --threads=32 --times=3600
|
||||
p-result 5e66b728b2445ec69f27e0f1a49f4b29-006.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 5e933a625099cc1ec6a8299a7848a2ae-Kakuro-easy-112-ext.xml.hg_7.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 5f24ae73bb2a0ec3bef68d8a9680f04f-af-synthesis_stb_50_80_7_unsat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 5ff92b9fa31963608674761e0d71fce8-sv-comp19_prop-reachsafety.triangular-longer_false-unreach-call.i-witness.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 608941b989227d93c62b3a9b4280011b-summle_X8639_steps8_I1-2-2-4-4-8-25-100.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 60a0ab2650e08f32c4fff6ff09369568-eqsparcl12bpwtrc12.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 61175b10026fe42cadd5e2f0088684ea-6s105_Iter99.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 622787535593269d5e9a1dc4fe01c4af-atco_enc1_opt2_10_16-sc2014.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 65138afdf7eb054be5131f2b0de84369-satch2ways12u.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 65514d6ff224df20ba8c1aeec1698ab6-PancakeVsInsertSort_8_7.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 6901858f1edbe3b1d327902dab720326-reconf20_20_grid10_4_4957.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 6965d5369d3ab26daaf074303c3d1739-mp1-squ_ali_s10x10_c39_abix_SAT.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 6a3e3d3a65a46608b44d81f9e4621087-6s105_Iter35.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 6b0dfcfa8cf0c0564f17ec0a5434b5b9-ITC2021_Early_4.xml.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 6b630aa05142274d965c8fc019db511e-bmc_QICE_rxrsp_vld_30.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 6b7e3415d7bd20be605b1f9723c43d68-Carry_Bits_Fast_5.cnf.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 6c34b7032712e16b08d97a0449d610e2-puzzle30_sat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 6d815089fb4095208754622b4c44a8f7-Carry_Bits_Fast_12.cnf.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 6dd57612dab7692b8c38225bb852ce36-hwmcc15deep-6s516r-k18-sc2017.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 6e1b970d637fca70d08b251766edade3-Nb8T61.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 6e3015f2ce1f17e4f2b81dae06d73eec-gus-md5-11.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 6e3ba15d8b33f40738f7e7d7355799a5-SC22_Timetable_C_436_E_41_Cl_29_S_27.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 6f956a3f95ccaf35a3de1fe72b9cf79e-soelberg_unit_109.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 6fa8b4b7f4b059bd46913dbe741c0b94-mdp-36-11-sat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 6fb0757ee018642fedd0669aad3882fe-grid-color-12-14-10-cb.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7016d1da3fdfe543de3b95f96a9ffe4c-summle_X8651_steps8_I1-2-2-4-4-8-25-100.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7018eff980d8183192d7a309e508b320-grid-color-14-14-10-cb.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 70289686a242c8380ca26bda45ad1278-summle_X111104_steps6_I1-2-2-4-4-8-25-100.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7101289c67f4c4ba117ad06ebb7d18a0-6s184.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 72329bc80f5f55dcc356a22f3f11ebec-GP_200_313_5.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 73ef1e87dbb7965ecb558e62dedb3a0c-SCPC-500-8.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7703f7d1901ff09a0f177c52a1a7c107-linked_list_swap_contents_safety_unwind43.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 78a0e76b68b536e2ea7d801fc6061cd2-grid-color-12-14-14-cb.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 78cdffdf5bbb89beb753f9ffab7fa45f-sudoku-N30-6.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7993005e2949524b293b216ed9c65126-cfi-rigid-s2-0064-03-or_2_shuffle_all.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7a236bb9e1566b80fa7b593a7e973efa-SCPC-500-16.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7a67847b81b414d659f005200cf56f6b-size_5_5_5_i198_r12.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7ab6615515ffc5ceb8f6bd440d159c3d-pj2016_k80.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7acf6cf25ddaf2ab98106e0bb3b9ddb1-af-synthesis_stb_50_140_3_sat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7adc1ade3384505af00ff8f7be23f5bd-ex175_20.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7af73f846548141cc97b8a149a20bfbf-vlsat2_57038_10572502.dimacs.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7b933d3e6b425772ed19eb0fec52bbf9-j3037_1_rggt_b.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7c15baa29f2228703e5161bfabd91773-reconf10_140_queen6_1.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7c6a06895899eab7cb83b658898ac327-reconf10_145_queen6_2.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7d2199baf2526263b5f753d290d2790b-md4__zeroOut_19__freeIn_23__seed_2.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7d9025b2f7e76f783a4ae5e8c9bf8e5c-4d_euler_bricks.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7e5396d6b00b82c2fc0ea1d7c6505afd-manthey_single-ordered-initialized-w50-b7.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7e9318578a6bdd7dfa9fc261be8a0839-PancakeVsSelectionSort_7_7.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7edaa759315f3762eee756c5bb843599-SC22_Timetable_C_436_E_42_Cl_29_S_27.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7efdf72de31fa82aeceb7acbc29a59bf-vlsat2_113_1150.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7f09f477d319cd79821c80504aa06a6e-Break_16_56.xml.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7f4d55b70c61ffc611a58e01d52c19bb-SCPC-500-11.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7fe153ced2c966dcdeb42b6714b4d6b7-sudoku-N30-11.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 7ff8c9781b3ada449ce489cdf444a760-Break_unsat_10_15.xml.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 80023e9fd0e627f71c2d953432613b5f-hyp_cec_multi_4.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 807133f4461a11e39a390dfcf67a4fc6-summle_X11113_steps8_I1-2-2-4-4-8-25-100.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 810ce4a78bc01ddc5a043d95f9584f2f-005-80-12.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 81b674a2aa6fbda9b06cf8ea334ddc44-beempgsol2b1.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 81e73c41a76d7b432cf86c43ffe23986-PancakeVsInsertSort_8_6.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 85aa1f0820da17412b8ee803b4a85207-sudoku-N30-4.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 885c0d25480fe4db3cd5d3b4bc044e76-SCPC-500-17.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 889b6d29998ade866e64c46f807a98bc-6s320rb1_Iter9.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 88bfa72210baef40a2903d95044dc19d-linked_list_swap_contents_safety_unwind40.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 8aee61ed27bf700a548ca9c097203749-SAT_MS_sat_snake_p01.pddl_39.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 8bb5819a23a8f1dff851d608bec008ca-ITC2021_Late_6.xml.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 8bfbffbfea9e5a5993bc024f39adff84-worker_40_80_40_0.85.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 8c0af30cc2a89e3fee97852633bed956-div_miter_lec_1.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 8c8b72ac19c0f93813b614a18abaf512-aws-encryption-sdk-c:aws_cryptosdk_keyring_trace_eq.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 8e659f42dd85a193fccc9cbbcc4627ed-sum_of_three_cubes_3_unknown_representation.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 8efdd60faa21ddcace492bff0479408b-Break_triple_20_54.xml.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 8f3d4a4fedf4689ae0e6df362478d551-PancakeVsSelectionSort_7_6.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 90add18e4ee4facb4f37737a9a2602cc-SC22_Timetable_C_436_E_40_Cl_29_S_27.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 90e839c4b05d4a7ac011435921551060-SC22_Timetable_C_436_E_43_Cl_29_S_27.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 90ec6ff35305fed1d9a87a3ecd87238b-linked_list_swap_contents_safety_unwind48.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 918ca8da0cbca88dcd34b0a6dec2b770-GP_100_950_32.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 920bbe559da4ea37fd636605316a791c-SCPC-500-19.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 925c82e25f5391fc2f1f7a4a9e093cec-6s186_Iter99.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 928436a6e8edbcde2d82504a85c88853-rphp_p90_r90.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 93695f689b57cdb57c9b6d0d726e0f53-Break_triple_18_48.xml.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 95c00d0ae51d5d0a2a931ce82b77701f-af-synthesis_stb_50_140_0_sat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 96f6aab24720f070a02e637f7252b482-grid-color-12-14-8-cb.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 98dbd257808e551fd26cad78ba520955-ITC2021_Late_2.xml.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 9954ccd77da65ad003b73bf38de3bd78-4d_perfect_euler_bricks.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 9cdf94203777c9f036f412bef1cc7c85-tseitin_n196_d3.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 9cea216ba8c5051e489af11150504ba6-Break_20_36.xml.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 9e35558ea8ffba630cd8c8f90e14af14-string_compare_safety_cbmc_unwinding_730.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 9f7ec7ef3a908c2e93b5553670a207b1-rphp_p14_r14.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result 9f901378a6feabcc94019a018a70d42b-sin-mitern29.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a09b0e7764666af044fa7e63dd7e7aef-PancakeVsSelectionSort_8_3.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a0e98fd44b74e6f255ca1e5a20bc01fd-cfi-rigid-d3-0180-02-orig.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a1158a2d8c8a1c6da02c2c4fcb32337f-6s158_Iter2.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a130a3f95891daed1bfd71c77bd2d8a1-SAT_dat.k80.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a2609893b71f219f4635d33ef1ff6eca-j3045_4_gmto_bm1.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a2bdae1f9d9695e8cf80cfbbd5f7d61f-PancakeVsSelectionSort_8_4.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a33d32bb816c0da62c7d946c18286a0d-SCPC-500-2.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a42230be4432b010789b6f97b090343c-soelberg_unit_223.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a4451734e7f5f2ce7b481688a693c4e9-worker_20_20_16_0.9.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a44fce1796383ea31df08af3b0f65db3-soelberg_unit_159.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a4bffff28417d6b4d72f7b9122988ba5-reconf10_68_queen15_2.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a58badecf3c901594f06d021f54c3a11-aws-c-common:aws_priority_queue_s_sift_either.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a5e0082efb1da4dabaa165c2bda5f85e-linked_list_swap_contents_safety_unwind41.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a65dfd8b3468d202ff3ba8731018622e-j3037_10_gmto_bm1.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a7aac5c83f236fd8b3de3275e3f5499d-edit_distance041_183.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a7b23445c21b27eb3c918c1e96ba25df-hyp_cec_multi_1.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result a7cb2567e1f5b7ec2f4ba09931e29b96-s2n:s2n_stuffer_write_base64.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result aa4638ca3654f1a300c809125a3133ee-6s22_Iter57.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result aad5bbe8920c5afc84068bb1da27ee8f-LABS_n041_goal003.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result ab660e179140ea816eca23098fd50078-sum_of_three_cubes_33_unknown_representation.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result ac6256657058fe65dc7ddaf773ab83bf-SC21_Timetable_C_527_E_71_Cl_35_S_35.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result ae5f6e83a289d226a353efd95b663717-6s22_Iter99.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result af63ce577d1fea121ba80b4b1d148f0c-sudoku-N30-22.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result af834fd3ce15078d2ab055c996758c00-sum_of_three_cubes_33_known_representation.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result b043968ec004b4ac19eb31926c24d22c-mdp-36-11-unsat.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result b1c44904cf06682f973b60c8282f45e8-mp1-squ_ali_s10x10_c39_bail_SAT.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result b24684abee2e253a4aee233eed155a5b-GP_100_948_34.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result b29cb3449d70126d186e1f6a4fccc419-pj2015_k9.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result b2bcdd97e7d0ca8858b412eb34b26ba9-hyp_cec_multi_5.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result b344f80cef9889d952c76736d0ad92d9-9dlx_vliw_at_b_iq6.cnf --share=1 --threads=32 --times=3600
|
||||
exp-result b3828c92f2c77f8d7581570685679d76-sin_depth_miter_8.cnf --share=1 --threads=32 --times=3600
|
||||
5661207
output.txt
5661207
output.txt
File diff suppressed because it is too large
Load Diff
@ -1,26 +0,0 @@
|
||||
#!/bin/bash
|
||||
|
||||
|
||||
make -j 8
|
||||
|
||||
cd ./docker
|
||||
cp ../light .
|
||||
|
||||
DOCKER_NETWORK="mallob-test"
|
||||
|
||||
|
||||
docker build --no-cache -f common.dockerfile -t light:common .
|
||||
docker build --no-cache -f leader.dockerfile -t light:leader .
|
||||
docker build --no-cache -f worker.dockerfile -t light:worker .
|
||||
|
||||
docker stop worker1
|
||||
docker stop worker2
|
||||
docker stop worker3
|
||||
|
||||
docker run -d --name worker1 --network $DOCKER_NETWORK --entrypoint bash --rm -t light:worker -c "/competition/init_solver.sh; exec bash"
|
||||
docker run -d --name worker2 --network $DOCKER_NETWORK --entrypoint bash --rm -t light:worker -c "/competition/init_solver.sh; exec bash"
|
||||
docker run -d --name worker3 --network $DOCKER_NETWORK --entrypoint bash --rm -t light:worker -c "/competition/init_solver.sh; exec bash"
|
||||
|
||||
docker stop leader
|
||||
|
||||
docker run -i --name leader --network $DOCKER_NETWORK --entrypoint bash --rm -t light:leader -c "/competition/init_solver.sh; exec bash"
|
||||
@ -1,24 +0,0 @@
|
||||
#!/bin/bash
|
||||
|
||||
instance="/pub/data/chenzh/data/sat2022"
|
||||
|
||||
run_solver(){
|
||||
solver=$1
|
||||
res_solver_ins=$2
|
||||
solver_args=$3
|
||||
if [ ! -d "$res_solver_ins" ]; then
|
||||
mkdir -p $res_solver_ins
|
||||
fi
|
||||
for dir_file in `cat $instance/all.txt`
|
||||
do
|
||||
file=$dir_file
|
||||
echo "$res_solver_ins $file $solver_args"
|
||||
touch $res_solver_ins/$file
|
||||
{ /usr/bin/time -f "\nreal\t%e\nuser\t%U\nsys\t%S\nmem\t%M\n" $solver $instance/$file $solver_args; } > $res_solver_ins/$file 2>&1
|
||||
done
|
||||
}
|
||||
|
||||
run_solver \
|
||||
'mpirun -np 9 --allow-run-as-root ./light -i ' \
|
||||
'exp-result'\
|
||||
'--share=1 --threads=32 --times=3600'
|
||||
@ -1,24 +0,0 @@
|
||||
#!/bin/bash
|
||||
|
||||
instance="/pub/data/chenzh/data/sat2022"
|
||||
|
||||
run_solver(){
|
||||
solver=$1
|
||||
res_solver_ins=$2
|
||||
solver_args=$3
|
||||
if [ ! -d "$res_solver_ins" ]; then
|
||||
mkdir -p $res_solver_ins
|
||||
fi
|
||||
for dir_file in `cat ./test.txt`
|
||||
do
|
||||
file=$dir_file
|
||||
echo "$res_solver_ins $file $solver_args"
|
||||
touch $res_solver_ins/$file
|
||||
{ /usr/bin/time -f "\nreal\t%e\nuser\t%U\nsys\t%S\nmem\t%M\n" $solver $instance/$file $solver_args; } > $res_solver_ins/$file 2>&1
|
||||
done
|
||||
}
|
||||
|
||||
run_solver \
|
||||
'mpirun -np 9 --allow-run-as-root ./light -i ' \
|
||||
'exp-result-seed10'\
|
||||
'--share=1 --threads=32 --times=3600'
|
||||
144
test.txt
144
test.txt
@ -1,144 +0,0 @@
|
||||
a7b23445c21b27eb3c918c1e96ba25df-hyp_cec_multi_1.cnf
|
||||
a7cb2567e1f5b7ec2f4ba09931e29b96-s2n:s2n_stuffer_write_base64.cnf
|
||||
aa4638ca3654f1a300c809125a3133ee-6s22_Iter57.cnf
|
||||
aad5bbe8920c5afc84068bb1da27ee8f-LABS_n041_goal003.cnf
|
||||
ab660e179140ea816eca23098fd50078-sum_of_three_cubes_33_unknown_representation.cnf
|
||||
ac6256657058fe65dc7ddaf773ab83bf-SC21_Timetable_C_527_E_71_Cl_35_S_35.cnf
|
||||
ae5f6e83a289d226a353efd95b663717-6s22_Iter99.cnf
|
||||
af63ce577d1fea121ba80b4b1d148f0c-sudoku-N30-22.cnf
|
||||
af834fd3ce15078d2ab055c996758c00-sum_of_three_cubes_33_known_representation.cnf
|
||||
b043968ec004b4ac19eb31926c24d22c-mdp-36-11-unsat.cnf
|
||||
b1c44904cf06682f973b60c8282f45e8-mp1-squ_ali_s10x10_c39_bail_SAT.cnf
|
||||
b24684abee2e253a4aee233eed155a5b-GP_100_948_34.cnf
|
||||
b29cb3449d70126d186e1f6a4fccc419-pj2015_k9.cnf
|
||||
b2bcdd97e7d0ca8858b412eb34b26ba9-hyp_cec_multi_5.cnf
|
||||
b344f80cef9889d952c76736d0ad92d9-9dlx_vliw_at_b_iq6.cnf
|
||||
b3828c92f2c77f8d7581570685679d76-sin_depth_miter_8.cnf
|
||||
b3cf73d0383f781adf09a2192fa03a15-string_compare_safety_cbmc_unwinding_670.cnf
|
||||
b51583e32432c5778c7e3e996c3bfeba-sqrt_ineq_3.c.cnf
|
||||
b88d206fb35ef87bd7ec5d4a1430ae0c-20-100-p100-55_sat.cnf
|
||||
b8d10f8c82a85c03c000fbd005e5a838-worker_50_150_40_0.85.cnf
|
||||
b8e3b884886922343f5cb72d92c24b97-frb75-13-2.used-as.sat04-878.cnf
|
||||
b8f9b018d16835c564dcd8395118c79f-aws-encryption-sdk-c:aws_cryptosdk_priv_hdr_parse_alg_id.cnf
|
||||
b913c17d26ac9f3ad15fa83dc98960c7-sudoku-N30-27.cnf
|
||||
b96071f89fa1b1670b8375010b1dd42b-SCPC-500-9.cnf
|
||||
b962abe508e5a677dbce14056111b48b-j3037_1_rggt_bm1.cnf
|
||||
ba8621490e4e7212fffdb55fb6bd282d-combined-crypto1-wff-seed-108-wffvars-500-cryptocplx-31-overlap-2.cnf
|
||||
bb0613595001749a0ada02f2da85bc89-PancakeVsInsertSort_7_7.cnf
|
||||
bb80971144a5423532aea9424dade891-div-mitern174.cnf
|
||||
bc16508e3f279bec0a072b939bbe6440-af-synthesis_stb_50_40_2_sat.cnf
|
||||
bcb2104a3558d87ac3b2107c10d54648-mp1-blockpuzzle_5x12_s6_free3.cnf
|
||||
bd5bc8b7711b75f3cd3ad935bf000659-af-synthesis_stb_50_20_8_unsat.cnf
|
||||
be2b20414899ed839ac14bf8b9365692-pj2016_k140.cnf
|
||||
c0d927c372e355081aa1f537cc910843-GP_100_948_32.cnf
|
||||
c0df94532b1ca8a705d3af05378f377d-SCPC-500-20.cnf
|
||||
c1b30b4e03c3024ad9d084e29e79aa46-BubbleVsPancakeSort_6_6.cnf
|
||||
c1cb62f85f0c6a29c5d3c47d25fbc24a-Carry_Bits_Fast_23.cnf.cnf
|
||||
c221c5dc006de79e561124dab52aae82-mdp-28-12-unsat.cnf
|
||||
c23aed727ae2d9cbb888d771991995aa-tseitin_grid_n16_m16.cnf
|
||||
c2596b3f0d779d532a667962b1e54b42-pj2008_k300.cnf
|
||||
c2828483a78420f9a90e3ed9728c06cc-GP_100_951_37.cnf
|
||||
c2894b8d82492f03bb73bbc65896c016-aws-c-common:aws_priority_queue_s_remove_node.cnf
|
||||
c2f827691e524e272d21de55b3749877-GP_100_951_35.cnf
|
||||
c33dc89922f1ddea4e7eeddafe4143b3-reconf20_20_grid10_1_6141.cnf
|
||||
c3b4a96d92da617218449abad4334d6d-div-mitern164.cnf
|
||||
c3de1f05d136b8ec420732ca829f3217-corePKCS11:C_CreateObject.cnf
|
||||
c5be40965caf3abdba3994ff3d1f32b6-grid-color-12-14-4-cb.cnf
|
||||
c846dfb21b50596aef8fbe5591d75eb0-UNSAT_MS_opt_snake_p20.pddl_29.cnf
|
||||
c98459d6a1763d809729e276b9c4cbbd-linked_list_swap_contents_safety_unwind74.cnf
|
||||
c9886f58320a360adbc8db9470563bea-ctl_4291_567_12_unsat.cnf
|
||||
ca6db14aaa04027d2b8af47ec910bd68-cfi-rigid-s2-0064-04-or_2.cnf
|
||||
cac1c09f968ef8654c499156d1292385-SCPC-500-18.cnf
|
||||
cb3c725fd30d50c6785b907054194260-worker_40_40_30_0.9.cnf
|
||||
cb8f9ffb66d9b5ef663e6759be0b5e4e-q_query_3_L200_coli.sat.cnf
|
||||
cbd7e28e510e658abbbe312bdffc6407-worker_50_50_50_0.85.cnf
|
||||
ccb55d1b802617fcb969e12859d66124-g2-mizh-md5-48-2.cnf
|
||||
cd1585619fea2f2634525a3663873764-linked_list_swap_contents_safety_unwind55.cnf
|
||||
cd361d33986dccd7f2d86016d6c35241-ecarev-110-4099-22-30-7.cnf
|
||||
cd36b290c27ed9bafedfb2ca88469f01-mdp-28-12-sat.cnf
|
||||
cd72a64e1b857fd30b9ec831cf462bf1-mp1-21.7.cnf
|
||||
cd7c8f8aa9901293a9bc31839eafcc40-reconf10_42_queen20_4_0961.cnf
|
||||
cda0871abcaa41bb403207731bd24fe5-af-synthesis_stb_50_100_4_unsat.cnf
|
||||
cdcdc78497a72d622493b1bac4f0f28b-reconf20_26_3-FullIns_4_1.cnf
|
||||
ce32731c73701c2ac2bed5341b6ae3ca-mp1-9_27.cnf
|
||||
ce4345ce697134021029c2686d5eb04c-Carry_Save_Fast_3.cnf.cnf
|
||||
cf194dbcba619ea53edb4170c056ac5b-grid-color-14-14-14-cb.cnf
|
||||
cfa14a7015b0f7fecd98e898f3c95896-velev-vliw-sat-4.0-b8.cnf
|
||||
d065d395159d19735706e0b5cb823f17-af-synthesis_stb_50_20_8_sat.cnf
|
||||
d0ee45ac97c6b5cc63a528f46a5797aa-linked_list_swap_contents_safety_unwind44.cnf
|
||||
d1a4dc04e54d4fa58dfbbf61bd2415b4-SC22_Timetable_C_451_E_50_Cl_30_S_28.cnf
|
||||
d1dbf88a58406c931fd696267ed8159e-s2n:s2n_stuffer_private_key_from_pem.cnf
|
||||
d1f5c3af78f13f39595288976115d7d3-3d_perfect_euler_bricks.cnf
|
||||
d21199e73859ca35386912c5c475d6c7-tseitin_n192_d3.cnf
|
||||
d32a1553afeebf44835370c9567b3598-cfi-rigid-t2-0048-01-or_3_shuffle_all.cnf
|
||||
d3c07914f3ebb42906b986aa431243af-summle_X8646_steps8_I1-2-2-4-4-8-25-100.cnf
|
||||
d3c22bb79a638adc35682226f35e3bc4-pj2003_k9.cnf
|
||||
d40af7b45bba9c64033c0dd47b07f4a4-mdp-36-16-sat.cnf
|
||||
d518d21a9d851741940749cb59f558af-rphp_p6_r28.cnf
|
||||
d60f78323b957025e55ca528d641b83b-SC22_Timetable_C_451_E_48_Cl_30_S_27.cnf
|
||||
d6947217ad779e1175c716cca42525c6-summle_X111113_steps7_I1-2-2-4-4-8-25-100.cnf
|
||||
d6c845a5f92ebc059b3f0ab2f6d395ed-cfi-rigid-z2-0088-02-or_2_shuffle_all.cnf
|
||||
d702aa8568706efda8308ef8d24f907b-div-mitern167.cnf
|
||||
d7039acbd2f060fe1e32a273b07c2c77-sudoku-N30-29.cnf
|
||||
d78819115db81dee343d7777fbc5844f-cfi-rigid-s2-0064-02-or_2.cnf
|
||||
d79e09d2a1639a01528c0703df4d4946-pj2008_k400.cnf
|
||||
d7f273dc6e97efe55c8b7f9cc547eb2d-sin_depth_miter_1.cnf
|
||||
d8602e623f87dd33f4a1a69ee42d15be-reconf20_50_grid10_3_6844.cnf
|
||||
d87714e099c66f0034fb95727fa47ccc-Wallace_Bits_Fast_2.cnf.cnf
|
||||
d892eb7b3b3a44192ee639e222eee058-reconf10_99_Ins_3_1.cnf
|
||||
d8bb23406e76bf5a4b7a6edba8784a74-Lab-Project-FreeRTOS-Cellular-Library:Cellular_ATRemoveTrailingWhiteSpaces.cnf
|
||||
d90c519010bfda89d1626c0321a55a64-j3045_10_gmto_bm1.cnf
|
||||
d9e9100c382d44fb67af82f8d69814f1-cfi-rigid-t2-0048-03-or_3_shuffle_all.cnf
|
||||
dcac26e190c906c61ac7222d6d4628c7-grid-color-14-14-12-cb.cnf
|
||||
dd0196aee30d0a83b6fe8bc7eba01806-aws-encryption-sdk-c:aws_cryptosdk_priv_hdr_parse_iv.cnf
|
||||
ddc7ca4c5dcb102a3ecc63721498f746-SC22_Timetable_C_436_E_39_Cl_29_S_27.cnf
|
||||
ddcb0cd9b7bca43c3a5189326ae88aab-linked_list_swap_contents_safety_unwind71.cnf
|
||||
e011c703e4a2ff46069ec2af2997b580-sin_depth_miter_6.cnf
|
||||
e01c39b7b41c9ff1621579b747254fab-ncc_none_3001_7_3_3_1_31_435991723.cnf
|
||||
e02e21075d3bb8b0e64ea9b8122c75ff-PancakeVsInsertSort_6_7.cnf
|
||||
e0b938c32e36e2939d712dd4024f9ec6-j3037_9_mdd_b.cnf
|
||||
e28cf003c086c99f3a3d9a90aebf8ed1-intel046_Iter124.cnf
|
||||
e4128445a07bb86afca1f3590d9adfa9-worker_80_80_80_0.8.cnf
|
||||
e436f6303d3f499969eafe05b0914a4b-bmc_QICE_snp_vld_50.cnf
|
||||
e47567e16e4aeb4d8f3806dfbfdfd646-sudoku-N30-8.cnf
|
||||
e4f345877ba5fa2b8fb26be06a123748-rphp_p105_r105.cnf
|
||||
e55a49d8065d65650f24c0f3ecef30b6-af-synthesis_stb_50_120_4_unsat.cnf
|
||||
e5f5dbace0183455d167a88100312c34-Nb52T6.cnf
|
||||
e6f793931983295561620a027d9b3e95-mdp-36-14-unsat.cnf
|
||||
e7c0d40392681b1a55d5d3c826a26766-reconf20_116_le450_25c_1.cnf
|
||||
e7cd2c407974b35fa97f8e64a691bfa0-j3037_10_gmto_b.cnf
|
||||
e85b6cb3e2751d5c80559433ba1adf06-vlsat2_24450_2770239.dimacs.cnf
|
||||
e8d9e3a985463b8e4f45b6e09b77bf6c-cfi-rigid-t2-0048-02-or_3_shuffle_all.cnf
|
||||
e97ebde59cb17ef6f7c4430224b21ed1-grid-color-14-14-8-cb.cnf
|
||||
e992a45933d191dc4fbe8cc4836109f8-sum_of_three_cubes_165_known_representation.cnf
|
||||
e99ce61fe251b404ec85f6246fd4bb19-Wallace_Bits_Fast_7.cnf.cnf
|
||||
e9b4369f9a98e397ac69eb7740ffef49-Carry_Save_Fast_2.cnf.cnf
|
||||
ea8a79747c7ab142a897b7e8e638245f-j3045_4_mdd_b.cnf
|
||||
eb659cd21250abdc8c9cec49073c32c6-linked_list_swap_contents_safety_unwind59.cnf
|
||||
eb8a25e0db5d0605e3e15670f7a07f27-grid-color-14-14-2-cb.cnf
|
||||
ed410c758e5025f1bb97922574d1c2ff-reconf10_86_sp003_1.cnf
|
||||
ed6920e7126f57daabfb85415607fdb5-sum_of_three_cubes_906_unknown_representation.cnf
|
||||
ee06244cc0ed073bd6abf147dc27eff6-pj2016_k120.cnf
|
||||
eede03732955f620b5291f9dcf9f95df-tseitin_n200_d3.cnf
|
||||
efc1b836380d0f84e7512f7b2ccdbb60-PancakeVsInsertSort_8_5.cnf
|
||||
f0f279c7d5043e783f73237cf6bddf33-Break_triple_20_72.xml.cnf
|
||||
f1afd5e8d4b842c15c6a2c420b2b2dba-pj2018_k10.cnf
|
||||
f1b3d254596523910f3af07fc1942e64-Break_unsat_12_19.xml.cnf
|
||||
f2a73aa514c859c91db462e1e2a1315b-af-synthesis_stb_50_140_1_sat.cnf
|
||||
f5f1d6a47ed7449a18d872a3f93d8aa5-GP_120_400_15.cnf
|
||||
f64806fd4fe79f1efaefa7ce68d93ee1-sin_depth_miter_4.cnf
|
||||
f8a966a2ba189ad5fa45f870f3c5e200-sudoku-N30-7.cnf
|
||||
f8ad493b11bf0692c1f3919642cebdb1-PancakeVsInsertSort_9_3.cnf
|
||||
f8b7241f662ab4d36337b74bb7984122-summle_X111119_steps7_I1-2-2-4-4-8-25-100.cnf
|
||||
f9dd957b2f5940a3e3adaa2eeaaba011-mdp-36-12-sat.cnf
|
||||
fa88b447f6b41b04686085480678affe-UNSAT_H_instances_childsnack_p12.hddl_1.cnf
|
||||
fb5cf4ad3c46dd294eb8253218524ba6-cfi-rigid-r2-0072-01-or_3.cnf
|
||||
fbf3b9f8a03a1efedae3da04622fe96e-sqrt-mitern168.cnf
|
||||
fca7a5a04aaed5f0eacccc4139dc894a-satcoin-genesis-SAT-8192.cnf
|
||||
fdfd5975c57d7cd2264ef6aff6cb4815-SE_PR_stb_588_138.apx_1.cnf
|
||||
fe800e62b55609cb152965c223e72280-div-mitern171.cnf
|
||||
fe96b630b3e761821308b544368dd521-GP_100_950_34.cnf
|
||||
fec4ba2cf2416933dcf7b8153be97344-bz-X-4-7-6.cnf
|
||||
fee70cede2b5b55bfbdb6e48fbe7ce4f-DLTM_twitter690_74_16.cnf
|
||||
ff3be72b9f5f44036875aa48f5434456-worker_20_60_20_0.9.cnf
|
||||
fff3f8c76467cdf9d92689969fd94281-mod2c-rand3bip-sat-240-2.shuffled-as.sat05-2519.cnf
|
||||
14
version.md
14
version.md
@ -1,14 +0,0 @@
|
||||
### 1.0
|
||||
base Framework
|
||||
RS
|
||||
#### 1.1
|
||||
Dynamically reseting
|
||||
#### 2.0
|
||||
Sharing (NPS)
|
||||
#### 3.-1
|
||||
Sharing (DPS)
|
||||
|
||||
## TODO
|
||||
- need merge (add option: NPS/DPS)
|
||||
- light_print ()
|
||||
- GE FME
|
||||
Loading…
x
Reference in New Issue
Block a user