Skip to content
  1. CLRS-Lean
  2. Chapter 34. NP-Completeness
  3. 34.4. NP-Completeness Proofs
  4. 34.4. Standalone SAT Certificate Semantics
  5. 34.4. Reduction-Backed SAT Verifier
  6. 34.4. SAT Reduction-Verifier Input
Browse chapters
Imports
import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.SAT.ReductionVerifier.ReductionMap

Reduction-backed SAT verifier input

namespace CLRS.Chapter34

A total SAT verifier obtained by composing the concrete SAT-to-3-CNF map with the fixed reduction-backed 3-CNF verifier.

def satReductionVerifier (certificate input : List FormulaSym) : Bool := threeCNFReductionVerifier (formulaToCNFCertificate certificate) (satToThreeCNFMap input)
namespace Turing.SATVerifierabbrev RawInput := List FormulaSym × List FormulaSymdef rawEncoding (input : RawInput) : List (Option FormulaSym) := pairEncoding input.1 input.2def reducedThreeCNFInput (input : RawInput) : List CNFSym × List CNFSym := (formulaToCNFCertificate input.1, satToThreeCNFMap input.2)end Turing.SATVerifierend CLRS.Chapter34