Hi! I show below how to reproduce results from finite-automata-reduction (a decider method with 2 search algorithms):
first with my program (repo/PR),
then by chaining @TonyG’s implementation of what I call direct with @djmati1111’s implementation of what I call mitm_dfa.
This is not an independent repro when I do it, so I’d like an independent operator to please try matching these results. I hope this demo is helpful.
The starting point is index revision 758324e with 535801 machines.
As a proof of concept, I’ll show a shallow search (less time / fewer solutions) that still involves both search modes.
Result: direct up to 6 plus mitm_dfa up to 9 solve the attached 520258, leaving 15543.
FAR_direct6_mitm9.index.zst (1.1 MB)
My program (requires Rust):
[justinb@husk beaver]$ git clone -q -b finite-automata-reduction https://github.com/UncombedCoconut/bbchallenge-deciders.git
[justinb@husk beaver]$ cp -l all_5_states_undecided_machines_with_global_header bbchallenge-undecided-index/bb5_undecided_index bbchallenge-deciders/
[justinb@husk beaver]$ cd bbchallenge-deciders/decider-finite-automata-reduction/
[justinb@husk decider-finite-automata-reduction]$ cargo build -r -q
[justinb@husk decider-finite-automata-reduction]$ # Run in "server" mode for distributed solving.
[justinb@husk decider-finite-automata-reduction]$ # Once started, please also start `target/release/decider-finite-automata-reduction --ip <server IP>` once per CPU to use. I used 14 here.
[justinb@husk decider-finite-automata-reduction]$ # Note: if you add too many CPUs too soon, progress-bar counts may vary. (If iterations overlap, it may double-solve some TMs.)
[justinb@husk decider-finite-automata-reduction]$ target/release/decider-finite-automata-reduction -s --ip $(hostname -i) -p direct -x 0 -l 6 -p mitm_dfa -x 6 -l 9
Done! Worker shutdown takes ~60s.
520258+ 15543 ████████████████████░ All Deciders: 01:32:32
535801/ 535801 ~00:00:00 █████████████████████ direct-1 : 00:00:00
476473/ 476473 ~00:00:00 █████████████████████ direct-2 : 00:00:01
402339/ 402339 ~00:00:00 █████████████████████ direct-3 : 00:00:04
300100/ 300100 ~00:00:00 █████████████████████ direct-4 : 00:00:13
159340/ 159340 ~00:00:00 █████████████████████ direct-5 : 00:01:04
70562/ 70562 ~00:00:00 █████████████████████ direct-6 : 00:08:04
32632/ 32632 ~00:00:00 █████████████████████ mitm_dfa-7 : 00:05:58
28581/ 28581 ~00:00:00 █████████████████████ mitm_dfa-8 : 00:19:48
21048/ 21048 ~00:00:00 █████████████████████ mitm_dfa-9 : 00:57:53
Reproduction (requires C++ with Boost; Python with packages automata-lib, pillow, python-sat, z3; and Glucose):
[justinb@husk beaver]$ git clone -q https://github.com/TonyGuil/bbchallenge.git tonyg
[justinb@husk beaver]$ cp -l all_5_states_undecided_machines_with_global_header tonyg/SeedDatabase.bin
[justinb@husk beaver]$ cp -l bbchallenge-undecided-index/bb5_undecided_index tonyg/FAR/far_0.umf
[justinb@husk beaver]$ cd tonyg/FAR/
[justinb@husk FAR]$ c++ -Wall -O3 -oDecideFAR DecideFAR.cpp FAR_Decider.cpp FAR_Verifier.cpp -lboost_thread
[justinb@husk FAR]$ # Using more threads than cores helps. Don't get scared by these "elapsed time" figures: units are thread-seconds.
[justinb@husk FAR]$ for n in $(seq 6); do ./DecideFAR -N$n -Ifar_$((n-1)).umf -Ufar_$n.umf -Vfar_$n.dvf -M8; done
100% 535801 59328
Decided 59328 out of 535801
Elapsed time 16.060
100% 476473 74134
Decided 74134 out of 476473
Elapsed time 20.719
100% 402339 102239
Decided 102239 out of 402339
Elapsed time 90.505
100% 300100 140760
Decided 140760 out of 300100
Elapsed time 690.951
100% 159340 88778
Decided 88778 out of 159340
Elapsed time 5050.644
100% 70562 37930
Decided 37930 out of 70562
Elapsed time 41561.788
[justinb@husk FAR]$ cd ../..
[justinb@husk beaver]$ git clone -q https://github.com/colette-b/bbchallenge
[justinb@husk beaver]$ cd bbchallenge
[justinb@husk bbchallenge]$ # As the README file indicates, we need to customize the "paths.py" script.
[justinb@husk bbchallenge]$ echo "GLUCOSE_PATH = '/usr/bin/glucose-syrup'" >> paths.py
[justinb@husk bbchallenge]$ mkdir datafiles tempfiles
[justinb@husk bbchallenge]$ touch datafiles/cfl_proofs.txt
[justinb@husk bbchallenge]$ cp -l ../all_5_states_undecided_machines_with_global_header datafiles/
[justinb@husk bbchallenge]$ cp -l ../tonyg/FAR/far_6.umf datafiles/bb5_undecided_index
[justinb@husk bbchallenge]$ # Args are: mode ("database"), depth, threads, timeout. (For reproduction, use a huge time limit.)
[justinb@husk bbchallenge]$ for n in $(seq 7 9); do python3 main.py database $n 4 86400; done
Namespace(mode='database', n=7, threads=4, timeout=86400, idx=None, machine_code=None, instance_path=None, additional_acc=None, prooftype='vanilla', force_symmetric=False)
[... SNIP: detailed status info, showing only the last update for the 3 iterations ...]
100%|██████████████████████████████████▉| 32619/32632 [1:22:02<00:01, 6.63it/s]
100%|██████████████████████████████████▉| 28576/28581 [2:27:47<00:01, 3.22it/s]
100%|██████████████████████████████████▉| 21047/21048 [5:23:43<00:00, 1.08it/s]
[justinb@husk bbchallenge]$ # Convert this program's output to a bbchallenge index format:
[justinb@husk bbchallenge]$ python3 -c "from db_utils import *; proof_file_info(); open('../mitm.umf', 'wb').writelines(seed.to_bytes(4, 'big') for seed in all_undecided())"
82261it [00:00, 1128275.06it/s]
total_dfas_seen = 0
total_dfas_with_sink_state = 0
proof info:
length of index file: 32632
total idxs considered: 32632
solved with param n=7: 4051 left: 28581 12.4 percent success rate
solved with param n=8: 7533 left: 21048 26.4 percent success rate
solved with param n=9: 5505 left: 15543 26.2 percent success rate
left unsolved: 15543
82261it [00:00, 1325657.84it/s]
total_dfas_seen = 0
total_dfas_with_sink_state = 0
Finally, we have a decided index from my program and an undecided index from the other pair, so I check that they match:
justinb@husk bbchallenge]$ cd ..
[justinb@husk beaver]$ python3
Python 3.10.9 (main, Dec 19 2022, 17:35:49) [GCC 12.2.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> def read_index(path):
... with open(path, 'rb') as f:
... while (seed4 := f.read(4)):
... yield int.from_bytes(seed4, 'big')
...
>>> set(read_index('mitm.umf')) == set(read_index('bbchallenge-undecided-index/bb5_undecided_index')) - set(read_index('bbchallenge-deciders/decider-finite-automata-reduction/output/finite_automata_reduction.index'))
True