[[["Easy to understand","easyToUnderstand","thumb-up"],["Solved my problem","solvedMyProblem","thumb-up"],["Other","otherUp","thumb-up"]],[["Missing the information I need","missingTheInformationINeed","thumb-down"],["Too complicated / too many steps","tooComplicatedTooManySteps","thumb-down"],["Out of date","outOfDate","thumb-down"],["Samples / code issue","samplesCodeIssue","thumb-down"],["Other","otherDown","thumb-down"]],["Last updated 2024-08-06 UTC."],[[["This documentation covers the internal representation of clauses and the classes used for their propagation within the C++ solver."],["The content is auto-generated and provides reference information related to the solver's clause implementation."],["Key classes discussed include BinaryClauseManager, BinaryImplicationGraph, LiteralWatchers, and SatClause."],["The provided classes are part of the `optimization/reference/sat/clause` directory."]]],["The document outlines the internal structure of clauses within a C++ solver, detailing their representation and propagation mechanisms. It defines classes crucial for managing these clauses: `BinaryClauseManager` handles binary clauses, `BinaryImplicationGraph` manages relationships within binary clauses, `LiteralWatchers` tracks literal occurrences, and `SatClause` represents a general satisfiability clause. These classes are essential for the solver's internal operations related to clause processing and are used to implement constraint propagation.\n"]]
