A stochastic Boolean satisfiability(SSAT) verification framework implemented on top of the model counting verification framework CPOG
Running the toolchain using prototype (unverified) tools requires the following:
- A C and C++ compiler
- A python3 interpreter
- Compiled CaDiCal SAT solver, Drat-trim proof checker, and SharpSSAT SSAT solver (included in tools as submodules)
- ssat_benchmarks: SSAT benchmark set
- src: Code for the CPOG generator and prototype checker
- tools: Code for a scripting program that runs the entire toolchain (put SharpSSAT, cadical, drat-trim here)
- install: Compiles evalSSAT, cpog-gen, cpog-check
- srun: Runs SharpSSAT, evalSSAT, cpog-gen, cpog-check on ssat_benchmark files
- clean: Removes intermediate files
- superclean: Removes all generated files