$ python3 run_expt.py - to run ggSAT_sim, proof_generation and proof_checking on 250 instances of uu50-218.
$ python3 run_expt2.py - to run ggSAT_sim, proof_generation and proof_checking on 5 instances in cnf with branching conditions obtained by running original ggSAT.
usage: (from top dir) python3 ggSAT_sim.py <path_to_problem_file> <branching_depth> <output_dir> <p/s> [path_to_leaf_branching_conditions]
p - for parallel execution
s - for sequential execution
branching_depth - Maximum number of variables the Look-Ahead solver will guess upto a solvable sub-problem.
output_dir - dir to dump clausal and resolution proofs.
path_to_leaf_branching_conditions - path to json file containing the list of variables that form the leaves of the full binary tree generated by ggSAT.
e.g., $ python3 ggSAT_sim.py cnfs/random_ksat.dimacs 5 outputs/random_ksat_inst1/ p cnfs/random_ksat_leaves.json
usage: (from top dir) python3 proof_concat.py <output_dir> <path_to_problem_file>
branching_depth - Maximum number of variables the Look-Ahead solver will guess upto a solvable sub-problem. output_dir - dir containing resolution proofs generated by ggSAT.
e.g., $ python3 proof_concat.py outputs/random_ksat_inst1/ cnfs/random_ksat.dimacs
usage: (from top dir) ./checker0 <path_to_problem_file> <path_to_proof_file>
1 Developed from "pysat," https://github.com/z11i/pysat, 2018.
2 Allen van Gelder "Resolution Proof Checker," http://www.satcompetition.org/2005, 2005.