GroupsWithPropertyT/AutFN.jl

110 lines
3.1 KiB
Julia
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

using ArgParse
using Nemo
Nemo.setpermstyle(:cycles)
using Groups
using GroupRings
using PropertyT
import SCS.SCSSolver
#=
Note that the element
α(i,j,k) = ϱ(i,j)*ϱ(i,k)*inv(ϱ(i,j))*inv(ϱ(i,k)),
which surely belongs to ball of radius 4 in Aut(F) becomes trivial under the representation
Aut(F) GL() GL().
Moreover, due to work of Potapchik and Rapinchuk [1] every real representation of Aut(F) into GL() (for m 2n-2) factors through GL(), so will have the same problem.
We need a different approach: Here we actually compute in Aut(𝔽)
=#
function cpuinfo_physicalcores()
maxcore = -1
for line in eachline("/proc/cpuinfo")
if startswith(line, "core id")
maxcore = max(maxcore, parse(Int, split(line, ':')[2]))
end
end
maxcore < 0 && error("failure to read core ids from /proc/cpuinfo")
return maxcore + 1
end
function parse_commandline()
s = ArgParseSettings()
@add_arg_table s begin
"--tol"
help = "set numerical tolerance for the SDP solver (default: 1e-5)"
arg_type = Float64
default = 1e-5
"--iterations"
help = "set maximal number of iterations for the SDP solver (default: 20000)"
arg_type = Int
default = 20000
"--upper-bound"
help = "Set an upper bound for the spectral gap (default: Inf)"
arg_type = Float64
default = Inf
"--cpus"
help = "Set number of cpus used by solver (default: auto)"
arg_type = Int
required = false
"-N"
help = "Consider automorphisms of free group on N generators (default: N=3)"
arg_type = Int
default = 2
end
return parse_args(s)
end
# const name = "SYM$N"
# const upper_bound=factorial(N)-TOL^(1/5)
# S() = generating_set_of_Sym(N)
# name = "AutF$N"
# S() = generating_set_of_AutF(N)
function main()
parsed_args = parse_commandline()
if parsed_args["cpus"] nothing
if parsed_args["cpus"] > cpuinfo_physicalcores()
warn("Number of specified cores exceeds the physical core cound. Performance will suffer.")
end
Blas.set_num_threads(parsed_args["cpus"])
end
tol = parsed_args["tol"]
iterations = parsed_args["iterations"]
# solver = SCSSolver(eps=tol, max_iters=iterations, verbose=true, linearsolver=SCS.Indirect)
solver = SCSSolver(eps=tol, max_iters=iterations, linearsolver=SCS.Direct)
N = parsed_args["N"]
upper_bound = parsed_args["upper-bound"]
name = "SOutF$N"
name = name*"-$(string(upper_bound))"
logger = PropertyT.setup_logging(name)
info(logger, "Group: $name")
info(logger, "Iterations: $iterations")
info(logger, "Precision: $tol")
info(logger, "Upper bound: $upper_bound")
AutFN = AutGroup(FreeGroup(N), special=true, outer=true)
S = generators(AutFN);
S = unique([S; [inv(s) for s in S]])
Id = AutFN()
@time PropertyT.check_property_T(name, S, Id, solver, upper_bound, tol, 2)
return 0
end
main()