Lrat.pb.cs File Reference

Go to the source code of this file.

Classes
class	OperationsResearch.Sat.LratReflection
	Holder for reflection information generated from ortools/sat/lrat.proto. More...
class	OperationsResearch.Sat.LratImportedClause
	A clause imported from the input problem, or from another worker. More...
class	OperationsResearch.Sat.LratInferredClause
	An LRAT inferred clause. More...
class	OperationsResearch.Sat.LratInferredClause.Types
	Container for nested types declared in the LratInferredClause message type. More...
class	OperationsResearch.Sat.LratInferredClause.Types.RatInfo
	If rat_infos is empty, the last unit_ids clause must become empty after unit propagation. If the last unit_ids clause does not become empty by unit propagation, then rat_infos must contain all the clauses which contain the negation of the first literals (called the pivot 'p') – and no other clauses. Moreover, for each r in rat_infos, all the r.unit_ids clauses must become unit and eventually empty if all the literals of the r.resolvant_id clause (minus ~p), plus those in literals, are assumed to be false (this list must be in unit propagation order; verification stops at the first empty clause). See LratChecker for more details. More...
class	OperationsResearch.Sat.LratExportedClause
	A clause to export, so that it can be imported from any worker. This is not needed for unary and binary clauses, which are always exported. More...
class	OperationsResearch.Sat.LratDeletedClauses
	A list of clauses to delete. More...
class	OperationsResearch.Sat.LratProofStep
	An LRAT UNSAT proof is a sequence of steps, starting from imported clauses and ending with the empty clause. At each step new clauses can be inferred from previous ones (with an explicit proof), or imported from another proof built by another thread. A proof step can also delete clauses which are no longer needed, or export a clause for other workers to import. Each clause is identified by a unique clause ID. More...

Namespaces
namespace	OperationsResearch
namespace	OperationsResearch.Sat