Closed BrianLi009 closed 1 year ago
Here's how the cnf instance can be replicated if needed:
Remove the noncolorability and mindegree constraint from generate-conway.py. The part of the code calling different constraint functions should look like the following:
clause_count += squarefree(n, edge_dict, cnf_file)
print ("graph is squarefree")
clause_count += triangle(n, edge_dict, tri_dict, cnf_file)
print ("all vertices are part of a triangle")
var_count, c_count = cubic(n, count, cnf_file)
clause_count += c_count
print ("isomorphism blocking applied")
var_count, c_count = conway(n, edge_dict, tri_dict, 1, 3, cnf_file, var_count) #at least 1 vertex is in 3 triangles
clause_count += c_count
print ("conway constraint")
Generate an instance with the following command:
python3 gen_instance/generate-conway.py 7
Given this cnf file: constraints_7.txt
Solve the instance using Maplesat-ks with the following command:
./maplesat-ks/simp/maplesat_static constraints_7.txt -order=7 -exhaustive=7.exhaust
The solver will output two solutions:
The 2nd solution does not satisfy the constraint, passing the 2nd solution to CaDiCaL would result in UNSAT.