#include <drat_proof_handler.h>

Public Member Functions
	DratProofHandler ()

	DratProofHandler (bool in_binary_format, File *output, bool check=false)

	~DratProofHandler ()=default

void	ApplyMapping (const util_intops::StrongVector< BooleanVariable, BooleanVariable > &mapping)

void	SetNumVariables (int num_variables)
	This need to be called when new variables are created.

void	AddOneVariable ()

void	AddProblemClause (absl::Span< const Literal > clause)

void	AddClause (absl::Span< const Literal > clause)

void	DeleteClause (absl::Span< const Literal > clause)

DratChecker::Status	Check (double max_time_in_seconds)

Detailed Description

DRAT is a SAT proof format that allows a simple program to check that the problem is really UNSAT. The description of the format and a checker are available at: ///< http://www.cs.utexas.edu/~marijn/drat-trim/

Note: DRAT proofs are often huge (can be GB), and take about as much time to check as it takes for the solver to find the proof in the first place!

This class is used to build the SAT proof, and can either save it to disk, and/or store it in memory (in which case the proof can be checked when it is complete).

Definition at line 43 of file drat_proof_handler.h.

Constructor & Destructor Documentation

◆ DratProofHandler() [1/2]

operations_research::sat::DratProofHandler::DratProofHandler ( )

Use this constructor to store the DRAT proof in memory. The proof will not be written to disk, and can be checked with Check() when it is complete.

Definition at line 34 of file drat_proof_handler.cc.

◆ DratProofHandler() [2/2]

operations_research::sat::DratProofHandler::DratProofHandler	(	bool	in_binary_format,
		File *	output,
		bool	check = false )

Use this constructor to write the DRAT proof to disk, and to optionally store it in memory as well (in which case the proof can be checked with Check() when it is complete).

Definition at line 37 of file drat_proof_handler.cc.

◆ ~DratProofHandler()

operations_research::sat::DratProofHandler::~DratProofHandler ( )

default

Member Function Documentation

◆ AddClause()

void operations_research::sat::DratProofHandler::AddClause ( absl::Span< const Literal > clause )

Writes a new clause to the DRAT output. The output clause is sorted so that newer variables always comes first. This is needed because in the DRAT format, the clause is checked for the RAT property with only its first literal. Must not be called after Check().

Definition at line 81 of file drat_proof_handler.cc.

◆ AddOneVariable()

void operations_research::sat::DratProofHandler::AddOneVariable ( )

Definition at line 71 of file drat_proof_handler.cc.

◆ AddProblemClause()

void operations_research::sat::DratProofHandler::AddProblemClause ( absl::Span< const Literal > clause )

Adds a clause of the UNSAT problem. This must be called before any call to AddClause() or DeleteClause(), in order to be able to check the DRAT proof with the Check() method when it is complete.

Definition at line 75 of file drat_proof_handler.cc.

◆ ApplyMapping()

void operations_research::sat::DratProofHandler::ApplyMapping ( const util_intops::StrongVector< BooleanVariable, BooleanVariable > & mapping )

During the presolve step, variable get deleted and the set of non-deleted variable is remaped in a dense set. This allows to keep track of that and always output the DRAT clauses in term of the original variables. Must be called before adding or deleting clauses AddClause() or DeleteClause().

Todo: (user): This is exactly the same mecanism as in the SatPostsolver class. Factor out the code.

Definition at line 46 of file drat_proof_handler.cc.

◆ Check()

DratChecker::Status operations_research::sat::DratProofHandler::Check ( double max_time_in_seconds )

Returns VALID if the DRAT proof is correct, INVALID if it is not correct, or UNKNOWN if proof checking was not enabled (by choosing the right constructor) or timed out. This requires the problem clauses to be specified with AddProblemClause(), before the proof itself.

Warning: no new clause must be added or deleted after this method has been called.

The empty clause is not explicitly added by the solver.

Definition at line 101 of file drat_proof_handler.cc.

◆ DeleteClause()

void operations_research::sat::DratProofHandler::DeleteClause ( absl::Span< const Literal > clause )

Writes a "deletion" information about a clause that has been added before to the DRAT output. Note that it is also possible to delete a clause from the problem. Must not be called after Check().

Because of a limitation a the DRAT-trim tool, it seems the order of the literals during addition and deletion should be EXACTLY the same. Because of this we get warnings for problem clauses.

Definition at line 91 of file drat_proof_handler.cc.

◆ SetNumVariables()

void operations_research::sat::DratProofHandler::SetNumVariables ( int num_variables )

This need to be called when new variables are created.

Definition at line 64 of file drat_proof_handler.cc.

The documentation for this class was generated from the following files:

ortools/sat/drat_proof_handler.h
ortools/sat/drat_proof_handler.cc

Public Member Functions