OperationsResearch.Sat Namespace Reference

Classes
class	LratReflection
	Holder for reflection information generated from ortools/sat/lrat.proto. More...
class	LratImportedClause
	A clause imported from the input problem, or from another worker. More...
class	LratInferredClause
	An LRAT inferred clause. More...
class	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	LratDeletedClauses
	A list of clauses to delete. More...
class	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...