microsat's Introduction

microsat

microsat is a simple CDCL SAT solver, originally created by Marijn Heule and Armin Biere.

This fork adds the following features:

Deduce implicit variable decisions by propagating a (partial) assignment of the SAT problem variables
Check the status of a (partial) assignment of the SAT problem variables:
- BUILDABLE: The problem will evaluate to true after completing the assignment by setting all undecided variables implicitely to false.
- INCOMPLETE: Otherwise.

Build

./configure && make

Build and Install

./configure && sudo make install

Usage

Print usage

microsat

Version info

microsat --version

Check satisfiability of a DIMACS encoded SAT problem

microsat DIMACS_FILE

Propagate an (partial) assignment

microsat --propagate DIMACS_FILE

DIMACS file

The (partial) assignment is denoted as a DIMACS comment line which has to be added somewhere before the problem line:

c v<NUMBER_OF_ASSIGNED_VARIABLES> <ASSIGNED_VARIABLES>

For example:

c v4 5 -7 18 -20
p cnf ...

Two demo files (one for each status described above) can be found in the test subdirectory.

microsat's People

Contributors

Stargazers

Watchers

microsat's Issues

Segmentation fault

If I build and execute microsat on my Mac, in a 32 bit Ubuntu VM or using WSL on my Windows computer, no problem occurs.

If I build and execute microsat on a 64 bit Ubuntu VM, I get a segmentation fault.

Improve formatting

Source code formatting seems to be optimized towards a small number of code lines. This results in poor readability (at least for me).

Therefore the source code should be reformatted, preferable using a code style which is similar to the one used in Glencoe.

We should make sure the comments stay in correct lines.

Detect dead variables

The modified DIMACS file format contains a list of dead variables. This is list presumed at the moment.

Dead variables can be detected by repeated SAT solving the problem p (containing variables v1-vn), considering an additional conjecture in each run: If p AND vx is UNSAT then vx is dead (given that p is SAT).

An additional mode should be implemented that detects and outputs a list of dead variables.

Detect common variables

Common variables can be detected in the same way as dead variables:

By repeated SAT solving the problem p (containing variables v1-vn), considering an additional conjecture in each run: If p AND NOT(vx) is UNSAT then vx is common (given that p is SAT).

An additional mode could be implemented that detects and outputs a list of common variables.

Recommend Projects

glnc / microsat Goto Github PK