Embedding of the SAGE CAS within a SAT solver.
- Glucose SAT solver (see Glucose-SAGE extension below)
- SAGE (version 6.3)
- The Ply package for lexing and parsing must be installed on top of SAGE's built-in version of python.
- sharpSAT (only for matching counts in Table 1)
- Z3 (purely for Tseitin-encoding, will eventually be removed)
- Glucose-SAGE extension (https://bitbucket.org/ezulkosk/glucose-sage). Simple extension to Glucose 3.0.
- Copy the glucose executable in core to sagesat/bin
Locations for Glucose and sharpSAT must be set in src/common/common.py.
The resolution proof certificate for the matchings case study is too large to upload, and can be distributed as needed. Checks were performed using drup-trim.
The generated cycles and matchings for Q_5 are located in results/matchings/cycle_data_in. Each pair of consecutive lines correspond to a cycle and the matching it extends.
Must be run within the SAGE environment, from the src directory.
To run either case study:
- python main.py ../test/hamilton
- python main.py ../test/antipodal
To obtain matching counts for Table 1:
- python matching_counts.py
All files related to checkers are in /checks. To run the checks, from the root directory, run "python3 hamilton_clean #dims certificate_file out_cnf_file".