Boolean Satisfiability

Satisfiability/README.md

@@ -0,0 +1,19 @@
+# Problem: CNF Boolean Satisfiability
+
+## Description
+Given a logical formula φ in conjunctive normal form (CNF), an AND of ORs, find an assignment to the literals in φ such that φ evaluates to true under that assignment.
+
+Problems related to boolean satisfiability:
+
+- SAT - Find a satisfying assignment.
+- Max-SAT - Find an assignment which maximizes the number of satisfied clauses.
+
+## Example
+
+Given the formula:
+
+
+φ = (a ∨ b) ∧ (¬a ∨ c ∨ d) ∧ (¬b ∨ ¬d)
+
+
+A satisfying assignment is to set a = True, b = False, c = True, and d = True. This is not the only satisfying assignment to φ

Satisfiability/gen/README.md

@@ -0,0 +1,11 @@
+# Instance Generator: CNF Boolean Satisfiability
+
+## Description
+The generator creates a random CNF Boolean Satisfiability instance based on user provided arguments.
+The generator takes two required positional arguments:
+  1. `n` the number of literals.
+  2. `c` the number of clauses to generate.
+
+The generator also takes two optional arguments:
+  1. `-u` the upper bound on the number of literals per clause (default: 4).
+  2. `-l` the lower bound on the number of literals per clause (default: 1).

Satisfiability/gen/generate.py

@@ -0,0 +1,47 @@
+# File: generate.py
+# Author: Michael Huelsman
+
+# Description: CNF
+# Use: python3 generate.py <n> <c> -l <l> -u <u> > filename.lp
+#	where:
+#          <n> is the number of literals in the formula.
+#          <c> is the number of clauses to generate.
+#          <l> is the lower limit on the number of literals per clause (default: 1).
+#          <u> is the upper limit on the number of literals per clause (default: 4).
+#	       filename.lp is the file to write the instance to
+#	The redirect (> filename.lp) can be omitted (to write to stdout)
+
+
+import argparse
+import random
+
+def main(args):
+    literals = [i+1 for i in range(args.n)]
+    clauses = set()
+    # Generate clauses
+    while len(clauses) < args.c:
+        # Select literals for the new clause.
+        lits = random.randint(args.l, args.u)
+        clause = random.sample(literals, lits)
+        # Sort clauses to detect duplicates
+        clause.sort()
+        # Randomly negate literals.
+        for idx in range(len(clause)):
+            clause[idx] *= random.choice([-1, 1])
+        # Add clause if it has not already been generated.
+        clause = tuple(clause)
+        if clause not in clauses:
+            clauses.add(clause)
+    # Write out the logic program
+    for idx, clause in enumerate(clauses):
+        for literal in clause:
+            print(f'clause({idx+1},{literal}).')
+
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser(prog='CNF Formula Generator')
+    parser.add_argument('n', type=int, help='The number of literals in the formula.')
+    parser.add_argument('c', type=int, help='The number of clauses to generate.')
+    parser.add_argument('-l', type=int, default=1, help='The lower limit on the number of literals per clause (default: 1).')
+    parser.add_argument('-u', type=int, default=4, help='The upper limit on the number of literals per clause (default: 4).')
+    main(parser.parse_args())

Satisfiability/instance.lp

@@ -0,0 +1,8 @@
+clause(1, 1).
+clause(1, 2).
+clause(2, -1).
+clause(2, 2).
+clause(3, 1).
+clause(3, -2).
+clause(4, -1).
+clause(4, -2).

Satisfiability/max-sat.lp

@@ -0,0 +1,38 @@
+% File: max-sat.lp
+% Author: Michael Huelsman
+% Created On: 25 May 2026
+% Purpose:
+%   A CNF Max-SAT solver written in ASP.
+%
+% Usage:
+%   clingo max-sat.lp instance.lp
+%
+% Instance Setup:
+%   Each instance contains the following predicates:
+%     clause(I,L)
+%       which reads that clause I contains literal L.
+%   Literals values are only integers.
+%   Negative integer values means a particular literal is negated in
+%   the clause. Thus, clause(0, -1) is read as clause 0 contains NOT x1.
+%   Clauses may have any number of literals, but are assumed to be in CNF form.
+
+% Simplification predicates
+
+literal(L) :- L = |X|, clause(_,X).
+clause(C) :- clause(C,_).
+
+% Assign true/false values to literals
+1 {true(L); false(L)} 1 :- literal(L).
+
+% Clause satisfiability
+sat_clause(C) :- clause(C,L), true(L), L > 0.
+sat_clause(C) :- clause(C,L), false(|L|), L < 0.
+
+:- true(L), false(L).
+
+% Max-SAT optimization statement.
+#maximize {1,sat_clause(C):sat_clause(C)}.
+
+#show true/1.
+#show false/1.
+#show sat_clause/1.

Satisfiability/sat.lp

@@ -0,0 +1,36 @@
+% File: sat.lp
+% Author: Michael Huelsman
+% Created On: 25 May 2026
+% Purpose:
+%   A CNF SAT solver written in ASP.
+%
+% Usage:
+%   clingo max-sat.lp instance.lp
+%
+% Instance Setup:
+%   Each instance contains the following predicates:
+%     clause(I,L)
+%       which reads that clause I contains literal L.
+%   Literals values are only integers.
+%   Negative integer values means a particular literal is negated in
+%   the clause. Thus, clause(0, -1) is read as clause 0 contains NOT x1.
+%   Clauses may have any number of literals, but are assumed to be in CNF form.
+
+% Simplification predicates
+
+literal(L) :- L = |X|, clause(_,X).
+clause(C) :- clause(C,_).
+
+% Assign true/false values to literals
+1 {true(L); false(L)} 1 :- literal(L).
+
+% Clause satisfiability
+sat_clause(C) :- clause(C,L), true(L), L > 0.
+sat_clause(C) :- clause(C,L), false(|L|), L < 0.
+
+% SAT constraints
+:- true(L), false(L).
+:- not sat_clause(C), clause(C).
+
+#show true/1.
+#show false/1.