Search code examples
mathematical-optimizationscip

How to generate cutting planes for a SAT problem?

I am working on idea which requires me to generate cutting planes for SAT problems. I am using a problem from https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html, qg5-10.cnf from SAT-encoded Quasigroup (or Latin square) instances.

I am using the latest version of SCIP, SCIP8.0.0. I was wondering if there is any way to generate cutting planes for SAT problems and print out the cutting planes generated. I only need to do this for the first iteration after presolving.

I have tried the following:

  1. set separating gomory freq 65534, set separating (other cutting plane methods) freq -1

However this does not tell me if gomory cuts are being generated when I use the optimize command.

  1. Printing out the cuts by adding SCIPprintRow(scip, cut, NULL) in lines 270 and 309 of sepa_gomory.c.

However nothing is printed out, leading me to think that cutting planes are not used at all for SCIP's default branching rule.

Some advice on how to go about doing this would help me test my hypothesis of cutting planes. Thank you!

Solution

  • Cutting plane generation/separation is not bound to the branching rule. You just need to run display statistics to see whether and which cuts have been generated and separated.