diff --git a/Satisfiability/README.md b/Satisfiability/README.md new file mode 100644 index 0000000..9be15d9 --- /dev/null +++ b/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 φ diff --git a/Satisfiability/gen/README.md b/Satisfiability/gen/README.md new file mode 100644 index 0000000..8379405 --- /dev/null +++ b/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). diff --git a/Satisfiability/gen/generate.py b/Satisfiability/gen/generate.py new file mode 100644 index 0000000..25c7640 --- /dev/null +++ b/Satisfiability/gen/generate.py @@ -0,0 +1,47 @@ +# File: generate.py +# Author: Michael Huelsman + +# Description: CNF +# 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 (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) + + +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()) 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 new file mode 100644 index 0000000..627e055 --- /dev/null +++ b/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. diff --git a/Satisfiability/sat.lp b/Satisfiability/sat.lp new file mode 100644 index 0000000..c79f2bf --- /dev/null +++ b/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.