#NAE-SAT and #Set Splitting

Lax859101.CountingNaeSat · concepts/Lax859101/CountingNaeSat.lean · lax-859101

definition

Loading review…

Natural Language Statement

Definition

A not-all-equal model of a CNF instance is a set of variables such that every clause has a true literal and a false one; #NAE-SAT counts them. On a set system, a splitting color class is a set of ground elements meeting every set of the family and its complement; #Set Splitting counts them.

Concept map

12 concepts; 13 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Algebra.BigOperators.Ring.Finset
2	import Mathlib.Algebra.Order.BigOperators.Group.Finset
3	import Mathlib.Data.Fintype.BigOperators
4	import Mathlib.SetTheory.Cardinal.Finite
5	import Mathlib.Algebra.Group.Action.Defs
6	import Mathlib.Tactic.Ring
7	import Mathlib.Order.PiLex
8	import Mathlib.Data.Prod.Lex
9	import Mathlib.Data.Fintype.EquivFin
10	import Mathlib.ModelTheory.Order
11	import Mathlib.ModelTheory.Semantics
12	import Mathlib.ModelTheory.Complexity
13	import Mathlib.Tactic.FinCases
14	import Mathlib.Logic.Equiv.Fin.Basic
15	import Mathlib.Data.Fintype.Lattice
16	import Mathlib.Data.Finite.Sigma
17	import Mathlib.Order.Lattice.Nat
18	import Mathlib.Data.Set.Card
19	import Mathlib.Data.Fintype.Pigeonhole
20	import Mathlib.Dynamics.FixedPoints.Basic
21	import Mathlib.ModelTheory.Syntax
22	import Mathlib.Data.Fintype.Card
23	import Mathlib.Logic.Equiv.Prod
24	import Mathlib.Data.Set.Finite.Lemmas
25	import Lax366625.CountingSat
26	import Lax799700.NaeSat
27	import Lax799700.SetFamily
28	import Lax904597.Sat
29	import Lax366625.CountingProblems
30
31	/-!
32	---
33	title: #NAE-SAT and #Set Splitting
34	type: definition
35	---
36	A not-all-equal model of a CNF instance is a set of variables such that
37	every clause has a true literal and a false one; #NAE-SAT counts them. On a
38	set system, a splitting color class is a set of ground elements meeting
39	every set of the family and its complement; #Set Splitting counts them.
40	-/
41
42	namespace Lax859101.CountingNaeSat
43
44	open Lax366625.CountingSat Lax799700.NaeSat Lax799700.SetFamily Lax904597.Sat
45
46	open FirstOrder
47
48	open Language Structure
49
50	section Problem
51
52	variable (A : Type) [sat.Structure A]
53
54	/-- A not-all-equal model: a not-all-equal proper set of variables of the
55	formula. -/
56	def NAEModel (ν : A → Prop) : Prop :=
57	NAEProper ν ∧ ∀ x : A, ν x → SatOccurs A x
58
59	end Problem
60
61	section Split
62
63	variable (A : Type) [setSystem.Structure A]
64
65	/-- A splitting color class: a set of ground elements meeting every set of
66	the family and its complement. -/
67	def SplitColoring (S : A → Prop) : Prop :=
68	(∀ x : A, S x → SSElem x) ∧ ∀ f : A, SSFam f →
69	(∃ x : A, SSElem x ∧ SSMem x f ∧ S x) ∧ ∃ x : A, SSElem x ∧ SSMem x f ∧ ¬S x
70
71	end Split
72
73	open Lax366625.CountingProblems
74
75	/-- #NAE-SAT, as a counting problem. -/
76	noncomputable def SharpNAESAT : CountingProblem Lax904597.Sat.sat :=
77	CountingProblem.ofFun fun A _ =>
78	Nat.card {ν : A → Prop // NAEModel A ν}
79
80	/-- #Set Splitting, as a counting problem. -/
81	noncomputable def SharpSetSplitting : CountingProblem Lax799700.SetFamily.setSystem :=
82	CountingProblem.ofFun fun A _ =>
83	Nat.card {S : A → Prop // SplitColoring A S}
84
85	end Lax859101.CountingNaeSat
86

Builds on

Used by

From Mathlib

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

#NAE-SAT and #Set Splitting

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments