ortools.sat.lrat_pb2
@generated by mypy-protobuf. Do not edit manually! isort:skip_file Proto used to store LRAT proofs (https://arxiv.org/abs/1612.02353) with some extensions to support multi-threading (with one output file per file). This proto is only used internally to store partial proofs on disk before merging them. It can be changed without backward compatibility, and should not be used directly by users.
LINT: LEGACY_NAMES
1# -*- coding: utf-8 -*- 2# Generated by the protocol buffer compiler. DO NOT EDIT! 3# NO CHECKED-IN PROTOBUF GENCODE 4# source: ortools/sat/lrat.proto 5# Protobuf Python Version: 6.33.1 6"""Generated protocol buffer code.""" 7from google.protobuf import descriptor as _descriptor 8from google.protobuf import descriptor_pool as _descriptor_pool 9from google.protobuf import runtime_version as _runtime_version 10from google.protobuf import symbol_database as _symbol_database 11from google.protobuf.internal import builder as _builder 12_runtime_version.ValidateProtobufRuntimeVersion( 13 _runtime_version.Domain.PUBLIC, 14 6, 15 33, 16 1, 17 '', 18 'ortools/sat/lrat.proto' 19) 20# @@protoc_insertion_point(imports) 21 22_sym_db = _symbol_database.Default() 23 24 25 26 27DESCRIPTOR = _descriptor_pool.Default().AddSerializedFile(b'\n\x16ortools/sat/lrat.proto\x12\x17operations_research.sat\"=\n\x12LratImportedClause\x12\x11\n\tclause_id\x18\x01 \x01(\x03\x12\x14\n\x08literals\x18\x02 \x03(\x05\x42\x02\x10\x01\"\xe4\x01\n\x12LratInferredClause\x12\x11\n\tclause_id\x18\x01 \x01(\x03\x12\x14\n\x08literals\x18\x02 \x03(\x05\x42\x02\x10\x01\x12\x14\n\x08unit_ids\x18\x03 \x03(\x03\x42\x02\x10\x01\x12\x46\n\trat_infos\x18\x04 \x03(\x0b\x32\x33.operations_research.sat.LratInferredClause.RatInfo\x12\x10\n\x08\x65xported\x18\x05 \x01(\x08\x1a\x35\n\x07RatInfo\x12\x14\n\x0cresolvant_id\x18\x01 \x01(\x03\x12\x14\n\x08unit_ids\x18\x02 \x03(\x03\x42\x02\x10\x01\"=\n\x12LratExportedClause\x12\x11\n\tclause_id\x18\x01 \x01(\x03\x12\x14\n\x08literals\x18\x02 \x03(\x05\x42\x02\x10\x01\",\n\x12LratDeletedClauses\x12\x16\n\nclause_ids\x18\x01 \x03(\x03\x42\x02\x10\x01\"\xb7\x02\n\rLratProofStep\x12\x46\n\x0fimported_clause\x18\x01 \x01(\x0b\x32+.operations_research.sat.LratImportedClauseH\x00\x12\x46\n\x0finferred_clause\x18\x02 \x01(\x0b\x32+.operations_research.sat.LratInferredClauseH\x00\x12\x46\n\x0f\x65xported_clause\x18\x03 \x01(\x0b\x32+.operations_research.sat.LratExportedClauseH\x00\x12\x46\n\x0f\x64\x65leted_clauses\x18\x04 \x01(\x0b\x32+.operations_research.sat.LratDeletedClausesH\x00\x42\x06\n\x04step') 28 29_globals = globals() 30_builder.BuildMessageAndEnumDescriptors(DESCRIPTOR, _globals) 31_builder.BuildTopDescriptorsAndMessages(DESCRIPTOR, 'ortools.sat.lrat_pb2', _globals) 32if not _descriptor._USE_C_DESCRIPTORS: 33 DESCRIPTOR._loaded_options = None 34 _globals['_LRATIMPORTEDCLAUSE'].fields_by_name['literals']._loaded_options = None 35 _globals['_LRATIMPORTEDCLAUSE'].fields_by_name['literals']._serialized_options = b'\020\001' 36 _globals['_LRATINFERREDCLAUSE_RATINFO'].fields_by_name['unit_ids']._loaded_options = None 37 _globals['_LRATINFERREDCLAUSE_RATINFO'].fields_by_name['unit_ids']._serialized_options = b'\020\001' 38 _globals['_LRATINFERREDCLAUSE'].fields_by_name['literals']._loaded_options = None 39 _globals['_LRATINFERREDCLAUSE'].fields_by_name['literals']._serialized_options = b'\020\001' 40 _globals['_LRATINFERREDCLAUSE'].fields_by_name['unit_ids']._loaded_options = None 41 _globals['_LRATINFERREDCLAUSE'].fields_by_name['unit_ids']._serialized_options = b'\020\001' 42 _globals['_LRATEXPORTEDCLAUSE'].fields_by_name['literals']._loaded_options = None 43 _globals['_LRATEXPORTEDCLAUSE'].fields_by_name['literals']._serialized_options = b'\020\001' 44 _globals['_LRATDELETEDCLAUSES'].fields_by_name['clause_ids']._loaded_options = None 45 _globals['_LRATDELETEDCLAUSES'].fields_by_name['clause_ids']._serialized_options = b'\020\001' 46 _globals['_LRATIMPORTEDCLAUSE']._serialized_start=51 47 _globals['_LRATIMPORTEDCLAUSE']._serialized_end=112 48 _globals['_LRATINFERREDCLAUSE']._serialized_start=115 49 _globals['_LRATINFERREDCLAUSE']._serialized_end=343 50 _globals['_LRATINFERREDCLAUSE_RATINFO']._serialized_start=290 51 _globals['_LRATINFERREDCLAUSE_RATINFO']._serialized_end=343 52 _globals['_LRATEXPORTEDCLAUSE']._serialized_start=345 53 _globals['_LRATEXPORTEDCLAUSE']._serialized_end=406 54 _globals['_LRATDELETEDCLAUSES']._serialized_start=408 55 _globals['_LRATDELETEDCLAUSES']._serialized_end=452 56 _globals['_LRATPROOFSTEP']._serialized_start=455 57 _globals['_LRATPROOFSTEP']._serialized_end=766 58# @@protoc_insertion_point(module_scope)
A clause imported from the input problem, or from another worker.
An LRAT inferred clause.
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.
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.
A list of clauses to delete.
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.