#include <drat_writer.h>

Public Member Functions
	DratWriter (bool in_binary_format, File *output)

	~DratWriter ()

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

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

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!

Definition at line 36 of file drat_writer.h.

Constructor & Destructor Documentation

◆ DratWriter()

operations_research::sat::DratWriter::DratWriter	(	bool	in_binary_format,
		File *	output )

inline

Definition at line 38 of file drat_writer.h.

◆ ~DratWriter()

operations_research::sat::DratWriter::~DratWriter ( )

Definition at line 30 of file drat_writer.cc.

Member Function Documentation

◆ AddClause()

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

Writes a new clause to the DRAT output. Note that the RAT property is only checked on the first literal.

Definition at line 39 of file drat_writer.cc.

◆ DeleteClause()

void operations_research::sat::DratWriter::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.

Definition at line 43 of file drat_writer.cc.

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

ortools/sat/drat_writer.h
ortools/sat/drat_writer.cc