From fe30ae6e2c3e67a961ad8b8003c75594f1306db8 Mon Sep 17 00:00:00 2001 From: xLeachimx Date: Mon, 25 May 2026 11:52:31 -0400 Subject: [PATCH 1/6] base sat solvers --- satisfiability/3-sat.lp | 39 +++++++++++++++++++++++++++++++++++++++ satisfiability/max-sat.lp | 32 ++++++++++++++++++++++++++++++++ satisfiability/sat.lp | 32 ++++++++++++++++++++++++++++++++ 3 files changed, 103 insertions(+) create mode 100644 satisfiability/3-sat.lp create mode 100644 satisfiability/max-sat.lp create mode 100644 satisfiability/sat.lp diff --git a/satisfiability/3-sat.lp b/satisfiability/3-sat.lp new file mode 100644 index 0000000..ade5b1d --- /dev/null +++ b/satisfiability/3-sat.lp @@ -0,0 +1,39 @@ +% File: sat.lp +% Author: Michael Huelsman +% Created On: 25 May 2026 +% Purpose: +% A CNF 3-SAT solver written in ASP. +% +% Usage: +% clingo 3-sat.lp instance.lp +% +% Instance Setup: +% Each instance contains the following predicates: +% clause(I,L1,L2,L3) +% which reads that clause I contains literals L1, L2, and L3. +% Literals values are only integers. +% Negative integer values means a particular literal is negated in +% the clause. Thus, clause(0, 1, 2, -3) is read as clause 0 is +% x1 OR x2 OR (NOT x3). + +% Simplification predicates +literal(X) :- X = |L|, clause(_,L,_,_). +literal(X) :- X = |L|, clause(_,_,L,_). +literal(X) :- X = |L|, clause(_,_,_,L). + +clause(X) :- clause(X,_,_,_). + +% Assign true/false values to literals +1 {true(X); false(X)} 1 :- literal(X). + +% Clause satisfiability +sat_clause(X) :- clause(X,L,_,_,), true(L), L > 0. +sat_clause(X) :- clause(X,_,L,_,), true(L), L > 0. +sat_clause(X) :- clause(X,_,_,L,), true(L), L > 0. + +sat_clause(X) :- clause(X,L,_,_,), false(|L|), L < 0. +sat_clause(X) :- clause(X,_,L,_,), false(|L|), L < 0. +sat_clause(X) :- clause(X,_,_,L,), false(|L|), L < 0. + +% SAT constraints +:- not sat_clause(X), clause(X). diff --git a/satisfiability/max-sat.lp b/satisfiability/max-sat.lp new file mode 100644 index 0000000..00e4a59 --- /dev/null +++ b/satisfiability/max-sat.lp @@ -0,0 +1,32 @@ +% 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. + +% Max-SAT optimization statement. +#maximize {1,sat_clause(C):clause(C)}. diff --git a/satisfiability/sat.lp b/satisfiability/sat.lp new file mode 100644 index 0000000..3870116 --- /dev/null +++ b/satisfiability/sat.lp @@ -0,0 +1,32 @@ +% 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 +:- not sat_clause(C), clause(C). From 66ddece8bc87ecd770d57ecfc6e8a69a2abe6edc Mon Sep 17 00:00:00 2001 From: xLeachimx Date: Mon, 25 May 2026 16:36:19 -0400 Subject: [PATCH 2/6] case change of satisfiability directory --- {satisfiability => Satisfiability}/3-sat.lp | 0 Satisfiability/README.md | 14 ++++++++++++++ Satisfiability/gen/README.md | 5 +++++ Satisfiability/gen/generate.py | 18 ++++++++++++++++++ {satisfiability => Satisfiability}/max-sat.lp | 0 {satisfiability => Satisfiability}/sat.lp | 0 6 files changed, 37 insertions(+) rename {satisfiability => Satisfiability}/3-sat.lp (100%) create mode 100644 Satisfiability/README.md create mode 100644 Satisfiability/gen/README.md create mode 100644 Satisfiability/gen/generate.py rename {satisfiability => Satisfiability}/max-sat.lp (100%) rename {satisfiability => Satisfiability}/sat.lp (100%) diff --git a/satisfiability/3-sat.lp b/Satisfiability/3-sat.lp similarity index 100% rename from satisfiability/3-sat.lp rename to Satisfiability/3-sat.lp diff --git a/Satisfiability/README.md b/Satisfiability/README.md new file mode 100644 index 0000000..9243883 --- /dev/null +++ b/Satisfiability/README.md @@ -0,0 +1,14 @@ +# Problem: CNF Boolean Satisfiability + +## Description +Given a logical formula φ in conjunctive normal form (CNF), 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. +- 3-SAT - SAT which limits clause size to 3 literals OR'd together. +- Max-SAT - Find an assignment which maximizes the number of satisfied clauses. + +## Example + +Given the formulas φ = (x1 OR x2) AND (-x1 OR x3 OR x4) AND (-x2 OR -x4), a satisfying assignment is to set x1 = True, x2 = False, x3 = True, and x4 = True. This is not the only satisfying assignment to φ diff --git a/Satisfiability/gen/README.md b/Satisfiability/gen/README.md new file mode 100644 index 0000000..004d737 --- /dev/null +++ b/Satisfiability/gen/README.md @@ -0,0 +1,5 @@ +# Instance Generators: Boolean Satisfiability + +## Description + +## Algorithm diff --git a/Satisfiability/gen/generate.py b/Satisfiability/gen/generate.py new file mode 100644 index 0000000..0dec8dd --- /dev/null +++ b/Satisfiability/gen/generate.py @@ -0,0 +1,18 @@ +# File: generate.py +# Author: Michael Huelsman + +# Description: CNF +# Use: python3 generate.py -n -c -l -u < filename.lp +# where: +# is the number of literals in the formula. +# is the number of clauses to generate. +# is the lower limit on the number of literals per clause. +# is the upper limit on the number of literals per clause. +# filename.lp is the file to write the instance to +# The redirect (> filename.lp) can be omitted (to write to stdout) + + +def main(): + pass + +def diff --git a/satisfiability/max-sat.lp b/Satisfiability/max-sat.lp similarity index 100% rename from satisfiability/max-sat.lp rename to Satisfiability/max-sat.lp diff --git a/satisfiability/sat.lp b/Satisfiability/sat.lp similarity index 100% rename from satisfiability/sat.lp rename to Satisfiability/sat.lp From 387464c6051f40de7e8a505a99eb7da2e9b2fb81 Mon Sep 17 00:00:00 2001 From: xLeachimx Date: Mon, 25 May 2026 16:36:45 -0400 Subject: [PATCH 3/6] Removing 3-SAT due to redundancy. --- Satisfiability/3-sat.lp | 39 --------------------------------------- 1 file changed, 39 deletions(-) delete mode 100644 Satisfiability/3-sat.lp diff --git a/Satisfiability/3-sat.lp b/Satisfiability/3-sat.lp deleted file mode 100644 index ade5b1d..0000000 --- a/Satisfiability/3-sat.lp +++ /dev/null @@ -1,39 +0,0 @@ -% File: sat.lp -% Author: Michael Huelsman -% Created On: 25 May 2026 -% Purpose: -% A CNF 3-SAT solver written in ASP. -% -% Usage: -% clingo 3-sat.lp instance.lp -% -% Instance Setup: -% Each instance contains the following predicates: -% clause(I,L1,L2,L3) -% which reads that clause I contains literals L1, L2, and L3. -% Literals values are only integers. -% Negative integer values means a particular literal is negated in -% the clause. Thus, clause(0, 1, 2, -3) is read as clause 0 is -% x1 OR x2 OR (NOT x3). - -% Simplification predicates -literal(X) :- X = |L|, clause(_,L,_,_). -literal(X) :- X = |L|, clause(_,_,L,_). -literal(X) :- X = |L|, clause(_,_,_,L). - -clause(X) :- clause(X,_,_,_). - -% Assign true/false values to literals -1 {true(X); false(X)} 1 :- literal(X). - -% Clause satisfiability -sat_clause(X) :- clause(X,L,_,_,), true(L), L > 0. -sat_clause(X) :- clause(X,_,L,_,), true(L), L > 0. -sat_clause(X) :- clause(X,_,_,L,), true(L), L > 0. - -sat_clause(X) :- clause(X,L,_,_,), false(|L|), L < 0. -sat_clause(X) :- clause(X,_,L,_,), false(|L|), L < 0. -sat_clause(X) :- clause(X,_,_,L,), false(|L|), L < 0. - -% SAT constraints -:- not sat_clause(X), clause(X). From fde5b521e16753f4105d53e3e62aad868fd0728c Mon Sep 17 00:00:00 2001 From: xLeachimx Date: Mon, 25 May 2026 17:03:58 -0400 Subject: [PATCH 4/6] generator an basic unsat instance --- Satisfiability/gen/generate.py | 39 ++++++++++++++++++++++++++++------ Satisfiability/instance.lp | 8 +++++++ Satisfiability/max-sat.lp | 8 ++++++- Satisfiability/sat.lp | 4 ++++ 4 files changed, 52 insertions(+), 7 deletions(-) create mode 100644 Satisfiability/instance.lp diff --git a/Satisfiability/gen/generate.py b/Satisfiability/gen/generate.py index 0dec8dd..85f32b7 100644 --- a/Satisfiability/gen/generate.py +++ b/Satisfiability/gen/generate.py @@ -2,17 +2,44 @@ # Author: Michael Huelsman # Description: CNF -# Use: python3 generate.py -n -c -l -u < filename.lp +# Use: python3 generate.py -l -u > filename.lp # where: # is the number of literals in the formula. # is the number of clauses to generate. -# is the lower limit on the number of literals per clause. -# is the upper limit on the number of literals per clause. +# is the lower limit on the number of literals per clause (default: 1). +# 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) -def main(): - pass +import argparse +import random -def +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) + # 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()) diff --git a/Satisfiability/instance.lp b/Satisfiability/instance.lp new file mode 100644 index 0000000..c1bd0b5 --- /dev/null +++ b/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). diff --git a/Satisfiability/max-sat.lp b/Satisfiability/max-sat.lp index 00e4a59..627e055 100644 --- a/Satisfiability/max-sat.lp +++ b/Satisfiability/max-sat.lp @@ -28,5 +28,11 @@ clause(C) :- clause(C,_). 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):clause(C)}. +#maximize {1,sat_clause(C):sat_clause(C)}. + +#show true/1. +#show false/1. +#show sat_clause/1. diff --git a/Satisfiability/sat.lp b/Satisfiability/sat.lp index 3870116..c79f2bf 100644 --- a/Satisfiability/sat.lp +++ b/Satisfiability/sat.lp @@ -29,4 +29,8 @@ 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. From eafda12beda9a123409fdd06ba1fd95a53c47996 Mon Sep 17 00:00:00 2001 From: xLeachimx Date: Mon, 25 May 2026 17:11:25 -0400 Subject: [PATCH 5/6] Readme for the generator --- Satisfiability/gen/README.md | 10 ++++++++-- Satisfiability/gen/generate.py | 2 ++ 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/Satisfiability/gen/README.md b/Satisfiability/gen/README.md index 004d737..e2a5636 100644 --- a/Satisfiability/gen/README.md +++ b/Satisfiability/gen/README.md @@ -1,5 +1,11 @@ -# Instance Generators: Boolean Satisfiability +# Instance Generators: 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. -## Algorithm +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). diff --git a/Satisfiability/gen/generate.py b/Satisfiability/gen/generate.py index 85f32b7..25c7640 100644 --- a/Satisfiability/gen/generate.py +++ b/Satisfiability/gen/generate.py @@ -23,6 +23,8 @@ def main(args): # 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]) From 68b337e5150d6b694898a68c53333d2b2c19bb2d Mon Sep 17 00:00:00 2001 From: xLeachimx Date: Tue, 26 May 2026 10:19:54 -0400 Subject: [PATCH 6/6] Small readme changes. --- Satisfiability/README.md | 11 ++++++++--- Satisfiability/gen/README.md | 6 +++--- 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/Satisfiability/README.md b/Satisfiability/README.md index 9243883..9be15d9 100644 --- a/Satisfiability/README.md +++ b/Satisfiability/README.md @@ -1,14 +1,19 @@ # Problem: CNF Boolean Satisfiability ## Description -Given a logical formula φ in conjunctive normal form (CNF), AND of ORs, find an assignment to the literals in φ such that φ evaluates to true under that assignment. +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. -- 3-SAT - SAT which limits clause size to 3 literals OR'd together. - Max-SAT - Find an assignment which maximizes the number of satisfied clauses. ## Example -Given the formulas φ = (x1 OR x2) AND (-x1 OR x3 OR x4) AND (-x2 OR -x4), a satisfying assignment is to set x1 = True, x2 = False, x3 = True, and x4 = True. This is not the only satisfying assignment to φ +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 φ diff --git a/Satisfiability/gen/README.md b/Satisfiability/gen/README.md index e2a5636..8379405 100644 --- a/Satisfiability/gen/README.md +++ b/Satisfiability/gen/README.md @@ -1,4 +1,4 @@ -# Instance Generators: CNF Boolean Satisfiability +# Instance Generator: CNF Boolean Satisfiability ## Description The generator creates a random CNF Boolean Satisfiability instance based on user provided arguments. @@ -7,5 +7,5 @@ The generator takes two required positional arguments: 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). + 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).