#include <drat_checker.h>

Public Types
enum	Status { UNKNOWN , VALID , INVALID }

Public Member Functions
	DratChecker ()

	~DratChecker ()=default

int	num_variables () const

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

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

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

Status	Check (double max_time_in_seconds)
	See Algorithm of Fig. 8 in 'Trimming while Checking Clausal Proofs'.

std::vector< std::vector< Literal > >	GetUnsatSubProblem () const

std::vector< std::vector< Literal > >	GetOptimizedProof () const

Detailed Description

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

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

Definition at line 46 of file drat_checker.h.

Member Enumeration Documentation

◆ Status

enum operations_research::sat::DratChecker::Status

Checks that the infered clauses form a DRAT proof that the problem clauses are UNSAT. For this the last added infered clause must be the empty clause and each infered clause must have either the Reverse Unit Propagation (RUP) or the Reverse Asymmetric Tautology (RAT) property with respect to the problem clauses and the previously infered clauses which are not deleted. Returns VALID if the proof is valid, INVALID if it is not, and UNKNOWN if the check timed out.

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

Enumerator
UNKNOWN
VALID
INVALID

Definition at line 82 of file drat_checker.h.

Constructor & Destructor Documentation

◆ DratChecker()

operations_research::sat::DratChecker::DratChecker ( )

Definition at line 61 of file drat_checker.cc.

◆ ~DratChecker()

operations_research::sat::DratChecker::~DratChecker ( )

default

Member Function Documentation

◆ AddInferedClause()

void operations_research::sat::DratChecker::AddInferedClause ( absl::Span< const Literal > clause )

Adds a clause which is infered from the problem clauses and the previously infered clauses (that are have not been deleted). Infered clauses must be added after the problem clauses. Clauses with the Reverse Asymmetric Tautology (RAT) property for literal l must start with this literal. The given clause must not contain a literal and its negation. Must not be called after Check().

Definition at line 83 of file drat_checker.cc.

◆ AddProblemClause()

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

Adds a clause of the problem that must be checked. The problem clauses must be added first, before any infered clause. The given clause must not contain a literal and its negation. Must not be called after Check().

Definition at line 70 of file drat_checker.cc.

◆ Check()

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

See Algorithm of Fig. 8 in 'Trimming while Checking Clausal Proofs'.

First check that the last infered clause is empty (this implies there should be at least one infered clause), and mark it as needed for the proof.

Checks the infered clauses in reversed order. The advantage of this order is that when checking a clause, one can mark all the clauses that are used to check it. In turn, only these marked clauses need to be checked (and so on recursively). By contrast, a forward iteration needs to check all the clauses.

Start watching the literals of the clauses that were deleted just after this one, and which are now no longer deleted.

'clause' must have either the Reverse Unit Propagation (RUP) property:

or the Reverse Asymmetric Tautology (RAT) property. This property is defined by the fact that all clauses which contain the negation of the RAT literal of 'clause', after resolution with 'clause', must have the RUP property. Note from 'DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs': "[in order] to access to all clauses containing the negation of the resolution literal, one could build a literal-to-clause lookup table of the original formula and update it after each lemma addition and deletion step. However, these updates can be expensive and the lookup table potentially doubles the memory usage of the tool. Since most lemmas emitted by state-of-the-art SAT solvers can be validated using the RUP check, such a lookup table has been omitted."

Check that the resolvent has the RUP property.

Definition at line 153 of file drat_checker.cc.

◆ DeleteClause()

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

Deletes a problem or infered clause. The order of the literals does not matter. In particular, it can be different from the order that was used when the clause was added. Must not be called after Check().

Temporarily add 'clause' to find if it has been previously added.

Delete 'clause' and its literals.

Definition at line 125 of file drat_checker.cc.

◆ GetOptimizedProof()

std::vector< std::vector< Literal > > operations_research::sat::DratChecker::GetOptimizedProof ( ) const

Returns a DRAT proof that GetUnsatSubProblem() is UNSAT. The result is undefined if Check() was not previously called, or did not return true.

Definition at line 226 of file drat_checker.cc.

◆ GetUnsatSubProblem()

std::vector< std::vector< Literal > > operations_research::sat::DratChecker::GetUnsatSubProblem ( ) const

Returns a subproblem of the original problem that is already UNSAT. The result is undefined if Check() was not previously called, or did not return true.

Definition at line 222 of file drat_checker.cc.

◆ num_variables()

int operations_research::sat::DratChecker::num_variables ( ) const

inline

Returns the number of Boolean variables used in the problem and infered clauses.

Definition at line 53 of file drat_checker.h.

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

ortools/sat/drat_checker.h
ortools/sat/drat_checker.cc

Public Types

Public Member Functions