### Copying Theme Documentation Template (sh) Source: https://github.com/pysathq/pysat/blob/master/web/content/getstarted.md Copies the theme's example documentation directory to create a new website project and changes the current directory to the new project folder. ```sh cp -r scientific-python-hugo-theme-main/doc ./my-website cd my-website ``` -------------------------------- ### Installing PySAT from Source using setup.py (Shell) Source: https://github.com/pysathq/pysat/blob/master/README.rst Demonstrates how to install PySAT directly from a cloned repository using the standard Python setup.py script, installing it into the system's Python path. ```Shell $ python setup.py install ``` -------------------------------- ### Building Site HTML (sh) Source: https://github.com/pysathq/pysat/blob/master/web/content/getstarted.md Executes the build process to generate the static HTML files for the website, placing the output in the './public' directory. ```sh make html ``` -------------------------------- ### Installing PySAT from Source (Bash) Source: https://github.com/pysathq/pysat/blob/master/web/content/installation.md Installs the PySAT toolkit directly from a local copy of the source repository using the setup.py script. This command installs the package into the system's default Python path. Requires Python and the PySAT source code. ```bash python setup.py install ``` -------------------------------- ### Installing PySAT with Optional Dependencies (Bash) Source: https://github.com/pysathq/pysat/blob/master/web/content/installation.md Installs the PySAT toolkit using pip, including the optional dependencies 'aiger', 'approxmc', 'cryptosat', and 'pblib'. This command is the recommended way to get the full functionality of PySAT. Requires pip to be installed and configured. ```bash pip install python-sat[aiger,approxmc,cryptosat,pblib] ``` -------------------------------- ### Installing PySAT from Source to Custom Directory (Bash) Source: https://github.com/pysathq/pysat/blob/master/web/content/installation.md Installs the PySAT toolkit from a local source copy to a specified directory using the setup.py script and the --prefix option. Replace with the desired installation path. Requires Python, the PySAT source code, and write permissions to the target directory. ```bash python setup.py install --prefix= ``` -------------------------------- ### Installing PySAT from Source to a Specific Directory (Shell) Source: https://github.com/pysathq/pysat/blob/master/README.rst Shows how to install PySAT from a cloned repository to a custom directory specified by the --prefix option using the setup.py script. ```Shell $ python setup.py install --prefix= ``` -------------------------------- ### Initializing Git and Adding Theme Submodule (sh) Source: https://github.com/pysathq/pysat/blob/master/web/content/getstarted.md Initializes a new Git repository in the project directory and adds the scientific-python-hugo-theme repository as a Git submodule under the 'themes' directory. ```sh git init git submodule add https://github.com/scientific-python/scientific-python-hugo-theme themes/scientific-python-hugo-theme ``` -------------------------------- ### Installing PySAT Base Package (Bash) Source: https://github.com/pysathq/pysat/blob/master/web/content/installation.md Installs the core PySAT toolkit using pip without including the optional dependencies. Use this command if installation of the optional packages fails or is not desired. Requires pip to be installed and configured. ```bash pip install python-sat ``` -------------------------------- ### Serving Site Locally (sh) Source: https://github.com/pysathq/pysat/blob/master/web/content/getstarted.md Builds and serves the Hugo site locally, typically accessible at http://localhost:1313, allowing for live preview during development. ```sh make serve ``` -------------------------------- ### Installing PySAT without Optional Dependencies via Pip (Shell) Source: https://github.com/pysathq/pysat/blob/master/README.rst Shows the basic pip command to install the PySAT library without any of the optional dependencies. ```Shell $ pip install python-sat ``` -------------------------------- ### Serving the Hugo Site Locally (Shell) Source: https://github.com/pysathq/pysat/blob/master/web/themes/scientific-python-hugo-theme/doc/content/getstarted.md Runs the `make serve` command, which typically executes the Hugo command to build and serve the website locally. This allows the user to preview the site in a web browser, usually at `http://localhost:1313`. ```sh make serve ``` -------------------------------- ### Installing PySAT with Optional Dependencies via Pip (Shell) Source: https://github.com/pysathq/pysat/blob/master/README.rst Provides the command to install the PySAT library using pip, including optional dependencies like aiger, approxmc, cryptosat, and pblib for extended functionality. ```Shell $ pip install python-sat[aiger,approxmc,cryptosat,pblib] ``` -------------------------------- ### Updating PySAT with Pip (Bash) Source: https://github.com/pysathq/pysat/blob/master/web/content/installation.md Updates an existing PySAT installation to the latest version available on PyPI using pip. The -U flag ensures that the package is upgraded. Requires pip to be installed and configured. ```bash pip install -U python-sat ``` -------------------------------- ### Copying Theme Template Files (Shell) Source: https://github.com/pysathq/pysat/blob/master/web/themes/scientific-python-hugo-theme/doc/content/getstarted.md Copies the documentation directory from the downloaded theme archive to a new directory for the user's website and then changes the current directory to the newly created website directory. This sets up the basic structure for the new site. ```sh cp -r scientific-python-hugo-theme-main/doc ./my-website cd my-website ``` -------------------------------- ### Initializing Git and Adding Theme Submodule (Shell) Source: https://github.com/pysathq/pysat/blob/master/web/themes/scientific-python-hugo-theme/doc/content/getstarted.md Initializes a new Git repository in the current directory and adds the Scientific Python Hugo Theme repository as a Git submodule. This integrates the theme into the new website project, allowing for easy updates. ```sh git init git submodule add https://github.com/scientific-python/scientific-python-hugo-theme themes/scientific-python-hugo-theme ``` -------------------------------- ### Building the Hugo Site HTML Output (Shell) Source: https://github.com/pysathq/pysat/blob/master/web/themes/scientific-python-hugo-theme/doc/content/getstarted.md Executes the `make html` command, which triggers the Hugo build process to generate the static HTML files for the website. The output is typically placed in the `./public` directory, ready for deployment. ```sh make html ``` -------------------------------- ### Updating PySAT via Pip (Shell) Source: https://github.com/pysathq/pysat/blob/master/README.rst Provides the command to update an existing PySAT installation to the latest version using pip. ```Shell $ pip install -U python-sat ``` -------------------------------- ### Accessing Site Parameter in Hugo Template Source: https://github.com/pysathq/pysat/blob/master/web/content/getstarted.md Demonstrates the syntax used within Hugo templates (e.g., in CSS or HTML files) to access a parameter defined in the site's configuration file (config.yaml). ```Hugo Template {{ .Site.Params.somevar }} ``` -------------------------------- ### Running LBX as a Standalone Executable (Shell) Source: https://github.com/pysathq/pysat/blob/master/README.rst Shows how to execute the LBX tool directly from the command line, specifying options for enumeration mode, debugging, solver selection, verbosity, and input file. ```Shell $ lbx.py -e all -d -s g4 -v another-input.wcnf ``` -------------------------------- ### Basic SAT Solving with PySAT Glucose3 Source: https://github.com/pysathq/pysat/blob/master/README.rst Demonstrates the fundamental usage of PySAT's Glucose3 solver. It shows how to initialize the solver, add clauses, check satisfiability, and retrieve a satisfying model. ```python >>> from pysat.solvers import Glucose3 >>> >>> g = Glucose3() >>> g.add_clause([-1, 2]) >>> g.add_clause([-2, 3]) >>> print(g.solve()) >>> print(g.get_model()) ``` -------------------------------- ### Enumerating MCS using LBX in PySAT (Python) Source: https://github.com/pysathq/pysat/blob/master/README.rst Demonstrates how to use the LBX example solver from PySAT to load a CNF formula from a file, initialize the LBX solver, and iterate through its enumeration of Minimal Correction Subsets (MCS). ```Python from pysat.examples.lbx import LBX formula = CNF(from_file='input.cnf') mcsls = LBX(formula) for mcs in mcsls.enumerate(): print(mcs) ``` -------------------------------- ### Running LBX Example Script from Command Line Source: https://github.com/pysathq/pysat/blob/master/web/content/usage.md Executes the lbx.py script, which is a standalone example provided with PySAT. The command uses arguments to specify enumeration mode (-e all), enable debugging (-d), select the Glucose4 solver (-s g4), enable verbosity (-v), and provide the input weighted CNF file (another-input.wcnf). ```bash lbx.py -e all -d -s g4 -v another-input.wcnf ``` -------------------------------- ### Importing CNF Formula Class in PySAT Source: https://github.com/pysathq/pysat/blob/master/README.rst A simple example showing how to import the `CNF` class from the `pysat.formula` module, which is used for representing conjunctive normal form formulas in PySAT. ```python >>> from pysat.formula import CNF ``` -------------------------------- ### Extracting Unsatisfiable Cores with PySAT Minisat22 Source: https://github.com/pysathq/pysat/blob/master/README.rst Illustrates how to use PySAT's Minisat22 solver to find an unsatisfiable core. It shows initializing the solver with clauses, solving with assumptions, and retrieving the core when the formula is unsatisfiable under assumptions. ```python >>> from pysat.solvers import Minisat22 >>> >>> with Minisat22(bootstrap_with=[[-1, 2], [-2, 3]]) as m: ... print(m.solve(assumptions=[1, -3])) ... print(m.get_core()) ``` -------------------------------- ### Extracting SAT Proofs with PySAT Lingeling Source: https://github.com/pysathq/pysat/blob/master/README.rst Shows how to obtain a resolution proof from a PySAT solver that supports this feature (like Lingeling). It demonstrates creating a CNF formula, initializing the solver with proof tracking enabled, solving, and printing the proof if the formula is unsatisfiable. ```python >>> from pysat.formula import CNF >>> from pysat.solvers import Lingeling >>> >>> formula = CNF() >>> formula.append([-1, 2]) >>> formula.append([1, -2]) >>> formula.append([-1, -2]) >>> formula.append([1, 2]) >>> >>> with Lingeling(bootstrap_with=formula.clauses, with_proof=True) as l: ... if l.solve() == False: ... print(l.get_proof()) ``` -------------------------------- ### Example Fenced Code Block in Markdown (Markdown) Source: https://github.com/pysathq/pysat/blob/master/web/themes/scientific-python-hugo-theme/doc/content/features.md This example shows how to include a code snippet within your Markdown content using fenced code blocks. Specify the language (e.g., `python`) immediately after the opening backticks to enable syntax highlighting for that language. ```Markdown ```python def foo(x): return x**2 ``` ``` -------------------------------- ### Enumerating MCS using LBX Example Algorithm in PySAT Source: https://github.com/pysathq/pysat/blob/master/web/content/usage.md Loads a CNF formula from 'input.cnf'. It then initializes the LBX algorithm, designed for enumerating Minimal Correction Subsets (MCSs), using the weighted version of the formula. The code iterates through and prints each enumerated MCS found by the algorithm. ```python >>> from pysat.formula import CNF >>> from pysat.examples.lbx import LBX >>> >>> formula = CNF(from_file='input.cnf') >>> mcsls = LBX(formula.weighted()) >>> >>> for mcs in mcsls.enumerate(): ... print(mcs) ``` -------------------------------- ### Run Team Query Script (Bash) Source: https://github.com/pysathq/pysat/blob/master/web/themes/scientific-python-hugo-theme/doc/content/features.md Execute this command to run the `team_query.py` script. It queries the specified GitHub organization and team, generates Markdown content for the team members, and redirects the output to a file. Requires the `GH_TOKEN` environment variable to be set with a personal access token. ```Bash python team_query.py --org scientific-python --team spec-steering-committee --title "Spec Steering Committee" > content/en/teams/spec-steering-committee.md ``` -------------------------------- ### Extracting Proof of Unsatisfiability with Lingeling in PySAT Source: https://github.com/pysathq/pysat/blob/master/web/content/usage.md Constructs a CNF formula representing (-1 or 2) and (1 or -2) and (-1 or -2) and (1 or 2), which is unsatisfiable. It initializes the Lingeling solver with this formula and enables proof generation. If the formula is unsatisfiable (which it is), it prints the resolution proof steps. ```python >>> from pysat.formula import CNF >>> from pysat.solvers import Lingeling >>> >>> formula = CNF() >>> formula.append([-1, 2]) >>> formula.append([1, -2]) >>> formula.append([-1, -2]) >>> formula.append([1, 2]) >>> >>> with Lingeling(bootstrap_with=formula.clauses, with_proof=True) as l: ... if l.solve() == False: ... print(l.get_proof()) ... ``` -------------------------------- ### Generate Custom Chroma Stylesheet (Bash) Source: https://github.com/pysathq/pysat/blob/master/web/themes/scientific-python-hugo-theme/doc/content/features.md Use this command to generate a CSS stylesheet for syntax highlighting based on a specified Chroma theme (e.g., `monokai`). The output is redirected to a CSS file in the assets directory, which can then be included in your site. ```Bash hugo gen chromastyles --style=monokai > /assets/css/code-highlight.css ``` -------------------------------- ### Configure Plausible Analytics in Hugo (YAML) Source: https://github.com/pysathq/pysat/blob/master/web/themes/scientific-python-hugo-theme/doc/content/features.md Add this configuration block under the `params` section in your Hugo config file (e.g., `config.yaml`) to enable Plausible analytics. Set `dataDomain` to your site's domain and `javaScript` to the path of the Plausible script. ```YAML params: plausible: dataDomain: your-domain.org javaScript: https://your.plausible.io/javascript/path.js ``` -------------------------------- ### Basic SAT Solving with Glucose3 in PySAT Source: https://github.com/pysathq/pysat/blob/master/web/content/usage.md Initializes the Glucose3 SAT solver, adds two clauses (-1 or 2) and (-2 or 3), solves the formula, and prints the result (True) and the satisfying model [-1, -2, -3]. ```python >>> from pysat.solvers import Glucose3 >>> >>> g = Glucose3() >>> g.add_clause([-1, 2]) >>> g.add_clause([-2, 3]) >>> print(g.solve()) >>> print(g.get_model()) ... ``` -------------------------------- ### Configure Hugo for Code Highlighting (YAML) Source: https://github.com/pysathq/pysat/blob/master/web/themes/scientific-python-hugo-theme/doc/content/features.md Add this configuration block to your Hugo config file (e.g., `config.yaml`) to enable syntax highlighting for code blocks using Chroma. Setting `noClasses` to `false` allows the use of CSS classes for styling. ```YAML markup: highlight: noClasses: false ``` -------------------------------- ### Extracting Unsatisfiable Core with Minisat22 in PySAT Source: https://github.com/pysathq/pysat/blob/master/web/content/usage.md Initializes the Minisat22 solver with initial clauses (-1 or 2) and (-2 or 3). It then attempts to solve the formula under assumptions (1 and -3), which makes it unsatisfiable. The code prints the result (False) and the unsatisfiable core [-3, 1]. ```python >>> from pysat.solvers import Minisat22 >>> >>> with Minisat22(bootstrap_with=[[-1, 2], [-2, 3]]) as m: ... print(m.solve(assumptions=[1, -3])) ... print(m.get_core()) ... ``` -------------------------------- ### Include Custom SVG Icon Partial (Go Template) Source: https://github.com/pysathq/pysat/blob/master/web/themes/scientific-python-hugo-theme/doc/content/features.md Use this Hugo partial call within your templates to display a custom SVG icon located in the `/assets/icons` directory. The partial takes the icon filename (without the `.svg` extension) as an argument. ```Go Template {{ partial "svg-icon" "my-icon" }} ``` -------------------------------- ### BibTeX Citation for PySAT (SAT 2018) Source: https://github.com/pysathq/pysat/blob/master/web/content/citation.md This is the BibTeX entry for the original paper introducing PySAT, presented at the SAT 2018 conference. Use this citation to acknowledge the core PySAT toolkit in your academic work. ```BibTeX @inproceedings{imms-sat18, author = {Alexey Ignatiev and Antonio Morgado and Joao Marques{-}Silva}, title = {{PySAT:} {A} {Python} Toolkit for Prototyping with {SAT} Oracles}, booktitle = {SAT}, pages = {428--437}, year = {2018}, url = {https://doi.org/10.1007/978-3-319-94144-8_26}, doi = {10.1007/978-3-319-94144-8_26} } ``` -------------------------------- ### BibTeX Citation for PySAT (SAT 2024) Source: https://github.com/pysathq/pysat/blob/master/web/content/citation.md This is the BibTeX entry for a more recent paper related to PySAT, presented at the SAT 2024 conference. Consider citing this if your work relates to the advancements discussed in this publication. ```BibTeX @inproceedings{itk-sat24, author = {Alexey Ignatiev and Zi Li Tan and Christos Karamanos}, title = {Towards Universally Accessible {SAT} Technology}, booktitle = {SAT}, pages = {4:1--4:11}, year = {2024}, url = {https://doi.org/10.4230/LIPIcs.SAT.2024.16}, doi = {10.4230/LIPICS.SAT.2024.16}, } ``` === COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.