From a543b2d6aa8fe0a5b90beb444a0d4cd3a4e884d5 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Thu, 9 Nov 2023 21:50:23 -0500 Subject: [PATCH] Add bad SAT solver example --- README.md | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/README.md b/README.md index 2664756..ec65d36 100644 --- a/README.md +++ b/README.md @@ -126,6 +126,34 @@ that too: #demand guilt _ is guilty. +Answer set programming is sometimes compared to boolean satisfiability solving, and is sometimes +implemented with, general purpose satisfiablity solvers. We can also use Dusa as a pretty bad boolean +satisfibility solver, by assigning every proposition we come across the value `true` or `false`. The +[Wikipedia article describing a basic SAT-solving algorithm, DPLL](https://en.wikipedia.org/wiki/DPLL_algorithm), +uses as its example the following SAT instance: + + (a' + b + c ) * (a + c + d ) * + (a + c + d') * (a + c' + d ) * + (a + c' + d') * (b' + c' + d ) * + (a' + b + c') * (a' + b' + c ) + +We can ask Dusa to solve this problem by negating all the OR-ed together clauses and making them +`#forbid` constraints. + + a is { true, false }. + b is { true, false }. + c is { true, false }. + d is { true, false }. + + #forbid a is true, b is false, c is false. + #forbid a is false, c is false, c is false. + #forbid a is false, c is false, d is true. + #forbid a is false, c is true, d is false. + #forbid a is false, c is true, d is true. + #forbid b is true, c is true, d is false. + #forbid a is true, b is false, c is true. + #forbid a is true, b is true, c is false. + # Syntax ## Lexical tokens