[[["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."],[[["\u003cp\u003eThis documentation covers the internal representation of clauses and the classes used for their propagation within the C++ solver.\u003c/p\u003e\n"],["\u003cp\u003eThe content is auto-generated and provides reference information related to the solver's clause implementation.\u003c/p\u003e\n"],["\u003cp\u003eKey classes discussed include BinaryClauseManager, BinaryImplicationGraph, LiteralWatchers, and SatClause.\u003c/p\u003e\n"],["\u003cp\u003eThe provided classes are part of the \u003ccode\u003eoptimization/reference/sat/clause\u003c/code\u003e directory.\u003c/p\u003e\n"]]],["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"],null,["# clause\n\nC++ Reference: clause\n=====================\n\n\nNote: This documentation is automatically generated.\nThis file contains the solver internal representation of the clauses and the classes used for their propagation. \n\n| Classes ------- ||\n|-------------------------------------------------------------------------------------|---|\n| [BinaryClauseManager](/optimization/reference/sat/clause/BinaryClauseManager) |\n| [BinaryImplicationGraph](/optimization/reference/sat/clause/BinaryImplicationGraph) |\n| [LiteralWatchers](/optimization/reference/sat/clause/LiteralWatchers) |\n| [SatClause](/optimization/reference/sat/clause/SatClause) |"]]
