This is the github repo for Tool MonoProof. MonoProof supports the proof of unsatisfiability for finite domain monotonic theories, including:
- Graph Reachability
- Bit-vector summation and comparison
- Maximum Flow
- Graph cyclicity (incomplete)
- PB constraints (incomplete)
git clone https://github.com/NickF0211/monosat
cd {monosat_dir}
git checkout proof_of_unsat
Please follow MonoSAT's installation instruction to build MonoSAT
add monosat executable location to monosat_path
in mono_proof.py
gcc -o drat-trim drat-trim.c
gcc -o drat-trim-orig drat-trim-orig.c
- pysat: https://pysathq.github.io/installation/
- pyz3:
pip3 install z3-solver
(testing only) - numpy:
pip3 install numpy
(benchmarking only)
python3 run_mono_proof.py {input.gnf}
--no-backward-check # Skip theory lemma trimming
--lemma-bitblast # Use lemma specific bit-blasting for proof checking instead of Horn approixmation
--no-witness-reduction # eager theory axiomatization (for graph reachability only)
--solver-opt = {options} # options for launch MonoSAT
-
There are two sets of gnfs:
unzip key_flow.zip #Network Reachability UNSAT Benchmark unzip BGA_Escape_benchmark.zip # BGA Escape Routing UNSAT Benchmark
-
Launch benchmark:
python3 maxflow_experiment.py python3 reach_exp.py key_flow_simp key_flow.csv
The BGA Escape routing results will be saved in
maxflow.csv
and the network reachability results will be saved inkey_flow.csv
. -
Comparing with Bit-Blasting
-
download and build kissat:
wget https://github.com/arminbiere/kissat/archive/refs/tags/rel-3.1.1.zip unzip rel-3.1.1.zip cd kissat-rel-3.1.1 ./configure && make test
update
solver_path
inbit_blast.py
to the built kissat executable- Launch
The BGA Escape routing results will be saved in
python3 maxflow_exp_bitblast.py BGA_Escape_benchmark maxflow_bb.csv #pure bit-blast for BGA python3 maxflow_experiment_lsb.py #lemma specific bit-blasting for BGA python3 reach_exp_bitblast.py key_flow_simp key_flow_bb.csv #pure bit-blast for Network python3 reach_exp_lsb.py key_flow_simp key_flow_lsb.csv #lemma specific bit-blasting for Network
maxflow_bb.csv
(pure bit-blasting) andmaxflow_lsb.csv
(lemma-specific bit-blasting) The network reachability results will be saved inkey_flow_bb.csv
andkey_flow_lsb.csv
-