Brute force usage is application-determined

README.md

@@ -1,6 +1,8 @@
-# CAPABLANCA-SAT Solver
+# SAT Solver
 
-![Jose Raul Capablanca (Third World Chess Champion from 1921 to 1927)](docs/capablanca.jpg)
+![Honoring the Memory of Jose Raul Capablanca (Third World Chess Champion from 1921 to 1927)](docs/capablanca.jpg)
+
+This work builds upon [SAT in Polynomial Time: A Proof of P = NP](https://www.researchgate.net/publication/387727103_SAT_in_Logarithmic_Space_A_Proof_of_P_NP).
 
 # Boolean Satisfiability (SAT) Problem
 
@@ -197,7 +199,8 @@ By using these command-line options, you can customize the behavior of the `jaqu
 ## Complexity
 
 ```diff
-- The current implementation of the SAT solver likely uses a brute-force approach, which can be computationally expensive for larger and more complex problems.
++ The current implementation of the SAT solver achieves significant performance gains by avoiding a brute-force approach.
++ This allows it to tackle problems that would otherwise be computationally prohibitive.
 ```
 
 ## License

capablanca/__init__.py

@@ -1,4 +1,4 @@
-# CAPABLANCA package
+# capablanca package: https://pypi.org/project/capablanca
 # Author: Frank Vega ([email protected])
 
-__all__ = ["utils", "reduction", "parser", "applogger", "z3solver", "satpy"]
+__all__ = ["utils", "reduction", "parser", "applogger", "z3solver", "app"]

capablanca/satpy.py → capablanca/app.py

@@ -1,7 +1,7 @@
 #                          SAT Solver
 #                          CAPABLANCA
 #                          Frank Vega
-#                      December 30th, 2024
+#                      December 27th, 2024
 
 import argparse
 import time
@@ -23,29 +23,29 @@ def output(msg, use_logs):
     else:
         print(msg)
 
-def main():
-    global logger
-
-    # Define the parameters
-    helper = argparse.ArgumentParser(prog="jaque", description='Solve the Boolean Satisfiability (SAT) problem using a DIMACS file as input.')
-    helper.add_argument('-i', '--inputFile', type=str, help='Input file path', required=True)
-    helper.add_argument('-v', '--verbose', action='store_true', help='Enable verbose output')
-    helper.add_argument('-t', '--timer', action='store_true', help='Enable timer output')
-    helper.add_argument('-l', '--log', action='store_true', help='Enable file logging')
-    helper.add_argument('-u', '--unzip', action='store_true', help='Unzip file input')
+def sat_solver(inputFile, verbose=False, timed=False, log=False, unzip=False, brute_force=False):
+    """Solves a CNF formula.
+
+    Args:
+        inputFile: Input file path.
+        verbose: Enable verbose output.
+        timed: Enable timer output.
+        log: Enable file logging.
+        unzip: Unzip file input.
+        brute_force: True (Exponential Solution), False (Feasible Solution)
+    """
 
-    # Initialize the parameters
-    args = helper.parse_args()
-    logger = applogger.Logger(applogger.FileLogger() if (args.log) else applogger.ConsoleLogger(args.verbose))
-    timed = args.timer
+    global logger
+
+    logger = applogger.Logger(applogger.FileLogger() if (log) else applogger.ConsoleLogger(verbose))
     started = 0.0
 
     # Read and parse a dimacs file
     println("Pre-processing started")
     if timed:
         started = time.time()
 
-    formula, max_variable = parser.read(args.inputFile, not args.unzip)
+    formula, max_variable = parser.read(inputFile, not unzip)
 
     if timed:
         started = (time.time() - started) * 1000.0
@@ -58,7 +58,7 @@ def main():
     if timed:
         started = time.time()
 
-    new_clauses = reduction.reduce_sat(formula, max_variable, True)
+    new_clauses = reduction.reduce_cnf_to_3sat(formula, max_variable) if (brute_force) else reduction.reduce_cnf_to_xor_sat(formula, max_variable)
 
     if timed:
         started = (time.time() - started) * 1000.0
@@ -71,7 +71,7 @@ def main():
     if timed:
         started = time.time()
 
-    solver = z3solver.build(new_clauses)
+    solver = z3solver.build_brute_force(new_clauses) if (brute_force) else z3solver.build(new_clauses)
 
     if timed:
         started = (time.time() - started) * 1000.0
@@ -84,7 +84,7 @@ def main():
     if timed:
         started = time.time()
 
-    satisfiability, answer = z3solver.solve(solver, formula, max_variable)
+    satisfiability, answer = z3solver.solve_brute_force(solver, formula, max_variable) if (brute_force) else z3solver.solve(solver, formula, max_variable)
 
     if timed:
         started = (time.time() - started) * 1000.0
@@ -94,7 +94,27 @@ def main():
 
     # Output the solution
     answer = "s UNKNOWN" if (satisfiability is None) else ("s SATISFIABLE" + '\n' + "v " + ' '.join(map(str, answer)) + " 0" if (satisfiability) else "s UNSATISFIABLE")
-    output(answer, args.verbose or args.log)    
+    output(answer, verbose or log)    
 
+def main():
+
+
+    # Define the parameters
+    helper = argparse.ArgumentParser(prog="jaque", description='Solve the Boolean Satisfiability (SAT) problem using a DIMACS file as input.')
+    helper.add_argument('-i', '--inputFile', type=str, help='Input file path', required=True)
+    helper.add_argument('-v', '--verbose', action='store_true', help='Enable verbose output')
+    helper.add_argument('-t', '--timer', action='store_true', help='Enable timer output')
+    helper.add_argument('-l', '--log', action='store_true', help='Enable file logging')
+    helper.add_argument('-u', '--unzip', action='store_true', help='Unzip file input')
+
+    # Initialize the parameters
+    args = helper.parse_args()
+    sat_solver(args.inputFile, 
+               verbose=args.verbose, 
+               timed=args.timer, 
+               log=args.log,
+               unzip=args.unzip,
+               brute_force=True)
+
 if __name__ == "__main__":
     main()

capablanca/reduction.py

@@ -1,153 +1,117 @@
-from . import utils
-
 def reduce_sat_to_3sat(clauses, max_variable):
-    """
-    Converts a formula in SAT format to a 3CNF formula.
+    """Converts a formula in SAT format to a 3CNF formula.
 
     Args:
         clauses: A list of clauses, where each clause is a list of literals.
         max_variable: The maximum variable in the input formula.
 
     Returns:
-        A tuple (new_clauses, new_max_variable), where:
-            - new_clauses: A list of 3CNF clauses.
+        A tuple (three_sat_clauses, new_max_variable), where:
+            - three_sat_clauses: A list of 3CNF clauses.
             - new_max_variable: The maximum variable in the new 3CNF formula.
     """
-  
-    new_clauses = []
+
+    three_sat_clauses = []
     next_variable = max_variable + 1
-    A, B = next_variable, next_variable + 1 # Create Global Variables
+    A, B = next_variable, next_variable + 1 # Global Variables
     next_variable += 2
-
-    for literals in clauses:
-        clause = list(set(literals)) # Ensure clauses with distinct literals
-        if len(clause) == 1: # Unit clause
-            literal = clause[0]
-            new_clauses.extend([[literal, A, B], 
-                          [literal, -A, B], 
-                          [literal, A, -B], 
-                          [literal, -A, -B]])
-        elif len(clause) == 2: # 2CNF clause
-            new_clauses.extend([clause + [A], 
-                          clause + [-A], 
-                          clause + [B], 
-                          clause + [-B]])
-        elif len(clause) > 3: # kCNF clause with k > 3
-            while len(clause) > 3:
+
+    for clause in clauses:
+        # Remove duplicate literals within a clause for efficiency and correctness.
+        unique_clause = list(set(clause))
+
+        clause_len = len(unique_clause)
+
+        if clause_len == 1:  # Unit clause
+            three_sat_clauses.extend([
+                [unique_clause[0], A, B],
+                [unique_clause[0], -A, B],
+                [unique_clause[0], A, -B],
+                [unique_clause[0], -A, -B]
+            ])
+        elif clause_len == 2:  # 2CNF clause
+            three_sat_clauses.extend([
+                unique_clause + [A],
+                unique_clause + [-A],
+                unique_clause + [B],
+                unique_clause + [-B]
+            ])
+        elif clause_len > 3:  # kCNF clause with k > 3
+            current_clause = unique_clause
+            while len(current_clause) > 3:
                 D = next_variable
-                new_clauses.append(clause[:2] + [D])
-                clause = [-D] + clause[2:]
+                three_sat_clauses.append(current_clause[:2] + [D])
+                current_clause = [-D] + current_clause[2:]
                 next_variable += 1
-            new_clauses.append(clause)
-        else: # 3CNF clause
-            new_clauses.append(clause)
+            three_sat_clauses.append(current_clause)
+        else:  # 3CNF clause
+            three_sat_clauses.append(unique_clause)
 
-    return new_clauses, next_variable - 1    
+    return three_sat_clauses, next_variable - 1
 
-def reduce_3sat_to_1_in_3_3msat(clauses, max_variable):
-    """
-    Converts a 3SAT formula to a monotone 1-IN-3-3SAT instance.
+def reduce_3sat_to_xor_sat(clauses, max_variable):
+    """Converts a formula in 3SAT format to a XOR-SAT formula.
 
     Args:
-        clauses: A list of 3CNF clauses.
+        clauses: A list of clauses, where each clause is a list of three distinct literals.
         max_variable: The maximum variable in the input formula.
 
-    Returns: A tuple (new_clauses, new_max_variable), where:
-            - new_clauses: A list of monotone 1-IN-3-3SAT clauses.
-            - new_max_variable: The maximum variable in the new 3CNF formula.
+    Returns:
+        A list of XOR CNF clauses.
     """
 
-    new_clauses = []
-    next_variable = 2 * max_variable + 2
-
-    variables = utils.convert_to_absolute_value_set(clauses) # Set of all variables
-
-    for variable in variables: # Keep consistency between x and ¬x
-        positive_literal = utils.double(variable) # Map variable to 2 * variable
-        negative_literal = utils.double(-variable)  # Map =variable to 2 * variable + 1
+    xor_clauses = []
+    next_variable = max_variable + 1
 
-        new_var = next_variable
-        new_clauses.extend([[positive_literal, negative_literal, new_var],
-                         [positive_literal, negative_literal, new_var + 1],
-                         [new_var, new_var + 1, new_var + 2]])
-        next_variable += 3
-
-    for clause in clauses: # Classic reduction from 3SAT to 1-IN-3-3SAT 
-        # We map literals to positive variables
-        x, y, z = utils.double(-clause[0]), utils.double(clause[1]), utils.double(-clause[2])
+    for clause in clauses:
+        x, y, z = clause[0], clause[1], clause[2]
         # Auxiliary variables
-        a, b, d, e = next_variable, next_variable + 1, next_variable + 2, next_variable + 3 
-        # monotone 1-IN-3-3SAT clauses
-        new_clauses.extend([[x, a, b], [y, b, d], [z, d, e]])
-        next_variable += 4
-
-    return new_clauses, next_variable - 1    
-
-
-def reduce_1_in_3_3msat_to_unknown(clauses, max_variable):
-    """
-    Converts a 3SAT formula to a Unknown instance.
+        a_x, b_x = next_variable, next_variable + 1
+        d_y, e_y = next_variable + 2, next_variable + 3
+        f_z, g_z = next_variable + 4, next_variable + 5
+        next_variable += 6    
+        # F_i formula
+        F_i = [[-x, y], [-y, z], [-z, x]]
+        # E_i formula
+        E_i = [[x, y, z], [x, y, z, a_x]]
+        # F_i AND E_i
+        xor_clauses.extend(F_i + E_i)
+
+    return xor_clauses
+
+def reduce_cnf_to_3sat(clauses, max_variable):
+    """Reduces a CNF formula to a 3SAT instance.
 
     Args:
-        clauses: A list of 3CNF clauses.
-        max_variable: The maximum variable in the input formula.
-
-    Returns: A tuple (new_clauses), where:
-            - new_clauses: A list of Unknown clauses.
+        clauses: A list of clauses in CNF form.
+        max_variable: The maximum variable in the CNF formula.
+    
+    Returns:
+        A list of 3CNF clauses.
     """
 
-    new_clauses = []
-    next_variable = max_variable + 1
-    # Dictionary of variable pairs
-    pairs_dict = {}
+    # Convert the CNF formula to 3SAT
+    three_sat_clauses, _ = reduce_sat_to_3sat(clauses, max_variable)
 
-    for clause in clauses:
-        # Sort monotone clause in ascending order
-        sorted_clause = list(sorted(clause))
-        # Sorted variables
-        x, y, z = sorted_clause[0], sorted_clause[1], sorted_clause[2]
-        # Sorted Pairs such that (a, b) = (min(a, b), max(a, b))
-        x_y, y_x, x_z = (x, y), (y, z), (x, z)
-        pairs_list = [x_y, y_x, x_z]
-        for pair in pairs_list: # Register each new pair
-            if pair not in pairs_dict:
-                pairs_dict[pair] = next_variable
-                next_variable += 1
-        # Unknown instance        
-        new_clauses.extend([[x, y, z]])        
-
-    return new_clauses    
+    return three_sat_clauses
 
-def reduce_sat(clauses, max_variable, brute_force=False):
-    """
-    Reduces a CNF formula to an 3SAT instance.
+def reduce_cnf_to_xor_sat(clauses, max_variable):
+    """Reduces a CNF formula to a XOR-SAT instance.
 
     Args:
         clauses: A list of clauses in CNF form.
-        max_variable: The maximum variable.
-        brute_force: A boolean indicating whether to use brute force reduction.
+        max_variable: The maximum variable in the CNF formula.
 
-    Returns: A tuple (new_clauses, pure_literals), where:
-            - new_clauses: A list of 3CNF clauses
-            - pure_literals: Literals determined to be always true after simplification.
+    Returns:
+        A list of XOR CNF clauses.
     """
 
     # Convert the CNF formula to 3SAT
-    new_clauses, next_variable = reduce_sat_to_3sat(clauses, max_variable)
+    three_sat_clauses, new_max_variable = reduce_sat_to_3sat(clauses, max_variable)
 
-    if brute_force:
-
-        # Convert the 3SAT formula to mock 1-IN-3-3SAT
+    # Convert the 3SAT instance to XOR-SAT formula
+    xor_clauses = reduce_3sat_to_xor_sat(three_sat_clauses, new_max_variable)
 
-        new_clauses, next_variable = utils.reduce_3sat_to_mock_1_in_3_3msat(new_clauses, next_variable)
+    return xor_clauses
 
-    else: 
-        # Convert the 3SAT formula to monotone 1-IN-3-3SAT
-
-        new_clauses, next_variable = reduce_3sat_to_1_in_3_3msat(new_clauses, next_variable)
-
-        # Convert the monotone 1-IN-3-3SAT formula to Unknown
 
-        new_clauses = reduce_1_in_3_3msat_to_unknown(new_clauses, next_variable)
-
-    return new_clauses