消解算法是一種用於解決邏輯推理問題的算法，其核心思想可以概括為以下幾點：
集合與數組的定義：
s0、s1、s2：這三個集合分別用於存儲不同階段的簡單析取式。每次循環後，新出現的簡單析取式加入到s2中，然後將s2賦值給s1，上一次的s1賦值給s0。
c數組：用於記錄每次消解後的情況，判斷是否已出現的新集合。
消解過程：
在每次循環中，對s1數組內部進行消解，確保與上一次s1集合中的元素進行判斷。
如果在消解過程中出現完全消解，即得到結果為0，則直接得出結論。
如果在後續循環中s2中再無新元素加入，則表明找到了可滿足式。
字母表的離散化：
利用字母表進行離散化，給每個變元分配一個值（如0表示未出現，1表示真值為正，2表示真值為負）。
s數組用於記錄每組簡單析取式變元的情況，並將變元轉換為字母表進行表示和判斷。
主函式中的循環：
第一個循環表示至少經歷第一次循環之後的情況，確保與上一次s1集合中的元素進行判斷。
第二個循環表示第一次的情況，即在s1數組內部進行消解。
注意區分兩種情況下的循環，以及在第一個循環中可能存在的一些不必要的判斷。
通過上述步驟，消解算法能夠在邏輯推理問題中找到滿足特定條件的解或者證明不存在解。這種算法廣泛套用於人工智慧、邏輯編程等領域。