AllSMT

Introduction

AllSMT (All-Solutions Satisfiability Modulo Theories) extends AllSAT to SMT formulas, aiming to enumerate all satisfying assignments of an SMT formula. This problem is fundamental in various applications, including:

• Combinational iteration testing

• Quantitative program analysis

• Constrained test generation

• Program synthesis

• Formal verification

Related Work

The closely related AllSAT problem (finding all satisfying assignments for Boolean formulas) serves as a foundation for AllSMT. AllSAT is NP-hard and not fixed-parameter tractable unless P=NP.

Current AllSAT approaches fall into two categories:

Blocking Solvers

• Built on CDCL (Conflict-Driven Clause Learning)

• Uses non-chronological backtracking (NCB)

• Adds blocking clauses to prevent duplicate solutions

Non-blocking Solvers

• Avoids blocking clauses overhead

• Employs chronological backtracking (CB)

• Generally more memory-efficient

AllSMT in Arlib

[Content to be added]

References

[SAT23]

Masina, G., Spallita, G., Sebastiani, R. (2023). On CNF Conversion for Disjoint SAT Enumeration. SAT 2023.

[TACAS05]

Jin, H., Han, H., Somenzi, F. (2005). Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit. TACAS 2005.

[CAV02]

McMillan, K. L. (2002). Applying SAT Methods in Unbounded Symbolic Model Checking. CAV 2002.

[FMCAD04]

Grumberg, O., Schuster, A., Yadgar, A. (2004). Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis. FMCAD 2004.

[DATE04]

Li, B., Hsiao, M. S., Sheng, S. (2004). A Novel SAT All-Solutions Solver for Efficient Preimage Computation. DATE 2004.

[DPBS]

Spallitta, G., Sebastiani, R., Biere, A. Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses. GitHub Repository