ZBIGNIEW STACHNIAK



polSAT: non-clausal polarity-based SAT solver

Since the early 1990s, impressive progress has been made in applying methods for solving propositional satisfiability (SAT) to the development of effective tools in areas such as software and hardware verification, automated diagnosis, automatic test pattern generation, and scheduling. These SAT-based tools are of substantial interest to hardware manufacturers and software developers looking for high-performance formal verification tools.

polSAT is a non-clausal polarity-based stochastic local search algorithm for SAT. In contrast to "traditional" approaches that only permit inputs in conjunctive normal form (or as sets of clause), polSAT can handle inputs in an arbitrary syntactic form directly.

Detailed information on polSAT can be found in:

  • Belov, A. and Stachniak, Z. Improving Variable Selection Process in Stochastic Local Search for Propositional Satisfiability, Proc. 12th International Conference on Theory and Applications of Satisfiability Testing, SAT 2009.
  • Stachniak, Z. and Belov, A. Speeding-up Non-Clausal Local Search for Propositional Satisfiablity with Clause Learning, Proc. 11th International Conference on Theory and Applications of Satisfiability Testina (SAT 2008).
  • Belov, A., and Stachniak, Z. Substitutional Definition of Satisfiability in Classical Propositional Logic, Proc. 8th International Conference on Theory and Applications of Satisfiability Testing (SAT 2005), pp. 31--45.
  • Stachniak, Z, Going Non-clausal. 5th International Conference on the Theory and Applications of Satisfiability Testing, (SAT 2002), pp. 316--322.
polSAT has been extended to circuit inputs. Datails can be found in:
  • Belov, A., Järvisalo, M., and Stachniak, Z. Depth-Driven Circuit-Level Stochastic Local Search for SAT, Proc. of the 22nd International Joint Conference on Artificial Intelligence (IJCAI, 2011).
  • Belov, A. and Stachniak, Z. Improved Local Search for Circuit Satisfiability, Proc. 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010), LNCS 6175 (2010).

INPUT FORMULAS

polSAT accepts any formula of classical propositional logic (CPL) constructed in terms of the connectives:

  • - (negation),
  • v (disjunction),
  • & (conjunction),
  • > (implication),
  • (, ) (brackets),
and propositional variables (represented as positive integers).

Notes:

  • there is no equivalence connective,
  • Every CPL formula must end with the period,
  • input file must have .for extension.

Example: the expression

1>(-2 & -(4 & 5 v-2)). it is clearly satisgiable

is a valid input to polSAT. Any text that follows `.' of the input (in the above example: it is clearly satisfiable) is treated as a comment.

polSAT also accepts inputs in DIMACS SAT format (use .sat file extension).

polSAT source

polSAT's code is availabe on request and free of charge. Any person obtaining a copy of polSAT can use, copy, modify, merge, publish, distribute it without restrictions.

USING polSAT

Execute: polsat
with no arguments to see the usage information.

Execute: polsat [parameters] input_file
to search for a solution to a given SAT problem.

PRINTED STATISTICS

Problem information and execution statistics are displayed as shown in this example: 

Input formula                : test-problems/h-cnf-60-140-flat.sat
Variable selection algorithm : polsat
Candidate list heuristic     : all-all
Variable selection heuristic : min-cv
Filtering heuristic          : rand
Number of tries              : 100
Cutoff                       : 10000
Noise                        : 0.50

Machine name                 : indigo

Highest variable index       : 60
Polarized variables          : 0

|--------------------------------------------------------------------------------------------|
| try | sat.       | total flips | total time    | f.p.s. | candlist size | clash values     |
|     | assignment | this try    | this try (ms) |        | (min/max/avg) | (init/best/mean) |
|--------------------------------------------------------------------------------------------|
|   1 | found      |         975 |            10 |  97500 |    2  33   7  |      35   0    8 |
|   2 | found      |         582 |            10 |  58200 |    2  42   7  |      25   0    8 |
|   3 | found      |        3561 |            50 |  71220 |    2  45   7  |      27   0   10 |
.     .            .             .               .        .               .                  .
.     .            .             .               .        .               .                  .
.     .            .             .               .        .               .                  .    
|  99 | found      |         664 |            20 |  33200 |    2  33   6  |      20   0    7 |
| 100 | found      |        4194 |           100 |  41940 |    2  50   7  |      26   0   10 |
|--------------------------------------------------------------------------------------------|

Success rate                  :      94.0%
Mean number of flips when SAT :       2558
Mean f.p.s.                   :      53050
Mean candidate list size      :          7
Mean clash value              :          8

The meanings of the table's columns are as follows:

2nd column - reports whether or not a satisfying assignment was found,
3rd column - reports the total number of flips for a given try,
4th column - reports the execution time of a given try,
5th column - reports the number of flips/sec for a given try,
6th column - keeps track of the CandList size (minimal, maximal, average) for a given try,
7th column - records the cumulative clash value of the input formula for a given try (initial, best, and mean).



© ZBIGNIEW STACHNIAK 2024