caletechnology/satisfier

🧩 Application Programming Interface (API) for solving Boolean satisfiability problems

A step-by-step tutorial demonstrating Satisfier API (client.cpp, satisfier.hpp, satisfier.dll, libsatisfier.a) integration with Code::Blocks C++ project, using Dynamic Link Library (DLL). For resources on origin of the word "satisfier", read Harvey M. Friedman Adventures in Logic for Undergraduates, and The Dynmamics of Decision-Making Styles (Decision Dynamics Europe).

---

🛠 Prerequisites

• Operating System: Windows with Code::Blocks + MinGW

• Files required in your project folder:

  • client.cpp
  • satisfier.hpp
  • satisfier.dll
  • libsatisfier.a

  If you are downloading Code::Blocks for the first time, then you don't need this tutorial. Just download and extract codeblocks-satisfier-nosetup.zip via https://huggingface.co/caletechnology/codeblocks-satisfier-nosetup/tree/main, then open client.cpp

---

🏗️ Integration

1. Create Console Project
   File → New → Project → Console Application (C++)

2. Add files
   Copy client.cpp, satisfier.hpp into the project directory.

3. Linker Settings

   • Project → Build options → Linker settings
   • Under Link libraries click the Add button to add libsatisfier.a file
   • When the above dialog box appear, choose No
   • To debug, link again and choose Yes in the dialog box

4. Copy .dll

   • Comment erroneous code in main function of client.cpp
   • Build your project to compile .exe executable
   • Copy satisfier.dll next to the compiled executable
   • Uncomment code in the main function of client.cpp

5. Build & Run

   • Press F9—the project dynamically loads the DLL at runtime.

---

□ Proofs

Regarding context rule, read Yannis Kassios Formal Proof. Also read A. N. Prior The Runabout Inference-Ticket, to prove that A. And (B) is not equivalent to A. Tonk (B). Nuel D. Belnap Tonk, Plonk and Plink says that both A,B are deducible from A. And (B) in synthetic mode of logic relying on context.

When using Satisfier API to do formal proof, if you have consecutive disjunctions e.g., A. Or (B). Or (C) and you supposed only literal C is true, then type C. Or (A). Or (B) instead of A. Or (B). Or (C) to minimize number of recommendations from the API.