PySA-DPLL Solvers

This library implements the DPLL algorithm for PySA, an exact solver for SAT formulas. SAT problems are accepted in standard CNF format.

Getting Started (Applications)

The standalone command line application is configured using CMake. A C++17 compliant compiler is required. To build all targets, including examples and tests,

$ cmake -DCMAKE_BUILD_TYPE=Release -S . -B ./build-release/ && cmake --build ./build-release

The executable is built to ./build-release/src/dpll-sat.x .

DPLL-SAT uses standard C++ concurrency to parallelize generic branch exploration. Additionally, it supports distributing branches using MPI processes when compiled with MPI support by passing -DMPI=ON to CMake, and optionally -DMPIEXEC_EXECUTABLE=/path/to/mpiexec.

A Python interface is also available, and it can be installed using pip:

$ pip install [pysa_dpll_folder]

or directly from GitHub:

$ pip install git+https://github.com/nasa/pysa@pysa-dpll 

MPI is supported through the Python interface, but it must be enabled during the installation:

$ USE_MPI=1 pip install [pysa_dpll_folder]

or

$ USE_MPI=1 pip install git+https://github.com/nasa/pysa@pysa-dpll 

Similarly, PySA-DPLL can be installed as a container:

$ docker build . -t pysa-dpll

The formula can be then provided as stdin:

$ echo -e 'p cnf 2 1\n1 2 0' | docker run -i --rm pysa-dpll sat
[
  {
    "state": "01",
    "n_unsat": 0
  },
  {
    "state": "10",
    "n_unsat": 0
  },
  {
    "state": "11",
    "n_unsat": 0
  }
]

PySA-DPLL

pysa-dpll is the Python interface of PySA-DPLL:

$ pysa-dpll --help
 Usage: pysa-dpll [OPTIONS] COMMAND [ARGS]...

 PySA-DPLL

╭─ Options ────────────────────────────────────────────────────────────────────────────╮
│ --filename            -f      TEXT     Filename to use. Otherwise use stdin.         |
│ --walltime            -w      FLOAT    Walltime in seconds. [default: None]          |
│ --n-threads                   INTEGER  Number of threads to use (by default, all     |
|                                        available cores are used). [default: None]    |
│ --verbose             -v               Verbose output.                               |
│ --install-completion                   Install completion for the current shell.     |
│ --show-completion                      Show completion for the current shell, to     |
|                                        copy it or customize the installation.        |
│ --help                                 Show this message and exit.                   |
╰──────────────────────────────────────────────────────────────────────────────────────╯
╭─ Commands ───────────────────────────────────────────────────────────────────────────╮
│ sat   Find all configurations with a maximum number of unsatisfied clauses           │
╰──────────────────────────────────────────────────────────────────────────────────────╯

DPLL-SAT

DPLL-SAT enumerates all solutions up to a maximum number of unsatisfied clauses.

Usage: dpll-sat.x cnf_file [max_unsat = 0] [n_threads = 0] [verbose = 0]
Solve SAT formula in CNF format using DPLL.

   max_unsat    Number of maximum unsatisfied clauses that a configuration can have (default = 0)
   n_threads    Number of threads to use (default = 0, that is suggested by the implementation)
   verbose      Level of verbosity (default = 0)

If compiled with MPI, the application can be started using mpirun with the number of desired MPI processes.

Contributors

Salvatore Mandrà
Humberto Munoz-Bauza

NASA Open Source Agreement and Contributions

See NOSA.

Notices

Copyright @ 2023, United States Government, as represented by the Administrator of the National Aeronautics and Space Administration. All rights reserved.

Disclaimer

No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER, GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES IT "AS IS."

Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE, INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS AGREEMENT.

Licence

Copyright © 2023, United States Government, as represented by the Administrator of the National Aeronautics and Space Administration. All rights reserved.

The PySA, a powerful tool for solving optimization problems is licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at http://www.apache.org/licenses/LICENSE-2.0.

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.