布尔可满足性（Boolean Satisfiability,SAT）问题是数理逻辑与计算机理论领域当中的基础核心问题之一,也是首个被证明的NPC问题。理论上来讲,许多问题都可以在多项式时间内转化为SAT问题进行求解,因此,通过对SAT问题的求解可以解决众多实际问题。目前,SAT问题已经被广泛应用在电子设计自动化（EDA）、人工智能、数学以及生物信息等领域,因此针对SAT问题的求解方法与框架一直是相关领域的研究热点。首先,本论文对SAT问题的软件与硬件求解方式进行了研究,针对目前软硬件协同处理求解框架中软硬件部分相互独立导致的一系列问题,创新性地引入将ARM处理器与现场可编程逻辑门阵列（FPGA）集成在同一芯片内的ZYNQ全可编程平台,在此基础上提出了基于ZYNQ平台的SAT求解框架。该求解框架结合实例型求解方式特点以及软硬件协同设计方法,将SAT问题映射为ZYNQ平台的可编程逻辑（Programmable Logic,PL）部分的组合逻辑电路,通过运行在处理器系统（Processing System,PS）的应用程序来产生SAT问题中变量所对应的全部状态值,最后通过软硬件协同处理完成对SAT问题的求解。其次,本文针对所提出的基于ZYNQ平台的SAT求解框架设计得到一个简单的SAT求解系统实例。整个SAT求解系统的设计分为硬件和软件两个部分,硬件部分首先完成SAT问题的封装,将SAT问题转化为Verilog描述的组合逻辑电路并封装为IP核,其次设计软硬件之间的数据交互方式,最后进行软硬件部分IP模块的集成。软件部分主要完成状态遍历程序以及底层SAT问题所对应IP核的驱动程序的设计。最后,搭建系统运行环境并对基于ZYNQ平台的SAT求解系统实例进行测试与验证。实验选取不同种类的SAT实例并进行多次测试,实验结果表明本文所提出的基于ZYNQ平台的SAT求解框架针对SAT问题的求解具有较高的可行性以及正确性。