Documentation

CslibFrontier.Computability.Complexity.Problems.SAT.ExactOne.GeometryProfilesData

Composed positive exact-one geometry profiles #

The fifteen profiles describe zero through three source literal positions with every polarity pattern. The coordinates compose the parsimonious disjunction, positive complement and forced false gadgets. Every table matches the actual positive clause compiler, including its clause order, variable names and auxiliary occurrences. Source terminals have one internal incidence; the global drawing compiler removes their placeholder positions and joins their accesses to the inherited source incidence routes.

Main definitions #

References #

The logical gadgets are from [HuntMaratheRadhakrishnanStearns1998, Theorem 3.8]. The coordinates and finite profiles are original.

source
@[reducible, inline]
abbrev Cslib.Complexity.SAT.ExactOne.ClauseProfile :
Type

Fifteen signed source clauses: every sign pattern on zero through three distinct slots.

Instances For
    source
    def Cslib.Complexity.SAT.ExactOne.profileSource (p : ClauseProfile) :
    Logic.PL.Clause ℕ

    The signed source clause of a fixed profile, with variables named by their positions.

    Instances For
      source
      def Cslib.Complexity.SAT.ExactOne.profileFormula (p : ClauseProfile) :
      Logic.PL.CNF (Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ)

      The actual composed logical compiler on one source profile.

      Instances For
        source
        def Cslib.Complexity.SAT.ExactOne.profileVariables (p : ClauseProfile) :
        List (Logic.PL.CNF.PositiveExactOneCompile.Variable ℕ)

        The distinct logical variables, in the same order as the profile's variable positions.

        Instances For
          source
          def Cslib.Complexity.SAT.ExactOne.profileGeometry0 :
          LocalGeometry

          Fixed profile 0: source polarities [].

          Instances For
            source
            def Cslib.Complexity.SAT.ExactOne.profileGeometry1 :
            LocalGeometry

            Fixed profile 1: source polarities [false].

            Instances For
              source
              def Cslib.Complexity.SAT.ExactOne.profileGeometry2 :
              LocalGeometry

              Fixed profile 2: source polarities [true].

              Instances For
                source
                def Cslib.Complexity.SAT.ExactOne.profileGeometry3 :
                LocalGeometry

                Fixed profile 3: source polarities [false, false].

                Instances For
                  source
                  def Cslib.Complexity.SAT.ExactOne.profileGeometry4 :
                  LocalGeometry

                  Fixed profile 4: source polarities [false, true].

                  Instances For
                    source
                    def Cslib.Complexity.SAT.ExactOne.profileGeometry5 :
                    LocalGeometry

                    Fixed profile 5: source polarities [true, false].

                    Instances For
                      source
                      def Cslib.Complexity.SAT.ExactOne.profileGeometry6 :
                      LocalGeometry

                      Fixed profile 6: source polarities [true, true].

                      Instances For
                        source
                        def Cslib.Complexity.SAT.ExactOne.profileGeometry7 :
                        LocalGeometry

                        Fixed profile 7: source polarities [false, false, false].

                        Instances For
                          source
                          def Cslib.Complexity.SAT.ExactOne.profileGeometry8 :
                          LocalGeometry

                          Fixed profile 8: source polarities [false, false, true].

                          Instances For
                            source
                            def Cslib.Complexity.SAT.ExactOne.profileGeometry9 :
                            LocalGeometry

                            Fixed profile 9: source polarities [false, true, false].

                            Instances For
                              source
                              def Cslib.Complexity.SAT.ExactOne.profileGeometry10 :
                              LocalGeometry

                              Fixed profile 10: source polarities [false, true, true].

                              Instances For
                                source
                                def Cslib.Complexity.SAT.ExactOne.profileGeometry11 :
                                LocalGeometry

                                Fixed profile 11: source polarities [true, false, false].

                                Instances For
                                  source
                                  def Cslib.Complexity.SAT.ExactOne.profileGeometry12 :
                                  LocalGeometry

                                  Fixed profile 12: source polarities [true, false, true].

                                  Instances For
                                    source
                                    def Cslib.Complexity.SAT.ExactOne.profileGeometry13 :
                                    LocalGeometry

                                    Fixed profile 13: source polarities [true, true, false].

                                    Instances For
                                      source
                                      def Cslib.Complexity.SAT.ExactOne.profileGeometry14 :
                                      LocalGeometry

                                      Fixed profile 14: source polarities [true, true, true].

                                      Instances For
                                        source
                                        def Cslib.Complexity.SAT.ExactOne.profileGeometry (p : ClauseProfile) :
                                        LocalGeometry

                                        Select the fixed geometric data for the complete source polarity profile.

                                        Instances For