glnc / microsat Goto Github PK

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.

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.

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.

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.