The incremental satisfiability problem for a two conjunctive normal form. (English) Zbl 1401.68119
Arrazola-Ramírez, José Ramón (ed.) et al., Selected papers of the 10th Latin American workshop on logic/languages, algorithms and new methods of reasoning (LANMR), Puebla, Mexico, August 15, 2016. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 328, 31-45 (2016).
Summary: We propose a novel method to review \(K \vdash \phi\) when \(K\) and \(\phi\) are both in Conjunctive Normal Forms (CF). We extend our method to solve the incremental satisfiablity problem (ISAT), and we present different cases where ISAT can be solved in polynomial time.
Especially, we present an algorithm for 2-ISAT. Our last algorithm allow us to establish an upper bound for the time-complexity of 2-ISAT, as well as to establish some tractable cases for the 2-ISAT problem.
For the entire collection see [Zbl 1352.68007].
Especially, we present an algorithm for 2-ISAT. Our last algorithm allow us to establish an upper bound for the time-complexity of 2-ISAT, as well as to establish some tractable cases for the 2-ISAT problem.
For the entire collection see [Zbl 1352.68007].
MSC:
| 68Q25 | Analysis of algorithms and problem complexity |
| 03B05 | Classical propositional logic |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
Keywords:
satisfiability problem; incremental satisfiability problem; 2-SAT; entail propositional problem; efficient satisfiability instancesReferences:
| [1] | Barrett, C.; Stump, A.; Tinelli, C., The SMT-LIB standard version 2.0 (2010), Available from |
| [3] | Cabodi, G.; Lavagno, L.; Murciano, M.; Kondratyev, A.; Watanabe, Y., Speeding-up heuristic allocation, scheduling and binding with SAT-based abstraction/refinement techniques, ACM Trans. Design Autom. Electr. Syst., 15, 2 (2010) |
| [4] | Creignou, N.; Papini, O.; Pichler, R.; Woltran, S., Belief Revision within fragments of propositional logic (2012), DBAI Tech. Report DBAI-TR-2012-75 · Zbl 1433.03044 |
| [5] | Dubois, O., Counting the number of solutions for instances of satisfiability, Theor. Comp. Sc., 81, 49-64 (1991) · Zbl 0725.68045 |
| [6] | Eén, N.; Sorensson, K., An Extensible SAT-solver, (Giunchiglia, Enrico; Tacchella, Armando, Selected Revised Papers of 6th International Conference on Theory and Applicationsof Satisfiability Testing (SAT). Selected Revised Papers of 6th International Conference on Theory and Applicationsof Satisfiability Testing (SAT), Santa Margherita Ligure, Italy. Selected Revised Papers of 6th International Conference on Theory and Applicationsof Satisfiability Testing (SAT). Selected Revised Papers of 6th International Conference on Theory and Applicationsof Satisfiability Testing (SAT), Santa Margherita Ligure, Italy, LNCS, vol. 2919 (2003)), 502-518 · Zbl 1204.68191 |
| [7] | Eén, N.; Sorensson, K., Temporal induction by incremental SAT solving, (Procs. of First Int. Workshop on Bounded Model Checking (BMC). Procs. of First Int. Workshop on Bounded Model Checking (BMC), Electronic Notes in Theoretical Computer Science, vol. 89 (2003)), 543-560 · Zbl 1271.68215 |
| [9] | Gusfield, D.; Pitt, L., A Bounded Approximation for the Minimum Cost 2-Sat Problem, Algorithmica, 8, 103-117 (1992) · Zbl 0753.68048 |
| [10] | Hooker, J. N., Solving the incremental satisfiability problem, Journal of Logic Programming, 15, 177-186 (1993) · Zbl 0787.68049 |
| [12] | Khardon, R.; Roth, D., Reasoning with Models, Artificial Intelligence, 87, 1, 187-213 (1996) · Zbl 1506.68149 |
| [14] | Mahajan, Y. S.; Zhaohui, F.; Sharad, M., ZChaff2004: An Efficient SAT Solver, (Hoos, Holger H.; Mitchell, David G., Revised Selected Papers of 7th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT). Revised Selected Papers of 7th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT), Vancouver, Canada. Revised Selected Papers of 7th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT). Revised Selected Papers of 7th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT), Vancouver, Canada, LNCS, vol. 3542 (2004)), 360-375 · Zbl 1122.68610 |
| [15] | Marchi, J.; Bittencourt, G.; Perrusssel, L., Prime forms and minimal change in propositional belief bases, Ann. Math. Artif. Intelligence, 59, 1, 1-45 (2010) · Zbl 1219.03017 |
| [16] | Nadel, A.; Ryvchin, V.; Strichman, O., Ultimately Incremental SAT, Proc. SAT 2014, LNCS, 8561, 206218 (2014) · Zbl 1423.68464 |
| [17] | Shankar, N., Mathamathematics, Machines, and Godels Proof, Cambridge Tracks in Theoretical Computer Science, vol. 38 (1997), Cambridge University Press |
| [18] | Whittemore, J.; Joonyoung, K.; Sakallah, K. A., SATIRE: A New Incremental Satisfiability Engine, (Proceedings of the 38th Design Automation Conference (DAC)- ACM. Proceedings of the 38th Design Automation Conference (DAC)- ACM, Las Vegas, USA (2001)), 542-545 |
| [19] | Wieringa, S., Incremental Satisfbiability Solving and its Applications (2014), Department of Computer Science and Engineering, Aalto University Pub., PhD thesis |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
