Create new SAT generators

ml4co_kit/__init__.py

@@ -88,6 +88,10 @@
     PCTSPGenerator, SPCTSPGenerator, TSPGenerator, 
 )
 
+# SAT Generator
+from .generator import SATGeneratorBase, SAT_DISTRIBUTION
+from .generator import SATPGenerator, SATAGenerator, USATCGenerator
+
 
 ####################################################
 #                      Solver                      #

ml4co_kit/generator/__init__.py

@@ -40,4 +40,10 @@
 from .routing.op import OPGenerator, OP_TYPE
 from .routing.pctsp import PCTSPGenerator, PCTSP_TYPE
 from .routing.spctsp import SPCTSPGenerator, SPCTSP_TYPE
-from .routing.tsp import TSPGenerator, TSP_TYPE
+from .routing.tsp import TSPGenerator, TSP_TYPE
+
+# SAT Generator
+from .sat.base import SATGeneratorBase, SAT_DISTRIBUTION
+from .sat.satp import SATPGenerator
+from .sat.sata import SATAGenerator
+from .sat.unsatc import USATCGenerator

ml4co_kit/generator/sat/__init__.py

@@ -0,0 +1,19 @@
+r"""
+SAT Generator Module.
+"""
+
+# Copyright (c) 2024 Thinklab@SJTU
+# ML4CO-Kit is licensed under Mulan PSL v2.
+# You can use this software according to the terms and conditions of the Mulan PSL v2.
+# You may obtain a copy of Mulan PSL v2 at:
+# http://license.coscl.org.cn/MulanPSL2
+#
+# THIS SOFTWARE IS PROVIDED ON AN "AS IS" BASIS, WITHOUT WARRANTIES OF ANY KIND,
+# EITHER EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO NON-INFRINGEMENT,
+# MERCHANTABILITY OR FIT FOR A PARTICULAR PURPOSE.
+# See the Mulan PSL v2 for more details.
+
+from .base import SATGeneratorBase, SAT_DISTRIBUTION
+from .satp import SATPGenerator
+from .sata import SATAGenerator
+from .unsatc import USATCGenerator

ml4co_kit/generator/sat/base.py

@@ -0,0 +1,146 @@
+r"""
+Base classes for all SAT problem generators.
+"""
+
+# Copyright (c) 2024 Thinklab@SJTU
+# ML4CO-Kit is licensed under Mulan PSL v2.
+# You can use this software according to the terms and conditions of the Mulan PSL v2.
+# You may obtain a copy of Mulan PSL v2 at:
+# http://license.coscl.org.cn/MulanPSL2
+#
+# THIS SOFTWARE IS PROVIDED ON AN "AS IS" BASIS, WITHOUT WARRANTIES OF ANY KIND,
+# EITHER EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO NON-INFRINGEMENT,
+# MERCHANTABILITY OR FIT FOR A PARTICULAR PURPOSE.
+# See the Mulan PSL v2 for more details.
+
+
+import numpy as np
+from enum import Enum
+from typing import Union, List, Optional
+from ml4co_kit.task.base import TASK_TYPE
+from ml4co_kit.generator.base import GeneratorBase
+from ml4co_kit.task.sat.base import SATTaskBase
+
+
+class SAT_DISTRIBUTION(str, Enum):
+    """Define the SAT distribution types as an enumeration."""
+
+    # Basic distributions
+    UNIFORM_RANDOM = "uniform_random"  # Standard k-SAT with uniform random clauses
+
+    # Theory-based distributions
+    PHASE_TRANSITION = "phase_transition"  # Near satisfiability phase transition
+
+    # Solution-based distributions
+    PLANTED = "planted"  # Planted solution (guaranteed SAT)
+
+    # Advanced distributions (G4SATBench)
+    SR = "sr"  # Satisfiability Resolution (near SAT/UNSAT boundary)
+    CA = "ca"  # Community Attachment (industrial-like)
+
+    # NP-complete reductions
+    K_CLIQUE = "k_clique"  # Reduction from k-clique problem
+    K_DOMSET = "k_domset"  # Reduction from dominating set problem
+
+
+class SATGeneratorBase(GeneratorBase):
+    """Base class for all SAT problem generators."""
+
+    def __init__(
+        self, 
+        task_type: TASK_TYPE,
+        distribution_type: SAT_DISTRIBUTION = SAT_DISTRIBUTION.UNIFORM_RANDOM,
+        precision: Union[np.float32, np.float64] = np.float32,
+        vars_num: int = 50,
+        clauses_num: Optional[int] = None,
+        clause_length: int = 3,
+        seed: Optional[int] = None,
+    ):
+        # Super Initialization
+        super(SATGeneratorBase, self).__init__(
+            task_type=task_type,
+            distribution_type=distribution_type,
+            precision=precision
+        )
+
+        # Initialize Attributes
+        self.vars_num = vars_num
+        self.clause_length = clause_length
+        self.seed = seed
+
+        # Auto-calculate clauses_num if not provided
+        if clauses_num is None:
+            self.clauses_num = self._default_clauses_num()
+        else:
+            self.clauses_num = clauses_num
+
+        # Set random seed
+        if self.seed is not None:
+            np.random.seed(self.seed)
+
+    def _default_clauses_num(self) -> int:
+        """Calculate default number of clauses based on clause length."""
+        if self.clause_length == 2:
+            # 2-SAT phase transition: α ≈ 1
+            return int(1.0 * self.vars_num)
+        elif self.clause_length == 3:
+            # 3-SAT phase transition: α ≈ 4.26
+            return int(4.26 * self.vars_num)
+        else:
+            # k-SAT phase transition: α ≈ 2^k * ln(2)
+            alpha = (2 ** self.clause_length) * np.log(2)
+            return int(alpha * self.vars_num)
+
+    def _generate_random_clause(self, k: Optional[int] = None) -> List[int]:
+        """Generate a random clause with k literals."""
+        if k is None:
+            k = self.clause_length
+
+        # Randomly select k distinct variables
+        selected_vars = np.random.choice(
+            range(1, self.vars_num + 1), 
+            size=min(k, self.vars_num), 
+            replace=False
+        )
+
+        # Randomly assign polarities
+        clause = []
+        for var in selected_vars:
+            if np.random.random() < 0.5:
+                clause.append(int(var))  # Positive literal
+            else:
+                clause.append(-int(var))  # Negative literal
+
+        return clause
+
+    def _check_vig_connectivity(self, clauses: List[List[int]]) -> bool:
+        """
+        Check if Variable Incidence Graph (VIG) is connected.
+
+        VIG: nodes are variables, edges connect variables appearing together.
+        """
+        try:
+            import networkx as nx
+        except ImportError:
+            # If networkx not available, skip connectivity check
+            return True
+
+        # Build VIG
+        G = nx.Graph()
+        G.add_nodes_from(range(1, self.vars_num + 1))
+
+        for clause in clauses:
+            vars_in_clause = [abs(lit) for lit in clause]
+            # Add edges between all pairs in this clause
+            for i in range(len(vars_in_clause)):
+                for j in range(i + 1, len(vars_in_clause)):
+                    G.add_edge(vars_in_clause[i], vars_in_clause[j])
+
+        return nx.is_connected(G)
+
+    def _create_instance(self, clauses: List[List[int]], **kwargs) -> SATTaskBase:
+        """
+        Create a SAT task instance. 
+        Subclasses should override this to return specific task types.
+        """
+        raise NotImplementedError("Subclasses should implement _create_instance")

ml4co_kit/generator/sat/sata.py

@@ -0,0 +1,151 @@
+r"""
+Generator for SAT-A (Satisfying Assignment Prediction) task instances.
+"""
+
+# Copyright (c) 2024 Thinklab@SJTU
+# ML4CO-Kit is licensed under Mulan PSL v2.
+# You can use this software according to the terms and conditions of the Mulan PSL v2.
+# You may obtain a copy of Mulan PSL v2 at:
+# http://license.coscl.org.cn/MulanPSL2
+#
+# THIS SOFTWARE IS PROVIDED ON AN "AS IS" BASIS, WITHOUT WARRANTIES OF ANY KIND,
+# EITHER EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO NON-INFRINGEMENT,
+# MERCHANTABILITY OR FIT FOR A PARTICULAR PURPOSE.
+# See the Mulan PSL v2 for more details.
+
+
+import numpy as np
+from typing import Union, List, Optional
+from ml4co_kit.task.base import TASK_TYPE
+from ml4co_kit.task.sat import SATATask
+from ml4co_kit.generator.sat.base import SATGeneratorBase, SAT_DISTRIBUTION
+
+
+class SATAGenerator(SATGeneratorBase):
+    """Generator for SAT-A (Satisfying Assignment Prediction) task instances."""
+
+    def __init__(
+        self,
+        distribution_type: SAT_DISTRIBUTION = SAT_DISTRIBUTION.PLANTED,
+        precision: Union[np.float32, np.float64] = np.float32,
+        vars_num: int = 50,
+        clauses_num: Optional[int] = None,
+        clause_length: int = 3,
+        seed: Optional[int] = None,
+    ):
+        # Super Initialization
+        super(SATAGenerator, self).__init__(
+            task_type=TASK_TYPE.SATA,
+            distribution_type=distribution_type,
+            precision=precision,
+            vars_num=vars_num,
+            clauses_num=clauses_num,
+            clause_length=clause_length,
+            seed=seed
+        )
+
+        # Generation function dictionary
+        # SAT-A only generates SAT instances
+        self.generate_func_dict = {
+            SAT_DISTRIBUTION.PLANTED: self._generate_planted,
+            SAT_DISTRIBUTION.UNIFORM_RANDOM: self._generate_uniform_random_sat,
+        }
+
+    def _create_instance(
+        self, 
+        clauses: List[List[int]], 
+        solution: np.ndarray,
+        **kwargs
+    ) -> SATATask:
+        """Create a SAT-A task instance."""
+        task = SATATask(precision=self.precision)
+        task.from_data(
+            clauses=clauses,
+            vars_num=self.vars_num,
+            sol=solution,
+            ref=True  # This is a reference solution
+        )
+        return task
+
+    def _generate_planted(self) -> SATATask:
+        """Generate SAT instance with planted solution."""
+        # Generate planted solution
+        solution = np.random.randint(0, 2, self.vars_num).astype(bool)
+
+        clauses = []
+        for _ in range(self.clauses_num):
+            # Generate clause satisfied by the solution
+            clause = self._generate_satisfying_clause(solution)
+            clauses.append(clause)
+
+        return self._create_instance(clauses, solution)
+
+    def _generate_satisfying_clause(self, solution: np.ndarray) -> List[int]:
+        """Generate a clause satisfied by the given solution."""
+        while True:
+            clause = self._generate_random_clause()
+
+            # Check if at least one literal is satisfied
+            satisfied = False
+            for lit in clause:
+                var_idx = abs(lit) - 1
+                if (lit > 0 and solution[var_idx]) or (lit < 0 and not solution[var_idx]):
+                    satisfied = True
+                    break
+
+            if satisfied:
+                return clause
+
+            # If not satisfied, flip one literal to satisfy it
+            lit_to_flip = np.random.choice(len(clause))
+            var_idx = abs(clause[lit_to_flip]) - 1
+
+            if solution[var_idx]:
+                clause[lit_to_flip] = abs(clause[lit_to_flip])  # Make positive
+            else:
+                clause[lit_to_flip] = -abs(clause[lit_to_flip])  # Make negative
+
+            return clause
+
+    def _generate_uniform_random_sat(self) -> SATATask:
+        """
+        Generate uniform random SAT instance and find solution using solver.
+        Warning: This may fail if instance is UNSAT.
+        """
+        try:
+            from pysat.solvers import Glucose3
+        except ImportError:
+            print("Warning: python-sat not installed, using planted generation")
+            return self._generate_planted()
+
+        max_attempts = 100
+        for attempt in range(max_attempts):
+            clauses = []
+            for _ in range(self.clauses_num):
+                clause = self._generate_random_clause()
+                clauses.append(clause)
+
+            # Check if SAT and get solution
+            solver = Glucose3()
+            for clause in clauses:
+                solver.add_clause(clause)
+
+            if solver.solve():
+                # Get model (solution)
+                model = solver.get_model()
+                solver.delete()
+
+                # Convert model to boolean array
+                solution = np.zeros(self.vars_num, dtype=bool)
+                for lit in model:
+                    if abs(lit) <= self.vars_num:
+                        var_idx = abs(lit) - 1
+                        solution[var_idx] = (lit > 0)
+
+                return self._create_instance(clauses, solution)
+
+            solver.delete()
+
+        # If all attempts failed, use planted generation
+        print(f"Warning: Failed to generate SAT instance after {max_attempts} attempts, using planted")
+        return self._generate_planted()