Detailed Description

Access to all counters. Tracks various information about the solver progress.

Definition at line 405 of file sat_solver.h.

#include <sat_solver.h>

Public Attributes
int64_t	num_branches = 0
int64_t	num_failures = 0
int64_t	num_restarts = 0
int64_t	num_backtracks = 0
int64_t	num_minimizations = 0
	Minimization stats.
int64_t	num_literals_removed = 0
int64_t	num_learned_pb_literals = 0
	PB constraints.
int64_t	num_literals_learned = 0
	Clause learning /deletion stats.
int64_t	num_literals_forgotten = 0
int64_t	num_subsumed_clauses = 0
int64_t	minimization_num_clauses = 0
	TryToMinimizeClause() stats.
int64_t	minimization_num_decisions = 0
int64_t	minimization_num_true = 0
int64_t	minimization_num_subsumed = 0
int64_t	minimization_num_removed_literals = 0
int64_t	minimization_num_reused = 0

Member Data Documentation

◆ minimization_num_clauses

int64_t operations_research::sat::SatSolver::Counters::minimization_num_clauses = 0

TryToMinimizeClause() stats.

Definition at line 424 of file sat_solver.h.

◆ minimization_num_decisions

int64_t operations_research::sat::SatSolver::Counters::minimization_num_decisions = 0

Definition at line 425 of file sat_solver.h.

◆ minimization_num_removed_literals

int64_t operations_research::sat::SatSolver::Counters::minimization_num_removed_literals = 0

Definition at line 428 of file sat_solver.h.

◆ minimization_num_reused

int64_t operations_research::sat::SatSolver::Counters::minimization_num_reused = 0

Definition at line 429 of file sat_solver.h.

◆ minimization_num_subsumed

int64_t operations_research::sat::SatSolver::Counters::minimization_num_subsumed = 0

Definition at line 427 of file sat_solver.h.

◆ minimization_num_true

int64_t operations_research::sat::SatSolver::Counters::minimization_num_true = 0

Definition at line 426 of file sat_solver.h.

◆ num_backtracks

int64_t operations_research::sat::SatSolver::Counters::num_backtracks = 0

Definition at line 409 of file sat_solver.h.

◆ num_branches

int64_t operations_research::sat::SatSolver::Counters::num_branches = 0

Definition at line 406 of file sat_solver.h.

◆ num_failures

int64_t operations_research::sat::SatSolver::Counters::num_failures = 0

Definition at line 407 of file sat_solver.h.

◆ num_learned_pb_literals

int64_t operations_research::sat::SatSolver::Counters::num_learned_pb_literals = 0

PB constraints.

Definition at line 416 of file sat_solver.h.

◆ num_literals_forgotten

int64_t operations_research::sat::SatSolver::Counters::num_literals_forgotten = 0

Definition at line 420 of file sat_solver.h.

◆ num_literals_learned

int64_t operations_research::sat::SatSolver::Counters::num_literals_learned = 0

Clause learning /deletion stats.

Definition at line 419 of file sat_solver.h.

◆ num_literals_removed

int64_t operations_research::sat::SatSolver::Counters::num_literals_removed = 0

Definition at line 413 of file sat_solver.h.

◆ num_minimizations

int64_t operations_research::sat::SatSolver::Counters::num_minimizations = 0

Minimization stats.

Definition at line 412 of file sat_solver.h.

◆ num_restarts

int64_t operations_research::sat::SatSolver::Counters::num_restarts = 0

Definition at line 408 of file sat_solver.h.

◆ num_subsumed_clauses

int64_t operations_research::sat::SatSolver::Counters::num_subsumed_clauses = 0

Definition at line 421 of file sat_solver.h.

The documentation for this struct was generated from the following file:

ortools/sat/sat_solver.h