Browse Prior Art Database

Reuse for Inter-bound SAT Solver runs

IP.com Disclosure Number: IPCOM000236598D
Publication Date: 2014-May-05
Document File: 11 page(s) / 69K

Publishing Venue

The IP.com Prior Art Database

Abstract

A method for reuse for inter-bound Boolean Satisfiability Problem (SAT) Solver runs is disclosed.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 20% of the total text.

Page 01 of 11

Reuse for Inter-bound SAT Solver runs


Disclosed is a method for reuse for inter-bound Boolean Satisfiability Problem (SAT)

Solver runs.

An optimization for "information re-using" between two SAT runs of the same problem for two different bounds. (Incremental in bounds reuse, not incremental as in two runs of the same problem with different properties). An equivalent problem has a few intermediate steps that over-approximate and two final versions that exactly solve the original problem. The equivalent problem can be used in parallel with the solving of the original problem. One the answer is determined, processing is stopped. Under some circumstances, the equivalent problem determines faster the answer that the problem is un-satisfiable. This represents the situations when it does take more time to get to this conclusion.

Inter-Bound Reuse

The bound incremental reuse may be targeted with the purpose of identifying a way to re-use the work done for a lower bound, in the work needed to determine a higher bound.

The disclosed approach is to find a different way to express the new problem to be solved, for the higher bound. The equivalent problem should provide the following value:

It has the same solutions as the original problem


1.

There are circumstances in which it is easier to compute

2.

In order to identify an equivalent problem, analysis is started by determining the meaning of moving from a lower bound to a higher bound. Focus is on the changes in the conjunctive normal form (CNF) problem as the bound increases when it is known that the lower bound had no solution.


1. Problem Analysis

1 Inter-Bound Assumption

Bounded model checker (BMC) is used in order to prove a property for two different bounds.

First Assumption: The problem did not provide any solution for a lower bound hence the user will run again the same problem with a higher bound.

Second Assumption: The tool that builds the mathematical model will not change the

1


Page 02 of 11

meaning and the representation of the variables and clauses that already existed in the lower bound while moving to the higher bound. This consistency in meaning can be kept (and is generally) valid and allows an analysis of the changes that happen from a one bound to another.


2 Changes Due to Bound Increase
2.1 Lost Clauses
The CNF problems is generated for two different bounds with the assumption that the problem for the lower bound L is not satisfied. The problem for the higher bound H will have common clauses and variables with the L and will have different variables/clauses due to the additional problem space generated by the increase in bound.

Consider:

common

P L H

the clauses found in both

P H L

 

new

the clauses added by the bound increase

P L P

 

lost common

the clauses that were part of L and are not in


H anymore

Statement 1: If lost
L is empty H has no solution.

Proof 1.

If all clauses from L are incorporated into H , knowing that there is no combination of variab...