{"entities":{"Q2574654":{"pageid":2585397,"ns":120,"title":"Item:Q2574654","lastrevid":44383356,"modified":"2025-11-22T12:58:32Z","type":"item","id":"Q2574654","labels":{"en":{"language":"en","value":"Theory and applications of satisfiability testing. 8th international conference, SAT 2005, St Andrews, UK, June 19--23, 2005. Proceedings."}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2234333"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2574654$341586D5-0CBD-4310-8F98-42B7D869D2D5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"db8abd6fae4acafaa989d6bd5d9d9202cda5bf42","datavalue":{"value":{"text":"Theory and applications of satisfiability testing. 8th international conference, SAT 2005, St Andrews, UK, June 19--23, 2005. Proceedings.","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2574654$B04E7BC0-928C-40AB-8D89-87E990C7A317","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"096fbb1007074ab199f421a671dca2f3d892b57b","datavalue":{"value":"1077.68002","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2574654$4E45F435-E5F0-4985-9018-B09021F164AA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2574654$B717F219-9455-42DA-882A-F73CDEBE8208","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5bcdddc97c470cacef297f6810a3ba99ca55103c","datavalue":{"value":{"time":"+2005-11-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2574654$4828E098-CC22-497B-B069-3C097F02A12B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a47504f4cc55cadec71442f177ff19ea68904df5","datavalue":{"value":"The articles of this volume will be reviewed individually. The preceding conference has been reviewed (see Zbl 1075.68002).  Indexed articles:  \\textit{Argelich, Josep; Many\u00e0, Felip}, Solving over-constrained problems with SAT technology, 1-15 [Zbl 1124.68430]  \\textit{Audemard, Gilles; Sa\u00efs, Lakhdar}, A symbolic search based approach for quantified Boolean formulas, 16-30 [Zbl 1128.68451]  \\textit{Belov, Anton; Stachniak, Zbigniew}, Substitutional definition of satisfiability in classical propositional logic, 31-45 [Zbl 1128.03303]  \\textit{Dershowitz, Nachum; Hanna, Ziyad; Nadel, Alexander}, A clause-based heuristic for SAT solvers, 46-60 [Zbl 1128.68461]  \\textit{E\u00e9n, Niklas; Biere, Armin}, Effective preprocessing in SAT through variable and clause elimination, 61-75 [Zbl 1128.68463]  \\textit{Galesi, Nicola; Thapen, Neil}, Resolution and pebbling games, 76-90 [Zbl 1128.03304]  \\textit{Gent, Ian P.; Rowley, Andrew G. D.}, Local and global complete solution learning methods for QBF, 91-106 [Zbl 1128.68464]  \\textit{Goldberg, Eugene}, Equivalence checking of circuits with parameterized specifications, 107-121 [Zbl 1128.68367]  \\textit{Heule, Marijn; van Maaren, Hans}, Observed lower bounds for random 3-SAT phase transition density using linear programming, 122-134 [Zbl 1128.68466]  \\textit{Hirsch, Edward A.; Nikolenko, Sergey I.}, Simulating cutting plane proofs with restricted degree of falsity by resolution, 135-142 [Zbl 1128.03314]  \\textit{Kouril, Michal; Franco, John}, Resolution tunnels for improved SAT solver performance, 143-157 [Zbl 1128.68468]  \\textit{Li, Chu Min; Huang, Wen Qi}, Diversification and determinism in local search for satisfiability, 158-172 [Zbl 1128.68472]  \\textit{Liffiton, Mark H.; Sakallah, Karem A.}, On finding all minimally unsatisfiable subformulas, 173-186 [Zbl 1128.68473]  \\textit{Marinov, Darko; Khurshid, Sarfraz; Bugrara, Suhabe; Zhang, Lintao; Rinard, Martin}, Optimizations for compiling declarative models into Boolean formulas, 187-202 [Zbl 1128.68475]  \\textit{Prestwich, Steven}, Random walk with continuously smoothed variable weights, 203-215 [Zbl 1128.68478]  \\textit{Rolf, Daniel}, Derandomization of PPSZ for unique-\\(k\\)-SAT, 216-225 [Zbl 1128.68479]  \\textit{Sang, Tian; Beame, Paul; Kautz, Henry}, Heuristics for fast exact model counting, 226-240 [Zbl 1128.68481]  \\textit{Sheini, Hossein M.; Sakallah, Karem A.}, A scalable method for solving satisfiability of integer linear arithmetic logic, 241-256 [Zbl 1128.68483]  \\textit{Sinz, Carsten; Dieringer, Edda-Maria}, DPvis -- a tool to visualize the structure of SAT instances, 257-268 [Zbl 1128.68484]  \\textit{Southey, Finnegan}, Constraint metrics for local search, 269-281 [Zbl 1128.68485]  \\textit{Van Gelder, Allen}, Input distance and lower bounds for propositional resolution proof length, 282-293 [Zbl 1128.03315]  \\textit{van Maaren, Hans; van Norden, Linda}, Sums of squares, satisfiability and maximum satisfiability, 294-308 [Zbl 1128.68489]  \\textit{Wahlstr\u00f6m, Magnus}, Faster exact solving of SAT formulae with a low number of occurrences per variable, 309-323 [Zbl 1128.68486]  \\textit{Wei, Wei; Selman, Bart}, A new approach to model counting, 324-339 [Zbl 1128.68487]  \\textit{Zarpas, Emmanuel}, Benchmarking SAT solvers for bounded model checking, 340-354 [Zbl 1128.68368]  \\textit{Zhao, Xishun; Kleine B\u00fcning, Hans}, Model-equivalent reductions, 355-370 [Zbl 1128.68360]  \\textit{Alsinet, Teresa; Many\u00e0, Felip; Planes, Jordi}, Improved exact solvers for weighted Max-SAT, 371-377 [Zbl 1124.68429]  \\textit{Benedetti, Marco}, Quantifier trees for QBFs, 378-385 [Zbl 1128.68452]  \\textit{Bubeck, Uwe; Kleine B\u00fcning, Hans; Zhao, Xishun}, Quantifier rewriting and equivalence models for quantified Horn formulas, 386-392 [Zbl 1128.68455]  \\textit{Coste-Marquis, Sylvie; Le Berre, Daniel; Letombe, Florian}, A branching heuristics for quantified renamable Horn formulas, 393-399 [Zbl 1128.68459]  \\textit{Dantsin, Evgeny; Wolpert, Alexander}, An improved upper bound for SAT, 400-407 [Zbl 1128.68460]  \\textit{Dershowitz, Nachum; Hanna, Ziyad; Katz, Jacob}, Bounded model checking with QBF, 408-414 [Zbl 1128.68366]  \\textit{Durairaj, Vijay; Kalla, Priyank}, Variable ordering for efficient SAT search by analyzing constraint-variable dependencies, 415-422 [Zbl 1128.68462]  \\textit{Gershman, Roman; Strichman, Ofer}, Cost-effective hyper-resolution for preprocessing CNF formulas, 423-429 [Zbl 1128.68465]  \\textit{Kulikov, Alexander S.}, Automated generation of simplification rules for SAT and MAXSAT, 430-436 [Zbl 1128.68469]  \\textit{Lewis, Matthew D. T.; Schubert, Tobias; Becker, Bernd W.}, Speedup techniques utilized in modern SAT solvers -- an analysis in the MIRA environment., 437-443 [Zbl 1128.68471]  \\textit{Ling, Andrew; Singh, Deshanand P.; Brown, Stephen D.}, FPGA logic synthesis using quantified Boolean satisfiability, 444-450 [Zbl 1128.94308]  \\textit{Manquinho, Vasco; Marques-Silva, Jo\u00e3o}, On applying cutting planes in DLL-based algorithms for pseudo-Boolean optimization, 451-458 [Zbl 1128.68474]  \\textit{Meier, Andreas; Sorge, Volker}, A new set of algebraic benchmark problems for SAT solvers, 459-466 [Zbl 1128.68476]  \\textit{Mneimneh, Maher; Lynce, In\u00eas; Andraus, Zaher; Marques-Silva, Jo\u00e3o; Sakallah, Karem}, A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas, 467-474 [Zbl 1128.68477]  \\textit{Seitz, Sakari; Alava, Mikko; Orponen, Pekka}, Threshold behaviour of WalkSAT and focused Metropolis search on random 3-satisfiability, 475-481 [Zbl 1128.68482]  \\textit{Zhang, Lintao}, On subsumption removal and on-the-fly CNF simplification, 482-489 [Zbl 1128.68488]","type":"string"},"datatype":"string"},"type":"statement","id":"Q2574654$C681794D-2B38-4F5B-9EED-1D3D7222E988","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2574654$19E6CEA4-2F85-4136-BBC8-FE8E336B7800","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2574654$5C888E65-E505-466E-B57A-8E58FE8ED67F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6f2c17db95e93f9a5a19ff6c68b3a1df8b0c021e","datavalue":{"value":"00B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2574654$FA4D40E8-2CEC-4DC1-B8AD-650C1C298ED1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5ea95c9e4167d633b2e51ea50e310913842f24d4","datavalue":{"value":"2234333","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2574654$53E309F7-6FE3-4235-81FB-7D728C79193F","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2574654$342DC660-500D-4843-9E19-8D3262D95F70","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"64dc5720e0a37f50535f68f0b7d0dea92dd100ee","datavalue":{"value":"https://doi.org/10.1007/b137280","type":"string"},"datatype":"url"},"type":"statement","id":"Q2574654$07E7EA13-06D3-446B-90E1-7E04CE15EE26","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"27cb569ce05ea7d5068f7c4c9e4a78f789eebc5b","datavalue":{"value":"W2497844642","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2574654$14D72A06-97CC-4B2B-9911-A2ED2295D6F7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1afac04859384005528f8a8d1ef4ab30dee60cfd","datavalue":{"value":"10.1007/B137280","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2574654$A6A6C587-1B18-4EC9-ACDA-E2A28461C29D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2574654","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2574654"}}}}}