Discussion on Nov. 3

[isPANN]

• Benchmark on semiprime factorization

Note: X-SAT is an efficient Circuit-Based SAT solver.

[isPANN]

• Profiling Result

Count  Overhead File                                              Line Function
 =====  ======== ====                                              ==== ========
  1337         0 @Base/array.jl                                    800 collect(itr::Base.Generator{Vector{Vector{OptimalBranchingCore.Clause{…
  1339         0 @Base/array.jl                                    848 collect_to!
  1339         0 @Base/array.jl                                    826 collect_to_with_first!
  5974         0 @Base/client.jl                                   561 _start()
  5974         0 @Base/client.jl                                   586 repl_main
  5974         0 @Base/client.jl                                   499 run_main_repl(interactive::Bool, quiet::Bool, banner::Symbol, history_…
  5974         0 @Base/client.jl                                   478 run_std_repl(REPL::Module, quiet::Bool, banner::Symbol, history_file::…
  1485      1485 @Base/essentials.jl                               920 getindex
  2259         0 @Base/generator.jl                                 48 iterate
  2149         0 none                                                ? #greedymerge##1
  5974         0 @REPL/src/REPL.jl                                 653 run_repl(repl::REPL.AbstractREPL, consumer::Any; backend_on_current_ta…
  5974         0 @REPL/src/REPL.jl                                 427 start_repl_backend(backend::REPL.REPLBackend, consumer::Any; get_modul…
  5974        18 @REPL/src/REPL.jl                                 301 __repl_entry_eval_expanded_with_loc(mod::Module, ast::Any, toplevel_fi…
  5974         0 @REPL/src/REPL.jl                                 330 eval_user_input(ast::Any, backend::REPL.REPLBackend, mod::Module)
  5974         0 @REPL/src/REPL.jl                                 452 repl_backend_loop(backend::REPL.REPLBackend, get_module::Function)
  5974         0 @REPL/src/REPL.jl                                 639 run_repl(repl::REPL.AbstractREPL, consumer::Any)
  5974         0 @REPL/src/REPL.jl                                 424 start_repl_backend
  5974         0 @REPL/src/REPL.jl                                 305 toplevel_eval_with_hooks
  5974         0 @REPL/src/REPL.jl                                 308 toplevel_eval_with_hooks(mod::Module, ast::Any, toplevel_file::Any, to…
  5974         0 @REPL/src/REPL.jl                                 312 toplevel_eval_with_hooks(mod::Module, ast::Any, toplevel_file::Any, to…
  2149         0 @OptimalBranchingCore/src/branch.jl                23 size_reduction
  2149         0 @OptimalBranchingCore/src/greedymerge.jl           35 greedymerge(cls::Vector{Vector{OptimalBranchingCore.Clause{UInt64}}}, …
  3136        70 @BooleanInference/src/algorithms/propagate.jl      69 propagate(static::TNStatic, doms::Vector{DomainMask}, changed_vars::Ve…
  1855         0 @BooleanInference/src/algorithms/propagate.jl      99 propagate_tensor!(working_doms::Vector{DomainMask}, tensor::BoolTensor…
  1401         0 @BooleanInference/src/branching/branch.jl          24 branch_and_reduce(problem::TNProblem, config::OptimalBranchingCore.Bra…
  2314         1 @BooleanInference/src/branching/branch.jl          37 branch_and_reduce(problem::TNProblem, config::OptimalBranchingCore.Bra…
  1972         4 @BooleanInference/src/branching/branch.jl          56 branch_and_reduce(problem::TNProblem, config::OptimalBranchingCore.Bra…
  5742         0 @BooleanInference/src/branching/branch.jl          72 branch_and_reduce(problem::TNProblem, config::OptimalBranchingCore.Bra…
  3556         1 @BooleanInference/src/branching/branch.jl         135 apply_branch(problem::TNProblem, clause::OptimalBranchingCore.Clause{U…
  5742         0 @BooleanInference/src/branching/branch.jl           1 branch_and_reduce
  5742         3 @BooleanInference/src/branching/branch.jl           1 kwcall(::@NamedTuple{tag::Vector{Tuple{Int64, Int64}}, show_progress::…
  2307         0 @BooleanInference/src/branching/branch.jl          90 optimal_branching_rule(tbl::OptimalBranchingCore.BranchingTable{UInt64…
  5742         0 @BooleanInference/src/interface.jl                 17 #solve#48
  5742         0 @BooleanInference/src/interface.jl                 88 solve_factoring(n::Int64, m::Int64, N::Int64; bsconfig::OptimalBranchi…
  5742         0 @BooleanInference/src/interface.jl                 15 solve
  5954         0 @BooleanInference/src/interface.jl                 68 solve_factoring(n::Int64, m::Int64, N::Int64)
Total snapshots: 13422. Utilization: 50% across all threads and tasks. Use the `groupby` kwarg to break down by thread and/or task.

[isPANN]

• Things need to be done this week
  • Example + LookAhead
  • Read J-heap: https://ieeexplore.ieee.org/abstract/document/9643505 , Integrate CDCL framwork
  • Use SAT solver to test BMF

[isPANN]

Progress:

• Nov 5: I reviewed the branching process and confirmed that the contraction branches were correctly removed during the greedy merge phase. The greedy merge operation was found to repeatedly access certain branches, so I optimized this part and added several statistical interfaces.
  The current version now achieves performance nearly equivalent to XSAT.

[isPANN]

Nov. 7

1. Region size

Instance	Region Size	Set Cover Solver	Selector	Branch Number
20 bits factoring (UNSAT)	(1, 2)	Naive Branch	Most Occurrence	(421, 842)
20 bits factoring (UNSAT)	(1, 12)	Naive Branch	Most Occurrence	(1, 1024)

2. Different Set Cover Solver and Variable Selector

Instance	Region Size	Set Cover Solver	Selector	Branch Number	Max Depth
20 bits factoring (UNSAT)	(1, 2)	Greedy Merge	Most Occurrence	(481, 480)	8
20 bits factoring (UNSAT)	(1, 2)	Greedy Merge	Min Gamma	(824, 823)	59
10 bits factoring (UNSAT)	(1, 2)	Greedy Merge	Most Occurrence	(15, 14)	3
10 bits factoring (UNSAT)	(1, 2)	Greedy Merge	Min Gamma	(15, 14)	14
10 bits factoring (UNSAT)	(1, 2)	Integer Programming	Most Occurrence	(15, 14)	3
10 bits factoring (UNSAT)	(1, 2)	Integer Programming	Min Gamma	(34, 33)	12

Note: Here the measurement is the number of unfixed variables.