Weighted Satisfiability of CNF Formulas

Lax496464.WH_C3_WeightedSat · concepts/Lax496464/WH_C3_WeightedSat.lean · lax-496464

definition

Loading review…

Natural Language Statement

Definition

An assignment to the variables of a propositional formula $\alpha$ has weight $k$ if it sets exactly $k$ of them to true, and $\alpha$ is $k$ -satisfiable if some assignment of weight $k$ satisfies it [FG06, Section 4.1].

$p$ -WSat( $\Gamma$ ) for a class $\Gamma$ of formulas. Instance: $\alpha \in \Gamma$ and $k \in \mathbb N$ . Parameter: $k$ . Question: is $\alpha$ $k$ -satisfiable?

The classes used are the CNF formulas with clauses of at most $d$ literals, $d$ -CNF ( $\Gamma_{1,d}$ in [FG06]), and the monotone CNF formulas, all of whose literals are positive ( $\Gamma^+_{2,1}$ ).

Concept map

6 concepts; 3 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

1	import Lax888481.ParameterizedComplexity
2	import Lax429075.CNF
3
4	/-!
5	---
6	title: Weighted Satisfiability of CNF Formulas
7	type: definition
8	---
9	An assignment to the variables of a propositional formula $\alpha$ has weight $k$ if it sets
10	exactly $k$ of them to true, and $\alpha$ is * $k$ -satisfiable* if some assignment of weight $k$
11	satisfies it [FG06, Section 4.1].
12
13	$p$ -WSat( $\Gamma$ ) for a class $\Gamma$ of formulas. Instance: $\alpha \in \Gamma$ and
14	$k \in \mathbb N$ . Parameter: $k$ . Question: is $\alpha$ $k$ -satisfiable?
15
16	The classes used are the CNF formulas with clauses of at most $d$ literals, $d$ -CNF
17	( $\Gamma_{1,d}$ in [FG06]), and the monotone CNF formulas, all of whose literals are positive
18	( $\Gamma^+_{2,1}$ ).
19
20	# Formalization Notes
21
22	A CNF formula is the archive's `Lax429075.CNF.Formula`, a list of clauses, each a list of literals
23	with a variable index and a sign. The variables of $\alpha$ are the indices occurring in it, and an
24	assignment of weight $k$ is a set of $k$ of them, the variables set to true.
25
26	The word of an instance lists the number of clauses, then each clause as its length followed by its
27	literals — $X_i$ written $2i$ and $\neg X_i$ written $2i+1$ — and finally $k$ . The class $\Gamma$
28	restricts the instances only.
29	-/
30
31	namespace Lax496464.WH_C3_WeightedSat
32
33	open Lax429075.CNF
34	open Lax888481.ParameterizedComplexity (Problem)
35
36	/-- The variables that occur in a formula. -/
37	def vars (α : Formula) : Finset ℕ := (α.flatMap fun C => C.map Literal.index).toFinset
38
39	/-- `α` is `k`-satisfiable: setting some `k` of its variables to true, and the others to false,
40	satisfies it. -/
41	def WeightSat (α : Formula) (k : ℕ) : Prop :=
42	∃ S : Finset ℕ, S ⊆ vars α ∧ S.card = k ∧ eval α (fun i => decide (i ∈ S)) = true
43
44	/-- `α ∈ d-CNF`: every clause has at most `d` literals. -/
45	def IsDCNF (d : ℕ) (α : Formula) : Prop := ∀ C ∈ α, C.length ≤ d
46
47	/-- `α` is monotone: every literal is positive. -/
48	def IsMonotone (α : Formula) : Prop := ∀ C ∈ α, ∀ l ∈ C, l.positive = true
49
50	/-- The number standing for a literal: `2i` for `X_i`, `2i + 1` for `¬X_i`. -/
51	def litCode (l : Literal) : ℕ := 2 * l.index + if l.positive then 0 else 1
52
53	/-- The word of a formula: the number of clauses, then each clause as its length and its literals. -/
54	def encode (α : Formula) : List ℕ := α.length :: α.flatMap fun C => C.length :: C.map litCode
55
56	/-- `p-WSat(Γ)`, weighted satisfiability for the class `Γ` of CNF formulas. -/
57	def pWSat (Γ : Set Formula) : Problem where
58	Domain := {x \| ∃ α ∈ Γ, ∃ k, x = encode α ++ [k]}
59	Yes x := ∃ α k, x = encode α ++ [k] ∧ WeightSat α k
60	param x := x.getLast?.getD 0
61
62	end Lax496464.WH_C3_WeightedSat
63

Formalization Notes

A CNF formula is the archive's $Lax429075.CNF.Formula$ , a list of clauses, each a list of literals with a variable index and a sign. The variables of $\alpha$ are the indices occurring in it, and an assignment of weight $k$ is a set of $k$ of them, the variables set to true.

The word of an instance lists the number of clauses, then each clause as its length followed by its literals — $X_i$ written $2i$ and $\neg X_i$ written $2i+1$ — and finally $k$ . The class $\Gamma$ restricts the instances only.

Builds on

Used by

From Mathlib

none

Discussion

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

Loading discussion…

Lax Lean Archive

Weighted Satisfiability of CNF Formulas

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments