This is the source code of SATCH a SAT solver written from scratch in C.

Related tags

Miscellaneous satch
Overview

License: MIT Build Status

Sat Solver SATCH

This is the source code of SATCH a SAT solver written from scratch in C.

The main purpose of this solver is to provide a simple and clean code base for explaining and experimenting with SAT solvers. It is simpler than the source code of CaDiCaL and of Kissat in particular, while still featuring most important implementation techniques needed to obtain a state-of-the-art SAT solver (the current version still lacks preprocessing and incremental solving though). Thus is also serves as a gentle introduction into the code base of CaDiCaL and Kissat.

The code allows to switch off individual and more basic features at compile time by using different ./configure options. For instance completely disabling clause learning can be achieved with ./configure --no-learn. This not only gives a clean separation of features in the code but also makes it easier to disable (through the C pre-processor) redundant not needed code anymore if a certain feature is disabled.

For a more complete SAT solver you might want to use CaDiCaL, particularly for incremental usage, and for fastest solving fall back to Kissat.

Building

Run ./configure && make test to build and test the solver binary satch as well as the library libsatch.a:

satch stand-alone solver binary satch.h solver API similar to IPASIR libsatch.a library with API in satch.h

The source of the application and library consists of the following:

satch.c library code of the SAT solver stack.h generic stack implementation (header file only) rank.h generic radix-sort implementation (header file only) config.c provides build-information generated by mkconfig.sh main.c application code with parser and witness printer

The files used by the build process are the following:

VERSION current version configure configuration utility makefile.in makefile template used by configure makefile generated from makefile.in by configure mkconfig.sh generates config.c to provide build information

Some additional documentation can be found in these files:

README.md this file explains build process and files FEATURES.md compile time option and feature set-up

The configure script will generate makefile from the template makefile.in. The default make goal all first calls mkconfig.sh to generate config.c to record build and version information. Then the object files config.o, satch.o and main.o are compiled. The first two are combined to form the library libsatch.a which is linked against main.o to produce the solver binary satch. The test target will call the shell script tatch.sh, which performs tests on CNFs in cnfs. See below for information on testing and debugging.

See ./configure -h for build options and after building the solver satch -h for run-time options of the solver (solver usage is also shown at the top of main.c). For debugging you can use ./configure -g and optionally then at run-time also enable logging with ./satch -l.

Testing

For testing and debugging the following are used:

cnfs directory containing CNF files for testing catch.[ch] internal proof checker for testing and debugging testapi.c simple separate preliminary API test suite tatch.sh test suite for CNFs in cnfs and building testapi testapi binary built from testapi.c by tatch.sh

Furthermore, as we are having many different combinations of configurations, testing them is non-trivial and is achieved with the following:

combi4.sh complete 4-fold combinatorial testing of configurations gencombi.c generates configurations ("eat your own dogfood") gencombi binary built from gencombi.c (by make test) checkconfig.sh checks configurations (e.g., produced by gencombi)

Here are potential flows for testing configurations:

./combi.sh # Configure and test all 4-fold combinations # of configuration options (does not need gencombi). # Invalid combinations are tested too!

The previous command does not require gencombi and thus can be run without executing a preliminary build. Alternatively, the more flexible combinatorial testing flow does require ./configure && make gencombi first (or just ./configure && make which also builds gencombi):

./gencombi | ./checkconfig.sh # covers all valid pairs ./gencombi -a 4 | ./checkconfig.sh # 4-fold valid combinations ./gencombi -a 9 | ./checkconfig.sh # 9-fold valid combinations ./gencombi -a -i 2 | ./checkconfig.sh -i # check invalid option pairs

The first of these uses the SAT solver to generate a set of configurations which covers all valid pairs of options and at the same time makes sure that there is a configuration which does not contain it. It is also executed by the 'pairwise' make goal which also triggers the last command.

Armin Biere
February 2021

Issues
  • Small typo in a comment?

    Small typo in a comment?

    Dear Armin,

    It is nearly irrelevant, but I believe there might be a small typo in a comment (features.h:73), where NQUEUE should be replaced by NHEAP.

    Apologies if that is not the case, and thank you for this project!

    opened by JoanEspasa 3
  • Small parser issue

    Small parser issue

    I've seen a CNF input that ends with the

    -450 -480 0
    

    without a newline.

    Satch rejects this as incorrect (which sounds too harsh). I think EOF should be allowed after the last digit of a literal (or 0 in this case).

    opened by BrunoDutertre 1
Owner
Armin Biere
Professor for Computer Science at the Johannes Kepler University Linz, Austria.
Armin Biere
Lee Thomason 293 Aug 8, 2022
PastaOS is a simple open-source kernel written from scratch for didactic purposes

What is PastaOS? ================ PastaOS is a simple open-source kernel written from scratch for didactic purposes. The main goal of this project i

Andrea Righi 10 Mar 30, 2022
Tic-Tac-Toe, Scientific calculator, Sudoku solver written in C.

Simple command line projects in C: Tic-Tac-Toe - A computer Tic-Tac-Toe player. No algorithms used, simply written using too many if statements. Sudok

Kovvuri Sai Gopal Reddy 1 Dec 25, 2021
A Modern Operating System Written in C++ From Scratch!

README Features Long Mode (64-bit) OS Higher Half Kernel Stack Based - Page Frame Allocator (PMM) with O(1) time complexity Virtual Memory Manager (VM

null 7 Jun 22, 2022
SANM: A Symbolic Asymptotic Numerical Solver

SANM: A Symbolic Asymptotic Numerical Solver This repository is the official implementation of the SANM solver described in our paper to appear at SIG

Kai Jia 25 Jul 10, 2022
A crossword solver

Word Search Word search is a program that takes a corpus and searches for those words in a grid of letters using a trie and DFS. Quick start Word sear

Yuhan Liu 1 Nov 3, 2021
Wavelike and Particlelike Phonon Transport (WPPT) Solver

'WPPT': A solver for Wave- and Particle-like Phonon Transport (WPPT) Authors: Zhongwei Zhang [email protected] / [email protected], Inst

Zhongwei Zhanng 9 Jul 21, 2022
The ROS version of ICP Mapping with QPEP Solver (Quadratic Pose Estimation Problems)

The ROS version of ICP Mapping with QPEP Solver (Quadratic Pose Estimation Problems) The project is based on https://github.com/ethz-asl/ethzasl_icp_m

Jin Wu 10 Feb 25, 2022
Contains a sudoku solver - OCR. Project done with classmates during third semester at EPITA.

sudokUwU sudokUwU is a sudoku solver made by 4 students at EPITA. This project is a mandatory work from S3 cycle! The Team Johan Tran Adrian Grillet V

okywu 2 May 5, 2022
DG-Mesh-Optimization - Discontinuous Galerkin (DG) solver coupled with a Quasi-Newton line-search algorithm to optimize the DG mesh.

Date written: December 2020 This project was pursued as my final project for MECH 579 (Multidisciplinary Design Optimization) at McGill University, ta

Julien Brillon 7 Apr 6, 2022
Openmind - Deduction framework with arbitrary mathematical system solver.

openmind Compilation: Debian/Ubuntu: sudo apt install cmake g++ git libboost-all-dev libxss-dev libx11-dev libxcb-screensaver0-dev ocl-icd-opencl-dev

Sergei Krivonos 10 Apr 3, 2022
Maya Soft IK Solver

Maya Soft IK Solver Our maya IK solver is an advanced solution for 2 bones setup. It fixes the annoying “pop” problem at full extension in the normal

Toolchefs 74 Mar 3, 2022
Offline fluid simulation solver adopted from https://github.com/doyubkim/fluid-engine-dev.

FluidEngine This is a fluid simulation engine for computer graphics applications. I adopt it from Doyub Kim's fluid-engine-dev. It's built on C++11 an

YangWC 53 Jul 20, 2022
An active set-based NLP solver

SLEQP Introduction SLEQP is a software package for large-scale nonlinear optimization. It is designed to find (local) solutions of mathematical optimi

Christoph Hansknecht 6 Jul 13, 2022
Project is to port original Zmodem for Unix to CP/M and provide binaries and source code for platform specific modification as needed. Based on 1986 C source code by Chuck Forsberg

Zmodem-CP-M This repository is intended to foster a RetroBrewComputers community effort to port the original Zmodem source code for Unix to CP/M so ev

null 10 Apr 7, 2022
Project is to port original Zmodem for Unix to CP/M and provide binaries and source code for platform specific modification as needed. Based on 1986 C source code by Chuck Forsberg

Zmodem4CPM This repository is intended to foster a RetroBrewComputers community effort to port the original Zmodem source code for Unix to CP/M so eve

null 10 Apr 7, 2022
A simple Unix like operating system from scratch.

HOS-x86 an x86 operating system written from scratch How to Build? Currently you need NASM, GCC and QEMU to build the image file. Install the packages

Jayachandra Kasarla 15 Feb 7, 2021
This is an experimental OS-from-scratch project. Just for demonstration, not useful at all.

OS Playground This is an experimental OS-from-scratch project. Just for demonstration, not useful at all. Different from OS in other projects, this OS

null 5 Dec 5, 2021
A unix operating system made from scratch using c++

pranaos A unix operating system made from scratch using c++ Dependencies g++ version should be more than 10.0.0 ninja gcc compiler needed prana os is

Krisna Pranav 17 Jul 11, 2022