https://gitlab.com/MIAOresearch/roundingsat/
RoundingSAT can solve any problem in the OPB format. A natural choice would be the instances from the PB16 competition. (direct link.)
Running the command
./roundingsat instance.opb --proof-log=out
will generate a file out.proof containing the proof log.
https://github.com/ciaranm/glasgow-subgraph-solver
Uses dimacs graphs as instances, a collection of subgraph instances can be found at https://perso.liris.cnrs.fr/christine.solnon/SIP.html
For finding subgraphs:
./glasgow_subgraph_solver pattern_graph target_graph --prove out --no-clique-detection
Will generate files out.opb and out.veripb
For finding cliques:
./glasgow_clique_solver graph --prove out
Will generate files out.opb and out.veripb
For finding common subgraphs:
./glasgow_common_subgraph_solver graphA graphB --prove out
Will generate files out.opb and out.veripb
https://github.com/ciaranm/glasgow-constraint-solver
https://gitlab.com/MIAOresearch/minisat_with_xorengine
Any CNF instances, e.g., from the SAT competition. For instances with Xors see the supplementary material of the parity paper.
Compile with make pbp to enable proof logging.
./bin/minisat_pbp instances.cnf
Will generate file proof.txt.
To verify CNF instances with VeriPB it is neccessary to use the
--cnf option. E.g.,
veripb --cnf instance.cnf proof.txt
https://bitbucket.org/krr/breakid/
Any CNF instances, e.g., from the SAT competition.
./BreakID -f test.cnf -no-bin -no-relaxed -logfile out.pbp
To verify CNF instances with VeriPB it is neccessary to use the
--cnf option. E.g.,
veripb --cnf instance.cnf proof.txt
https://gitlab.com/MIAOresearch/kissat_fork
Any CNF instance
./kissat instance.cnf out.pbp --no-binary